let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E
for i, j being Element of NAT st i < j & j < deg (MinPoly (a,F)) holds
a |^ i <> a |^ j
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E
for i, j being Element of NAT st i < j & j < deg (MinPoly (a,F)) holds
a |^ i <> a |^ j
let a be F -algebraic Element of E; :: thesis: for i, j being Element of NAT st i < j & j < deg (MinPoly (a,F)) holds
a |^ i <> a |^ j
let i, j be Element of NAT ; :: thesis: ( i < j & j < deg (MinPoly (a,F)) implies a |^ i <> a |^ j )
assume AS: ( i < j & j < deg (MinPoly (a,F)) ) ; :: thesis: a |^ i <> a |^ j
set ma = MinPoly (a,F);
reconsider n = deg (MinPoly (a,F)) as Element of NAT ;
j >= 0 + 1 by AS, INT_1:7;
then X: not MinPoly (a,F) is linear by AS, FIELD_5:def 1;
j - i <= j by XREAL_1:43;
then j - i < n by AS, XXREAL_0:2;
then Y3: n - n < n - (j - i) by XREAL_1:15;
then 0 + 1 <= (i + n) - j by INT_1:7;
then Y7: (0 + 1) - 1 <= ((i + n) - j) - 1 by XREAL_1:9;
i - j < 0 by AS, XREAL_1:49;
then Y4: n + (i - j) < n + 0 by XREAL_1:8;
reconsider k = (i + n) - j as Element of NAT by Y3, INT_1:3;
Y8: (n + (i - j)) - 1 < n - 1 by Y4, XREAL_1:9;

Y9: now :: thesis: not (i + n) - j >= n

assume (i + n) - j >= n ; :: thesis: contradiction
then ((i + n) - j) - n >= n - n by XREAL_1:9;
then (i - j) + j >= 0 + j by XREAL_1:6;
hence contradiction by AS; :: thesis: verum

end;

reconsider h = n - j as Element of NAT by AS, INT_1:5;
set p = (0_. F) +* ((k,n) --> ((1. F),(- (1. F))));

now :: thesis: for x being object st x in {k,n} holds
x in NAT

let x be object ; :: thesis: ( x in {k,n} implies b₁ in NAT )
assume x in {k,n} ; :: thesis: b₁ in NAT

per cases then ( x = k or x = n ) by TARSKI:def 2;

suppose x = k ; :: thesis: b₁ in NAT

hence x in NAT ; :: thesis: verum

end;

suppose x = n ; :: thesis: b₁ in NAT

hence x in NAT ; :: thesis: verum

end;

end;

end;

then A: {k,n} c= NAT ;
B: ( dom ((k,n) --> ((1. F),(- (1. F)))) = {k,n} & dom (0_. F) = NAT ) by FUNCT_2:def 1;
then dom ((0_. F) +* ((k,n) --> ((1. F),(- (1. F))))) = NAT \/ {k,n} by FUNCT_4:def 1
.= NAT by A, XBOOLE_1:12 ;
then ( dom ((0_. F) +* ((k,n) --> ((1. F),(- (1. F))))) = NAT & rng ((0_. F) +* ((k,n) --> ((1. F),(- (1. F))))) c= the carrier of F ) ;
then reconsider p = (0_. F) +* ((k,n) --> ((1. F),(- (1. F)))) as sequence of F by FUNCT_2:2;
reconsider p = p as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
k in dom ((k,n) --> ((1. F),(- (1. F)))) by TARSKI:def 2, B;
then p . k = ((k,n) --> ((1. F),(- (1. F)))) . k by FUNCT_4:13
.= 1. F by Y4, FUNCT_4:63 ;
then p <> 0_. F ;
then reconsider p = p as non zero Element of the carrier of (Polynom-Ring F) by UPROOTS:def 5;
reconsider p1 = p, ma1 = MinPoly (a,F) as non zero Polynomial of F ;
reconsider q1 = p1 + ma1 as Polynomial of F ;

now :: thesis: not p1 + ma1 = 0_. F

assume K: p1 + ma1 = 0_. F ; :: thesis: contradiction
K1: - p1 = (- p1) + (0_. F)
.= (p1 - p1) + ma1 by K, POLYNOM3:26
.= (0_. F) + ma1 by POLYNOM3:29 ;
set q = (0_. F) +* (((((n + i) - j) - 1),(n - 1)) --> ((- (1. F)),(1. F)));

now :: thesis: for x being object st x in {(((n + i) - j) - 1),(n - 1)} holds
x in NAT

let x be object ; :: thesis: ( x in {(((n + i) - j) - 1),(n - 1)} implies b₁ in NAT )
assume x in {(((n + i) - j) - 1),(n - 1)} ; :: thesis: b₁ in NAT

per cases then ( x = ((n + i) - j) - 1 or x = n - 1 ) by TARSKI:def 2;

suppose x = ((n + i) - j) - 1 ; :: thesis: b₁ in NAT

hence x in NAT by Y7, INT_1:3; :: thesis: verum

end;

suppose x = n - 1 ; :: thesis: b₁ in NAT

hence x in NAT by AS, INT_1:3; :: thesis: verum

end;

end;

end;

then Z2: {(((n + i) - j) - 1),(n - 1)} c= NAT ;
Z3: ( dom (((((n + i) - j) - 1),(n - 1)) --> ((- (1. F)),(1. F))) = {(((n + i) - j) - 1),(n - 1)} & dom (0_. F) = NAT ) by FUNCT_2:def 1;
then dom ((0_. F) +* (((((n + i) - j) - 1),(n - 1)) --> ((- (1. F)),(1. F)))) = NAT \/ {(((n + i) - j) - 1),(n - 1)} by FUNCT_4:def 1
.= NAT by Z2, XBOOLE_1:12 ;
then ( dom ((0_. F) +* (((((n + i) - j) - 1),(n - 1)) --> ((- (1. F)),(1. F)))) = NAT & rng ((0_. F) +* (((((n + i) - j) - 1),(n - 1)) --> ((- (1. F)),(1. F)))) c= the carrier of F ) ;
then reconsider q = (0_. F) +* (((((n + i) - j) - 1),(n - 1)) --> ((- (1. F)),(1. F))) as sequence of F by FUNCT_2:2;
reconsider q = q as Polynomial of F ;
K: <%(0. F),(1. F)%> *' q = - p1

proof

now :: thesis: for u being Element of NAT holds (<%(0. F),(1. F)%> *' q) . u = (- p1) . u

let u be Element of NAT ; :: thesis: (<%(0. F),(1. F)%> *' q) . b₁ = (- p1) . b₁

per cases ( u = 0 or u <> 0 ) ;

suppose K2: u = 0 ; :: thesis: (<%(0. F),(1. F)%> *' q) . b₁ = (- p1) . b₁

then K3: not u in dom ((k,n) --> ((1. F),(- (1. F)))) by AS, Y3;
K4: 0. F = (0_. F) . u
.= p1 . u by K3, FUNCT_4:11 ;
thus (<%(0. F),(1. F)%> *' q) . u = - (p1 . u) by K4, K2, thE2
.= (- p1) . u by BHSP_1:44 ; :: thesis: verum

end;

suppose u <> 0 ; :: thesis: (<%(0. F),(1. F)%> *' q) . b₁ = (- p1) . b₁

then consider u1 being Nat such that
K2: u = u1 + 1 by NAT_1:6;
K5: (<%(0. F),(1. F)%> *' q) . u = q . u1 by K2, thE1;

per cases ( u = k or u = n or ( u <> k & u <> n ) ) ;

suppose K6: u = k ; :: thesis: (<%(0. F),(1. F)%> *' q) . b₁ = (- p1) . b₁

k in dom ((k,n) --> ((1. F),(- (1. F)))) by TARSKI:def 2, B;
then K7: p . k = ((k,n) --> ((1. F),(- (1. F)))) . k by FUNCT_4:13
.= 1. F by Y4, FUNCT_4:63 ;
K8: u1 in dom (((((n + i) - j) - 1),(n - 1)) --> ((- (1. F)),(1. F))) by K2, K6, Z3, TARSKI:def 2;
(((((n + i) - j) - 1),(n - 1)) --> ((- (1. F)),(1. F))) . u1 = - (1. F) by K2, K6, Y8, FUNCT_4:63;
hence (<%(0. F),(1. F)%> *' q) . u = - (1. F) by K8, K5, FUNCT_4:13
.= (- p1) . u by K6, K7, BHSP_1:44 ;
:: thesis: verum

end;

suppose K6: u = n ; :: thesis: (<%(0. F),(1. F)%> *' q) . b₁ = (- p1) . b₁

n in dom ((k,n) --> ((1. F),(- (1. F)))) by TARSKI:def 2, B;
then K7: p . n = ((k,n) --> ((1. F),(- (1. F)))) . n by FUNCT_4:13
.= - (1. F) by FUNCT_4:63 ;
K8: u1 in dom (((((n + i) - j) - 1),(n - 1)) --> ((- (1. F)),(1. F))) by K2, K6, Z3, TARSKI:def 2;
(((((n + i) - j) - 1),(n - 1)) --> ((- (1. F)),(1. F))) . u1 = 1. F by K2, K6, FUNCT_4:63;
hence (<%(0. F),(1. F)%> *' q) . u = - (p1 . u) by K6, K7, K8, K5, FUNCT_4:13
.= (- p1) . u by BHSP_1:44 ;
:: thesis: verum

end;

suppose K6: ( u <> k & u <> n ) ; :: thesis: (<%(0. F),(1. F)%> *' q) . b₁ = (- p1) . b₁

then not u in dom ((k,n) --> ((1. F),(- (1. F)))) by TARSKI:def 2;
then K7: p . u = (0_. F) . u by FUNCT_4:11
.= 0. F ;
( u1 <> ((n + i) - j) - 1 & u1 <> n - 1 ) by K2, K6;
then not u1 in dom (((((n + i) - j) - 1),(n - 1)) --> ((- (1. F)),(1. F))) by TARSKI:def 2;
then q . u1 = (0_. F) . u1 by FUNCT_4:11
.= 0. F by ORDINAL1:def 12, FUNCOP_1:7 ;
hence (<%(0. F),(1. F)%> *' q) . u = - (p1 . u) by K7, K2, thE1
.= (- p1) . u by BHSP_1:44 ;
:: thesis: verum

end;

end;

end;

end;

end;

hence <%(0. F),(1. F)%> *' q = - p1 ; :: thesis: verum

end;

eval (<%(0. F),(1. F)%>,(0. F)) = (0. F) + (0. F) by POLYNOM5:47;
then <%(0. F),(1. F)%> is with_roots by POLYNOM5:def 7, POLYNOM5:def 8;
hence contradiction by K, K1, X; :: thesis: verum

end;

then reconsider q1 = q1 as non zero Polynomial of F by UPROOTS:def 5;
reconsider q = q1 as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
X: F is Subring of E by FIELD_4:def 1;

now :: thesis: not a |^ i = a |^ j

assume A0: a |^ i = a |^ j ; :: thesis: contradiction
A1: a |^ k = a |^ (i + h)
.= (a |^ i) * (a |^ h) by BINOM:10
.= a |^ (j + h) by A0, BINOM:10
.= a |^ n ;
A: deg q < deg (MinPoly (a,F))

proof

D: now :: thesis: not deg q1 = deg ma1

assume B0: deg q1 = deg ma1 ; :: thesis: contradiction
B2: ( (deg ma1) + 1 = ((len ma1) - 1) + 1 & (deg q1) + 1 = ((len q1) - 1) + 1 ) by HURWITZ:def 2;
B3: (len ma1) -' 1 = n by B2, XREAL_0:def 2;
n in dom ((k,n) --> ((1. F),(- (1. F)))) by TARSKI:def 2, B;
then p . n = ((k,n) --> ((1. F),(- (1. F)))) . n by FUNCT_4:13
.= - (1. F) by FUNCT_4:63 ;
then q1 . n = (- (1. F)) + (ma1 . n) by NORMSP_1:def 2
.= (- (1. F)) + (LC ma1) by B3, RATFUNC1:def 6
.= (- (1. F)) + (1. F) by RATFUNC1:def 7 ;
hence contradiction by B2, B0, ALGSEQ_1:10, RLVECT_1:5; :: thesis: verum

end;

now :: thesis: not deg p1 > n

assume G: deg p1 > n ; :: thesis: contradiction
B3: (deg p1) + 1 = ((len p1) - 1) + 1 by HURWITZ:def 2;
not deg p1 in dom ((k,n) --> ((1. F),(- (1. F)))) by G, Y9, TARSKI:def 2;
then p1 . (deg p1) = (0_. F) . (deg p1) by FUNCT_4:11
.= 0. F ;
hence contradiction by B3, ALGSEQ_1:10; :: thesis: verum

end;

then max ((deg p1),(deg ma1)) = deg ma1 by XXREAL_0:def 10;
then deg q <= deg ma1 by HURWITZ:22;
hence deg q < deg (MinPoly (a,F)) by D, XXREAL_0:1; :: thesis: verum

end;

reconsider pE = (anpoly ((1. E),k)) + (anpoly ((- (1. E)),n)) as Element of the carrier of (Polynom-Ring E) by POLYNOM3:def 10;
p = (anpoly ((1. E),k)) + (anpoly ((- (1. E)),n))

proof

set g = (anpoly ((1. E),k)) + (anpoly ((- (1. E)),n));

now :: thesis: for u being Element of NAT holds ((anpoly ((1. E),k)) + (anpoly ((- (1. E)),n))) . u = p . u

let u be Element of NAT ; :: thesis: ((anpoly ((1. E),k)) + (anpoly ((- (1. E)),n))) . b₁ = p . b₁

per cases ( u = k or u = n or ( u <> k & u <> n ) ) ;

suppose H: u = k ; :: thesis: ((anpoly ((1. E),k)) + (anpoly ((- (1. E)),n))) . b₁ = p . b₁

k in dom ((k,n) --> ((1. F),(- (1. F)))) by TARSKI:def 2, B;
then H1: p . k = ((k,n) --> ((1. F),(- (1. F)))) . k by FUNCT_4:13
.= 1. F by Y4, FUNCT_4:63 ;
thus ((anpoly ((1. E),k)) + (anpoly ((- (1. E)),n))) . u = ((anpoly ((1. E),k)) . u) + ((anpoly ((- (1. E)),n)) . u) by NORMSP_1:def 2
.= ((anpoly ((1. E),k)) . u) + (0. E) by Y4, H, POLYDIFF:25
.= (1. E) + (0. E) by H, POLYDIFF:24
.= p . u by H1, H, X, C0SP1:def 3 ; :: thesis: verum

end;

suppose H: u = n ; :: thesis: ((anpoly ((1. E),k)) + (anpoly ((- (1. E)),n))) . b₁ = p . b₁

n in dom ((k,n) --> ((1. F),(- (1. F)))) by TARSKI:def 2, B;
then H1: p . n = ((k,n) --> ((1. F),(- (1. F)))) . n by FUNCT_4:13
.= - (1. F) by FUNCT_4:63 ;
H2: 1. E = 1. F by X, C0SP1:def 3;
thus ((anpoly ((1. E),k)) + (anpoly ((- (1. E)),n))) . u = ((anpoly ((1. E),k)) . u) + ((anpoly ((- (1. E)),n)) . u) by NORMSP_1:def 2
.= (0. E) + ((anpoly ((- (1. E)),n)) . u) by Y4, H, POLYDIFF:25
.= (0. E) + (- (1. E)) by H, POLYDIFF:24
.= p . u by H2, H1, H, X, Th19 ; :: thesis: verum

end;

suppose H: ( u <> k & u <> n ) ; :: thesis: ((anpoly ((1. E),k)) + (anpoly ((- (1. E)),n))) . b₁ = p . b₁

then not u in dom ((k,n) --> ((1. F),(- (1. F)))) by TARSKI:def 2;
then H1: p . u = (0_. F) . u by FUNCT_4:11
.= 0. F ;
thus ((anpoly ((1. E),k)) + (anpoly ((- (1. E)),n))) . u = ((anpoly ((1. E),k)) . u) + ((anpoly ((- (1. E)),n)) . u) by NORMSP_1:def 2
.= (0. E) + ((anpoly ((- (1. E)),n)) . u) by H, POLYDIFF:25
.= (0. E) + (0. E) by H, POLYDIFF:25
.= p . u by H1, X, C0SP1:def 3 ; :: thesis: verum

end;

end;

end;

hence p = (anpoly ((1. E),k)) + (anpoly ((- (1. E)),n)) ; :: thesis: verum

end;

then B: Ext_eval (p,a) = eval (pE,a) by FIELD_4:26
.= (eval ((anpoly ((1. E),k)),a)) + (eval ((anpoly ((- (1. E)),n)),a)) by POLYNOM4:19
.= ((1. E) * (a |^ k)) + (eval ((anpoly ((- (1. E)),n)),a)) by Y3, FIELD_1:6
.= ((1. E) * (a |^ k)) + ((- (1. E)) * (a |^ k)) by A1, AS, FIELD_1:6
.= ((1. E) + (- (1. E))) * (a |^ k) by VECTSP_1:def 3
.= (0. E) * (a |^ k) by RLVECT_1:5 ;
Ext_eval (q,a) = (Ext_eval (p,a)) + (Ext_eval ((MinPoly (a,F)),a)) by X, ALGNUM_1:15
.= (0. E) + (0. E) by B, mpol3 ;
hence contradiction by mpol4, A, RING_5:13; :: thesis: verum

end;

hence a |^ i <> a |^ j ; :: thesis: verum