let F be Field; :: thesis: for E being FieldExtension of F
for a being Element of E st a ^2 in F & not a in F holds
for f being non empty quadratic FinSequence of (FAdj (F,{a})) ex g1, g2, g3 being non empty FinSequence of (FAdj (F,{a})) st
( g1 is non empty quadratic FinSequence of F & g2 is non empty quadratic FinSequence of F & g3 is non empty FinSequence of F & Sum f = ((Sum g1) + (((@ ((FAdj (F,{a})),a)) ^2) * (Sum g2))) + ((@ ((FAdj (F,{a})),a)) * (Sum g3)) )
let E be FieldExtension of F; :: thesis: for a being Element of E st a ^2 in F & not a in F holds
for f being non empty quadratic FinSequence of (FAdj (F,{a})) ex g1, g2, g3 being non empty FinSequence of (FAdj (F,{a})) st
( g1 is non empty quadratic FinSequence of F & g2 is non empty quadratic FinSequence of F & g3 is non empty FinSequence of F & Sum f = ((Sum g1) + (((@ ((FAdj (F,{a})),a)) ^2) * (Sum g2))) + ((@ ((FAdj (F,{a})),a)) * (Sum g3)) )
let a be Element of E; :: thesis: ( a ^2 in F & not a in F implies for f being non empty quadratic FinSequence of (FAdj (F,{a})) ex g1, g2, g3 being non empty FinSequence of (FAdj (F,{a})) st
( g1 is non empty quadratic FinSequence of F & g2 is non empty quadratic FinSequence of F & g3 is non empty FinSequence of F & Sum f = ((Sum g1) + (((@ ((FAdj (F,{a})),a)) ^2) * (Sum g2))) + ((@ ((FAdj (F,{a})),a)) * (Sum g3)) ) )
assume AS: ( a ^2 in F & not a in F ) ; :: thesis: for f being non empty quadratic FinSequence of (FAdj (F,{a})) ex g1, g2, g3 being non empty FinSequence of (FAdj (F,{a})) st
( g1 is non empty quadratic FinSequence of F & g2 is non empty quadratic FinSequence of F & g3 is non empty FinSequence of F & Sum f = ((Sum g1) + (((@ ((FAdj (F,{a})),a)) ^2) * (Sum g2))) + ((@ ((FAdj (F,{a})),a)) * (Sum g3)) )
let f be non empty quadratic FinSequence of (FAdj (F,{a})); :: thesis: ex g1, g2, g3 being non empty FinSequence of (FAdj (F,{a})) st
( g1 is non empty quadratic FinSequence of F & g2 is non empty quadratic FinSequence of F & g3 is non empty FinSequence of F & Sum f = ((Sum g1) + (((@ ((FAdj (F,{a})),a)) ^2) * (Sum g2))) + ((@ ((FAdj (F,{a})),a)) * (Sum g3)) )
set K = FAdj (F,{a});
( {a} is Subset of (FAdj (F,{a})) & a in {a} ) by TARSKI:def 1, FIELD_6:35;
then a is FAdj (F,{a}) -membered ;
then reconsider a = a as FAdj (F,{a}) -membered Element of E ;
ex g1, g2, g3 being non empty FinSequence of (FAdj (F,{a})) st
( dom g1 = dom f & dom g2 = dom f & dom g3 = dom f & ( for i being Nat st i in dom f holds
for x, y being Element of F st f . i = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 holds
( g1 . i = x ^2 & g2 . i = y ^2 & g3 . i = (2 '*' x) * y ) ) )
proof
defpred S1[ object , object ] means for x, y being Element of F st f . $1 = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 holds
$2 = x ^2 ;
defpred S2[ object , object ] means for x, y being Element of F st f . $1 = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 holds
$2 = y ^2 ;
defpred S3[ object , object ] means for x, y being Element of F st f . $1 = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 holds
$2 = (2 '*' x) * y;
H0: F is Subring of FAdj (F,{a}) by FIELD_4:def 1;
A1: now :: thesis: for k being Nat st k in Seg (len f) holds
ex x being Element of the carrier of (FAdj (F,{a})) st S1[k,x]
let k be Nat; :: thesis: ( k in Seg (len f) implies ex x being Element of the carrier of (FAdj (F,{a})) st S1[k,x] )
assume k in Seg (len f) ; :: thesis: ex x being Element of the carrier of (FAdj (F,{a})) st S1[k,x]
then reconsider i = k as Element of dom f by FINSEQ_1:def 3;
f . i is square by REALALG2:def 5;
then consider z being Element of (FAdj (F,{a})) such that
B2: f . i = z ^2 ;
consider c1, c2 being Element of (FAdj (F,{a})) such that
B1: ( c1 in F & c2 in F & z = c1 + ((@ ((FAdj (F,{a})),a)) * c2) ) by AS, XYZb;
reconsider d1 = c1, d2 = c2 as Element of F by B1;
thus ex x being Element of the carrier of (FAdj (F,{a})) st S1[k,x] :: thesis: verum
proof
take c1 ^2 ; :: thesis: S1[k,c1 ^2 ]
thus S1[k,c1 ^2 ] :: thesis: verum
proof
now :: thesis: for x, y being Element of F st f . k = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 holds
c1 ^2 = x ^2
let x, y be Element of F; :: thesis: ( f . k = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 implies c1 ^2 = b1 ^2 )
assume A2: f . k = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 ; :: thesis: c1 ^2 = b1 ^2
A3: ( c1 = @ (d1,(FAdj (F,{a}))) & c2 = @ (d2,(FAdj (F,{a}))) ) by FIELD_7:def 4;
per cases then ( (@ (d1,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (d2,(FAdj (F,{a}))))) = (@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a}))))) or (@ (d1,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (d2,(FAdj (F,{a}))))) = - ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ) by A2, B2, B1, REALALG2:10;
suppose B3: (@ (d1,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (d2,(FAdj (F,{a}))))) = (@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a}))))) ; :: thesis: c1 ^2 = b1 ^2
( @ (d1,(FAdj (F,{a}))) = d1 & @ (d2,(FAdj (F,{a}))) = d2 & @ (x,(FAdj (F,{a}))) = x & @ (y,(FAdj (F,{a}))) = y ) by FIELD_7:def 4;
then ( @ (d1,(FAdj (F,{a}))) in F & @ (d2,(FAdj (F,{a}))) in F & @ (x,(FAdj (F,{a}))) in F & @ (y,(FAdj (F,{a}))) in F ) ;
then @ (d1,(FAdj (F,{a}))) = @ (x,(FAdj (F,{a}))) by AS, B3, XYZc
.= x by FIELD_7:def 4 ;
hence c1 ^2 = x ^2 by A3, H0, FIELD_6:16; :: thesis: verum
end;
suppose (@ (d1,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (d2,(FAdj (F,{a}))))) = - ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ; :: thesis: c1 ^2 = b1 ^2
then B3: (@ (d1,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (d2,(FAdj (F,{a}))))) = (- (@ (x,(FAdj (F,{a}))))) + (- ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) by RLVECT_1:31
.= (- (@ (x,(FAdj (F,{a}))))) + ((@ ((FAdj (F,{a})),a)) * (- (@ (y,(FAdj (F,{a})))))) by VECTSP_1:8 ;
B4: ( @ (d1,(FAdj (F,{a}))) = d1 & @ (d2,(FAdj (F,{a}))) = d2 & - (@ (x,(FAdj (F,{a})))) = - x & - (@ (y,(FAdj (F,{a})))) = - y ) by FIELD_7:def 4, H0, FIELD_6:17;
then ( @ (d1,(FAdj (F,{a}))) in F & @ (d2,(FAdj (F,{a}))) in F & - (@ (x,(FAdj (F,{a})))) in F & - (@ (y,(FAdj (F,{a})))) in F ) ;
then @ (d1,(FAdj (F,{a}))) = - x by B4, AS, B3, XYZc;
hence c1 ^2 = (- x) * (- x) by A3, H0, FIELD_6:16
.= x ^2 by VECTSP_1:10 ;
:: thesis: verum
end;
end;
end;
hence S1[k,c1 ^2 ] ; :: thesis: verum
end;
end;
end;
A2: now :: thesis: for k being Nat st k in Seg (len f) holds
ex x being Element of the carrier of (FAdj (F,{a})) st S2[k,x]
let k be Nat; :: thesis: ( k in Seg (len f) implies ex x being Element of the carrier of (FAdj (F,{a})) st S2[k,x] )
assume k in Seg (len f) ; :: thesis: ex x being Element of the carrier of (FAdj (F,{a})) st S2[k,x]
then reconsider i = k as Element of dom f by FINSEQ_1:def 3;
f . i is square by REALALG2:def 5;
then consider z being Element of (FAdj (F,{a})) such that
B2: f . i = z ^2 ;
consider c1, c2 being Element of (FAdj (F,{a})) such that
B1: ( c1 in F & c2 in F & z = c1 + ((@ ((FAdj (F,{a})),a)) * c2) ) by AS, XYZb;
reconsider d1 = c1, d2 = c2 as Element of F by B1;
thus ex x being Element of the carrier of (FAdj (F,{a})) st S2[k,x] :: thesis: verum
proof
take c2 ^2 ; :: thesis: S2[k,c2 ^2 ]
thus S2[k,c2 ^2 ] :: thesis: verum
proof
now :: thesis: for x, y being Element of F st f . k = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 holds
c2 ^2 = y ^2
let x, y be Element of F; :: thesis: ( f . k = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 implies c2 ^2 = b2 ^2 )
assume A2: f . k = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 ; :: thesis: c2 ^2 = b2 ^2
A3: ( c1 = @ (d1,(FAdj (F,{a}))) & c2 = @ (d2,(FAdj (F,{a}))) ) by FIELD_7:def 4;
per cases then ( (@ (d1,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (d2,(FAdj (F,{a}))))) = (@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a}))))) or (@ (d1,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (d2,(FAdj (F,{a}))))) = - ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ) by A2, B1, B2, REALALG2:10;
suppose B3: (@ (d1,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (d2,(FAdj (F,{a}))))) = (@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a}))))) ; :: thesis: c2 ^2 = b2 ^2
( @ (d1,(FAdj (F,{a}))) = d1 & @ (d2,(FAdj (F,{a}))) = d2 & @ (x,(FAdj (F,{a}))) = x & @ (y,(FAdj (F,{a}))) = y ) by FIELD_7:def 4;
then ( @ (d1,(FAdj (F,{a}))) in F & @ (d2,(FAdj (F,{a}))) in F & @ (x,(FAdj (F,{a}))) in F & @ (y,(FAdj (F,{a}))) in F ) ;
then @ (d2,(FAdj (F,{a}))) = @ (y,(FAdj (F,{a}))) by AS, B3, XYZc
.= y by FIELD_7:def 4 ;
hence c2 ^2 = y ^2 by A3, H0, FIELD_6:16; :: thesis: verum
end;
suppose (@ (d1,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (d2,(FAdj (F,{a}))))) = - ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ; :: thesis: c2 ^2 = b2 ^2
then B3: (@ (d1,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (d2,(FAdj (F,{a}))))) = (- (@ (x,(FAdj (F,{a}))))) + (- ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) by RLVECT_1:31
.= (- (@ (x,(FAdj (F,{a}))))) + ((@ ((FAdj (F,{a})),a)) * (- (@ (y,(FAdj (F,{a})))))) by VECTSP_1:8 ;
B4: ( @ (d1,(FAdj (F,{a}))) = d1 & @ (d2,(FAdj (F,{a}))) = d2 & - (@ (x,(FAdj (F,{a})))) = - x & - (@ (y,(FAdj (F,{a})))) = - y ) by FIELD_7:def 4, H0, FIELD_6:17;
then ( @ (d1,(FAdj (F,{a}))) in F & @ (d2,(FAdj (F,{a}))) in F & - (@ (x,(FAdj (F,{a})))) in F & - (@ (y,(FAdj (F,{a})))) in F ) ;
then @ (d2,(FAdj (F,{a}))) = - y by B4, AS, B3, XYZc;
hence c2 ^2 = (- y) * (- y) by A3, H0, FIELD_6:16
.= y ^2 by VECTSP_1:10 ;
:: thesis: verum
end;
end;
end;
hence S2[k,c2 ^2 ] ; :: thesis: verum
end;
end;
end;
A3: now :: thesis: for k being Nat st k in Seg (len f) holds
ex x being Element of the carrier of (FAdj (F,{a})) st S3[k,x]
let k be Nat; :: thesis: ( k in Seg (len f) implies ex x being Element of the carrier of (FAdj (F,{a})) st S3[k,x] )
assume k in Seg (len f) ; :: thesis: ex x being Element of the carrier of (FAdj (F,{a})) st S3[k,x]
then reconsider i = k as Element of dom f by FINSEQ_1:def 3;
f . i is square by REALALG2:def 5;
then consider z being Element of (FAdj (F,{a})) such that
B2: f . i = z ^2 ;
consider c1, c2 being Element of (FAdj (F,{a})) such that
B1: ( c1 in F & c2 in F & z = c1 + ((@ ((FAdj (F,{a})),a)) * c2) ) by AS, XYZb;
reconsider d1 = c1, d2 = c2 as Element of F by B1;
thus ex x being Element of the carrier of (FAdj (F,{a})) st S3[k,x] :: thesis: verum
proof
take (2 '*' c1) * c2 ; :: thesis: S3[k,(2 '*' c1) * c2]
thus S3[k,(2 '*' c1) * c2] :: thesis: verum
proof
now :: thesis: for x, y being Element of F st f . k = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 holds
(2 '*' c1) * c2 = (2 '*' x) * y
let x, y be Element of F; :: thesis: ( f . k = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 implies (2 '*' c1) * c2 = (2 '*' b1) * b2 )
assume A2: f . k = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 ; :: thesis: (2 '*' c1) * c2 = (2 '*' b1) * b2
A3: ( c1 = @ (d1,(FAdj (F,{a}))) & c2 = @ (d2,(FAdj (F,{a}))) ) by FIELD_7:def 4;
per cases then ( (@ (d1,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (d2,(FAdj (F,{a}))))) = (@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a}))))) or (@ (d1,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (d2,(FAdj (F,{a}))))) = - ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ) by A2, B1, B2, REALALG2:10;
suppose B3: (@ (d1,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (d2,(FAdj (F,{a}))))) = (@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a}))))) ; :: thesis: (2 '*' c1) * c2 = (2 '*' b1) * b2
( @ (d1,(FAdj (F,{a}))) = d1 & @ (d2,(FAdj (F,{a}))) = d2 & @ (x,(FAdj (F,{a}))) = x & @ (y,(FAdj (F,{a}))) = y ) by FIELD_7:def 4;
then B4: ( @ (d1,(FAdj (F,{a}))) in F & @ (d2,(FAdj (F,{a}))) in F & @ (x,(FAdj (F,{a}))) in F & @ (y,(FAdj (F,{a}))) in F ) ;
then B5: @ (d1,(FAdj (F,{a}))) = @ (x,(FAdj (F,{a}))) by AS, B3, XYZc
.= x by FIELD_7:def 4 ;
B6: @ (d2,(FAdj (F,{a}))) = @ (y,(FAdj (F,{a}))) by AS, B3, B4, XYZc
.= y by FIELD_7:def 4 ;
2 '*' c1 = 2 '*' x by A3, B5, FIELD_9:7;
hence (2 '*' c1) * c2 = (2 '*' x) * y by B6, A3, H0, FIELD_6:16; :: thesis: verum
end;
suppose (@ (d1,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (d2,(FAdj (F,{a}))))) = - ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ; :: thesis: (2 '*' c1) * c2 = (2 '*' b1) * b2
then B3: (@ (d1,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (d2,(FAdj (F,{a}))))) = (- (@ (x,(FAdj (F,{a}))))) + (- ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) by RLVECT_1:31
.= (- (@ (x,(FAdj (F,{a}))))) + ((@ ((FAdj (F,{a})),a)) * (- (@ (y,(FAdj (F,{a})))))) by VECTSP_1:8 ;
B4: ( @ (d1,(FAdj (F,{a}))) = d1 & @ (d2,(FAdj (F,{a}))) = d2 & - (@ (x,(FAdj (F,{a})))) = - x & - (@ (y,(FAdj (F,{a})))) = - y ) by FIELD_7:def 4, H0, FIELD_6:17;
then B5: ( @ (d1,(FAdj (F,{a}))) in F & @ (d2,(FAdj (F,{a}))) in F & - (@ (x,(FAdj (F,{a})))) in F & - (@ (y,(FAdj (F,{a})))) in F ) ;
then B6: @ (d1,(FAdj (F,{a}))) = - x by B4, AS, B3, XYZc;
B7: @ (d2,(FAdj (F,{a}))) = - y by B4, AS, B3, B5, XYZc;
2 '*' c1 = 2 '*' (- x) by B4, B6, FIELD_9:7;
then (2 '*' c1) * c2 = (2 '*' (- x)) * (- y) by B4, B7, H0, FIELD_6:16
.= 2 '*' ((- x) * (- y)) by REALALG2:5
.= 2 '*' (x * y) by VECTSP_1:10 ;
hence (2 '*' c1) * c2 = (2 '*' x) * y by REALALG2:5; :: thesis: verum
end;
end;
end;
hence S3[k,(2 '*' c1) * c2] ; :: thesis: verum
end;
end;
end;
consider g1, g2, g3 being FinSequence of the carrier of (FAdj (F,{a})) such that
A4: ( dom g1 = Seg (len f) & dom g2 = Seg (len f) & dom g3 = Seg (len f) & ( for k being Nat st k in Seg (len f) holds
( S1[k,g1 . k] & ( for k being Nat st k in Seg (len f) holds
( S2[k,g2 . k] & ( for k being Nat st k in Seg (len f) holds
S3[k,g3 . k] ) ) ) ) ) ) from REALALG3:sch 1(A1, A2, A3);
 reconsider g1 = g1, g2 = g2, g3 = g3 as non empty FinSequence of (FAdj (F,{a})) by A4;
take g1 ; :: thesis: ex g2, g3 being non empty FinSequence of (FAdj (F,{a})) st
( dom g1 = dom f & dom g2 = dom f & dom g3 = dom f & ( for i being Nat st i in dom f holds
for x, y being Element of F st f . i = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 holds
( g1 . i = x ^2 & g2 . i = y ^2 & g3 . i = (2 '*' x) * y ) ) )
take g2 ; :: thesis: ex g3 being non empty FinSequence of (FAdj (F,{a})) st
( dom g1 = dom f & dom g2 = dom f & dom g3 = dom f & ( for i being Nat st i in dom f holds
for x, y being Element of F st f . i = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 holds
( g1 . i = x ^2 & g2 . i = y ^2 & g3 . i = (2 '*' x) * y ) ) )
take g3 ; :: thesis: ( dom g1 = dom f & dom g2 = dom f & dom g3 = dom f & ( for i being Nat st i in dom f holds
for x, y being Element of F st f . i = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 holds
( g1 . i = x ^2 & g2 . i = y ^2 & g3 . i = (2 '*' x) * y ) ) )
thus ( dom g1 = dom f & dom g2 = dom f & dom g3 = dom f ) by A4, FINSEQ_1:def 3; :: thesis: for i being Nat st i in dom f holds
for x, y being Element of F st f . i = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 holds
( g1 . i = x ^2 & g2 . i = y ^2 & g3 . i = (2 '*' x) * y )
now :: thesis: for k being Nat st k in dom f holds
for x, y being Element of F st f . k = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 holds
( g1 . k = x ^2 & g2 . k = y ^2 & g3 . k = (2 '*' x) * y )
let k be Nat; :: thesis: ( k in dom f implies for x, y being Element of F st f . k = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 holds
( g1 . k = x ^2 & g2 . k = y ^2 & g3 . k = (2 '*' x) * y ) )
assume C: k in dom f ; :: thesis: for x, y being Element of F st f . k = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 holds
( g1 . k = x ^2 & g2 . k = y ^2 & g3 . k = (2 '*' x) * y )
then reconsider i = k as Element of dom f ;
set z = the Element of (FAdj (F,{a}));
consider c1, c2 being Element of (FAdj (F,{a})) such that
B1: ( c1 in F & c2 in F & the Element of (FAdj (F,{a})) = c1 + ((@ ((FAdj (F,{a})),a)) * c2) ) by AS, XYZb;
reconsider d1 = c1, d2 = c2 as Element of F by B1;
thus for x, y being Element of F st f . k = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 holds
( g1 . k = x ^2 & g2 . k = y ^2 & g3 . k = (2 '*' x) * y ) :: thesis: verum
proof
let x, y be Element of F; :: thesis: ( f . k = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 implies ( g1 . k = x ^2 & g2 . k = y ^2 & g3 . k = (2 '*' x) * y ) )
assume B5: f . k = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 ; :: thesis: ( g1 . k = x ^2 & g2 . k = y ^2 & g3 . k = (2 '*' x) * y )
B6: Seg (len f) = dom f by FINSEQ_1:def 3;
hence g1 . k = x ^2 by C, A4, B5; :: thesis: ( g2 . k = y ^2 & g3 . k = (2 '*' x) * y )
thus g2 . k = y ^2 by B6, B5, C, A4; :: thesis: g3 . k = (2 '*' x) * y
thus g3 . k = (2 '*' x) * y by B6, B5, C, A4; :: thesis: verum
end;
end;
hence for i being Nat st i in dom f holds
for x, y being Element of F st f . i = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 holds
( g1 . i = x ^2 & g2 . i = y ^2 & g3 . i = (2 '*' x) * y ) ; :: thesis: verum
end;
then consider g1, g2, g3 being non empty FinSequence of (FAdj (F,{a})) such that
A: ( dom g1 = dom f & dom g2 = dom f & dom g3 = dom f & ( for i being Nat st i in dom f holds
for x, y being Element of F st f . i = ((@ (x,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a})))))) ^2 holds
( g1 . i = x ^2 & g2 . i = y ^2 & g3 . i = (2 '*' x) * y ) ) ) ;
A0: now :: thesis: for k being Nat st k in dom g1 holds
g1 . k in F
let k be Nat; :: thesis: ( k in dom g1 implies g1 . k in F )
assume k in dom g1 ; :: thesis: g1 . k in F
then reconsider i = k as Element of dom f by A;
f . i is square by REALALG2:def 5;
then consider z being Element of (FAdj (F,{a})) such that
B2: f . i = z ^2 ;
consider c1, c2 being Element of (FAdj (F,{a})) such that
B1: ( c1 in F & c2 in F & z = c1 + ((@ ((FAdj (F,{a})),a)) * c2) ) by AS, XYZb;
reconsider d1 = c1, d2 = c2 as Element of F by B1;
( c1 = @ (d1,(FAdj (F,{a}))) & c2 = @ (d2,(FAdj (F,{a}))) ) by FIELD_7:def 4;
then g1 . i = d1 ^2 by A, B1, B2;
hence g1 . k in F ; :: thesis: verum
end;
A1: now :: thesis: for k being Nat st k in dom g1 holds
g2 . k in F
let k be Nat; :: thesis: ( k in dom g1 implies g2 . k in F )
assume k in dom g1 ; :: thesis: g2 . k in F
then reconsider i = k as Element of dom f by A;
f . i is square by REALALG2:def 5;
then consider z being Element of (FAdj (F,{a})) such that
B2: f . i = z ^2 ;
consider c1, c2 being Element of (FAdj (F,{a})) such that
B1: ( c1 in F & c2 in F & z = c1 + ((@ ((FAdj (F,{a})),a)) * c2) ) by AS, XYZb;
reconsider d1 = c1, d2 = c2 as Element of F by B1;
( c1 = @ (d1,(FAdj (F,{a}))) & c2 = @ (d2,(FAdj (F,{a}))) ) by FIELD_7:def 4;
then g2 . i = d2 ^2 by A, B1, B2;
hence g2 . k in F ; :: thesis: verum
end;
now :: thesis: for k being Nat st k in dom g3 holds
g3 . k in F
let k be Nat; :: thesis: ( k in dom g3 implies g3 . k in F )
assume k in dom g3 ; :: thesis: g3 . k in F
then reconsider i = k as Element of dom f by A;
f . i is square by REALALG2:def 5;
then consider z being Element of (FAdj (F,{a})) such that
B2: f . i = z ^2 ;
consider c1, c2 being Element of (FAdj (F,{a})) such that
B1: ( c1 in F & c2 in F & z = c1 + ((@ ((FAdj (F,{a})),a)) * c2) ) by AS, XYZb;
reconsider d1 = c1, d2 = c2 as Element of F by B1;
( c1 = @ (d1,(FAdj (F,{a}))) & c2 = @ (d2,(FAdj (F,{a}))) ) by FIELD_7:def 4;
then g3 . i = (2 '*' d1) * d2 by A, B1, B2;
hence g3 . k in F ; :: thesis: verum
end;
then reconsider d1 = g1, d2 = g2, d3 = g3 as non empty FinSequence of F by A, A1, A0, finex;
A2: now :: thesis: for k being Element of dom d1 holds d1 . k is square
let k be Element of dom d1; :: thesis: d1 . k is square
reconsider i = k as Element of dom f by A;
f . i is square by REALALG2:def 5;
then consider z being Element of (FAdj (F,{a})) such that
B2: f . i = z ^2 ;
consider c1, c2 being Element of (FAdj (F,{a})) such that
B1: ( c1 in F & c2 in F & z = c1 + ((@ ((FAdj (F,{a})),a)) * c2) ) by AS, XYZb;
reconsider x = c1, y = c2 as Element of F by B1;
B3: ( c1 = @ (x,(FAdj (F,{a}))) & c2 = @ (y,(FAdj (F,{a}))) ) by FIELD_7:def 4;
g1 . i = x ^2 by A, B1, B2, B3;
hence d1 . k is square ; :: thesis: verum
end;
now :: thesis: for k being Element of dom d2 holds d2 . k is square
let k be Element of dom d2; :: thesis: d2 . k is square
reconsider i = k as Element of dom f by A;
f . i is square by REALALG2:def 5;
then consider z being Element of (FAdj (F,{a})) such that
B2: f . i = z ^2 ;
consider c1, c2 being Element of (FAdj (F,{a})) such that
B1: ( c1 in F & c2 in F & z = c1 + ((@ ((FAdj (F,{a})),a)) * c2) ) by AS, XYZb;
reconsider x = c1, y = c2 as Element of F by B1;
B3: ( c1 = @ (x,(FAdj (F,{a}))) & c2 = @ (y,(FAdj (F,{a}))) ) by FIELD_7:def 4;
g2 . i = y ^2 by A, B1, B2, B3;
hence d2 . k is square ; :: thesis: verum
end;
then reconsider d1 = d1, d2 = d2 as non empty quadratic FinSequence of F by A2, REALALG2:def 5;
A3: ( dom (g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) = dom g3 & dom (g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) = dom ((@ ((FAdj (F,{a})),a)) * g3) & dom g1 = dom (((@ ((FAdj (F,{a})),a)) ^2) * g2) & dom f = dom ((g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) + ((@ ((FAdj (F,{a})),a)) * g3)) )
proof
thus dom (g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) = dom g3 by A, BINOM:def 1; :: thesis: ( dom (g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) = dom ((@ ((FAdj (F,{a})),a)) * g3) & dom g1 = dom (((@ ((FAdj (F,{a})),a)) ^2) * g2) & dom f = dom ((g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) + ((@ ((FAdj (F,{a})),a)) * g3)) )
hence dom (g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) = dom ((@ ((FAdj (F,{a})),a)) * g3) by POLYNOM1:def 1; :: thesis: ( dom g1 = dom (((@ ((FAdj (F,{a})),a)) ^2) * g2) & dom f = dom ((g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) + ((@ ((FAdj (F,{a})),a)) * g3)) )
thus dom g1 = dom (((@ ((FAdj (F,{a})),a)) ^2) * g2) by POLYNOM1:def 1, A; :: thesis: dom f = dom ((g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) + ((@ ((FAdj (F,{a})),a)) * g3))
dom (g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) = dom g3 by A, BINOM:def 1;
hence dom f = dom ((g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) + ((@ ((FAdj (F,{a})),a)) * g3)) by A, BINOM:def 1; :: thesis: verum
end;
A4: (g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) + ((@ ((FAdj (F,{a})),a)) * g3) = f
proof
set p = (g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) + ((@ ((FAdj (F,{a})),a)) * g3);
A5: ( dom ((g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) + ((@ ((FAdj (F,{a})),a)) * g3)) = Seg (len ((g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) + ((@ ((FAdj (F,{a})),a)) * g3))) & dom f = Seg (len f) ) by FINSEQ_1:def 3;
now :: thesis: for j being Nat st j in dom ((g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) + ((@ ((FAdj (F,{a})),a)) * g3)) holds
((g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) + ((@ ((FAdj (F,{a})),a)) * g3)) . j = f . j
let j be Nat; :: thesis: ( j in dom ((g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) + ((@ ((FAdj (F,{a})),a)) * g3)) implies ((g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) + ((@ ((FAdj (F,{a})),a)) * g3)) . j = f . j )
assume A6: j in dom ((g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) + ((@ ((FAdj (F,{a})),a)) * g3)) ; :: thesis: ((g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) + ((@ ((FAdj (F,{a})),a)) * g3)) . j = f . j
then C: j in Seg (len (g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2))) by A, A3, FINSEQ_1:def 3;
j in Seg (len ((g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) + ((@ ((FAdj (F,{a})),a)) * g3))) by A6, FINSEQ_1:def 3;
then A7: ( 1 <= j & j <= len ((g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) + ((@ ((FAdj (F,{a})),a)) * g3)) & j <= len (g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) ) by C, FINSEQ_1:1;
reconsider i = j as Element of dom f by A6, A3;
f . i is square by REALALG2:def 5;
then consider z being Element of (FAdj (F,{a})) such that
B2: f . i = z ^2 ;
consider c1, c2 being Element of (FAdj (F,{a})) such that
B1: ( c1 in F & c2 in F & z = c1 + ((@ ((FAdj (F,{a})),a)) * c2) ) by AS, XYZb;
reconsider x = c1, y = c2 as Element of F by B1;
B3: ( c1 = @ (x,(FAdj (F,{a}))) & c2 = @ (y,(FAdj (F,{a}))) ) by FIELD_7:def 4;
then A9: ( g1 . j = x ^2 & g2 . j = y ^2 & g3 . j = (2 '*' x) * y ) by B1, B2, A;
A10: ( g1 . j = (@ (x,(FAdj (F,{a})))) ^2 & g2 . j = (@ (y,(FAdj (F,{a})))) ^2 & g3 . j = (2 '*' (@ (x,(FAdj (F,{a}))))) * (@ (y,(FAdj (F,{a})))) )
proof
A11: F is Subring of FAdj (F,{a}) by FIELD_4:def 1;
@ (x,(FAdj (F,{a}))) = x by FIELD_7:def 4;
hence g1 . j = (@ (x,(FAdj (F,{a})))) ^2 by A9, A11, FIELD_6:16; :: thesis: ( g2 . j = (@ (y,(FAdj (F,{a})))) ^2 & g3 . j = (2 '*' (@ (x,(FAdj (F,{a}))))) * (@ (y,(FAdj (F,{a})))) )
A13: @ (y,(FAdj (F,{a}))) = y by FIELD_7:def 4;
hence g2 . j = (@ (y,(FAdj (F,{a})))) ^2 by A9, A11, FIELD_6:16; :: thesis: g3 . j = (2 '*' (@ (x,(FAdj (F,{a}))))) * (@ (y,(FAdj (F,{a}))))
2 '*' (@ (x,(FAdj (F,{a})))) = 2 '*' x by FIELD_7:def 4, FIELD_9:7;
hence g3 . j = (2 '*' (@ (x,(FAdj (F,{a}))))) * (@ (y,(FAdj (F,{a})))) by A13, A11, A9, FIELD_6:16; :: thesis: verum
end;
thus ((g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) + ((@ ((FAdj (F,{a})),a)) * g3)) . j = ((g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) + ((@ ((FAdj (F,{a})),a)) * g3)) /. j by A6, PARTFUN1:def 6
.= ((g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) /. j) + (((@ ((FAdj (F,{a})),a)) * g3) /. j) by A7, BINOM:def 1
.= ((g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) /. j) + ((@ ((FAdj (F,{a})),a)) * (g3 /. j)) by A6, A3, A, POLYNOM1:def 1
.= ((g1 /. j) + ((((@ ((FAdj (F,{a})),a)) ^2) * g2) /. j)) + ((@ ((FAdj (F,{a})),a)) * (g3 /. j)) by A7, BINOM:def 1
.= ((g1 /. j) + (((@ ((FAdj (F,{a})),a)) ^2) * (g2 /. j))) + ((@ ((FAdj (F,{a})),a)) * (g3 /. j)) by A6, A3, A, POLYNOM1:def 1
.= (((@ (x,(FAdj (F,{a})))) ^2) + (((@ ((FAdj (F,{a})),a)) ^2) * (g2 /. j))) + ((@ ((FAdj (F,{a})),a)) * (g3 /. j)) by A10, A6, A3, A, PARTFUN1:def 6
.= (((@ (x,(FAdj (F,{a})))) ^2) + (((@ ((FAdj (F,{a})),a)) ^2) * ((@ (y,(FAdj (F,{a})))) ^2))) + ((@ ((FAdj (F,{a})),a)) * (g3 /. j)) by A10, A6, A3, A, PARTFUN1:def 6
.= (((@ (x,(FAdj (F,{a})))) ^2) + (((@ ((FAdj (F,{a})),a)) ^2) * ((@ (y,(FAdj (F,{a})))) ^2))) + ((@ ((FAdj (F,{a})),a)) * ((2 '*' (@ (x,(FAdj (F,{a}))))) * (@ (y,(FAdj (F,{a})))))) by A10, A6, A3, A, PARTFUN1:def 6
.= ((@ (x,(FAdj (F,{a})))) ^2) + (((@ ((FAdj (F,{a})),a)) * ((2 '*' (@ (x,(FAdj (F,{a}))))) * (@ (y,(FAdj (F,{a})))))) + (((@ ((FAdj (F,{a})),a)) ^2) * ((@ (y,(FAdj (F,{a})))) ^2))) by RLVECT_1:def 3
.= ((@ (x,(FAdj (F,{a})))) ^2) + (((@ ((FAdj (F,{a})),a)) * ((2 '*' (@ (x,(FAdj (F,{a}))))) * (@ (y,(FAdj (F,{a})))))) + (((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a}))))) ^2)) by FIELD_9:2
.= ((@ (x,(FAdj (F,{a})))) ^2) + (((2 '*' (@ (x,(FAdj (F,{a}))))) * ((@ (y,(FAdj (F,{a})))) * (@ ((FAdj (F,{a})),a)))) + (((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a}))))) ^2)) by GROUP_1:def 3
.= (((@ (x,(FAdj (F,{a})))) ^2) + ((2 '*' (@ (x,(FAdj (F,{a}))))) * ((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a}))))))) + (((@ ((FAdj (F,{a})),a)) * (@ (y,(FAdj (F,{a}))))) ^2) by RLVECT_1:def 3
.= f . j by B1, B2, B3, REALALG2:7 ; :: thesis: verum
end;
hence (g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2)) + ((@ ((FAdj (F,{a})),a)) * g3) = f by A5, A3, FINSEQ_1:6, FINSEQ_2:9; :: thesis: verum
end;
take g1 ; :: thesis: ex g2, g3 being non empty FinSequence of (FAdj (F,{a})) st
( g1 is non empty quadratic FinSequence of F & g2 is non empty quadratic FinSequence of F & g3 is non empty FinSequence of F & Sum f = ((Sum g1) + (((@ ((FAdj (F,{a})),a)) ^2) * (Sum g2))) + ((@ ((FAdj (F,{a})),a)) * (Sum g3)) )
take g2 ; :: thesis: ex g3 being non empty FinSequence of (FAdj (F,{a})) st
( g1 is non empty quadratic FinSequence of F & g2 is non empty quadratic FinSequence of F & g3 is non empty FinSequence of F & Sum f = ((Sum g1) + (((@ ((FAdj (F,{a})),a)) ^2) * (Sum g2))) + ((@ ((FAdj (F,{a})),a)) * (Sum g3)) )
take g3 ; :: thesis: ( g1 is non empty quadratic FinSequence of F & g2 is non empty quadratic FinSequence of F & g3 is non empty FinSequence of F & Sum f = ((Sum g1) + (((@ ((FAdj (F,{a})),a)) ^2) * (Sum g2))) + ((@ ((FAdj (F,{a})),a)) * (Sum g3)) )
( g1 = d1 & g2 = d2 & g3 = d3 ) ;
hence ( g1 is non empty quadratic FinSequence of F & g2 is non empty quadratic FinSequence of F & g3 is non empty FinSequence of F ) ; :: thesis: Sum f = ((Sum g1) + (((@ ((FAdj (F,{a})),a)) ^2) * (Sum g2))) + ((@ ((FAdj (F,{a})),a)) * (Sum g3))
Sum f = (Sum (g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2))) + (Sum ((@ ((FAdj (F,{a})),a)) * g3)) by A3, A4, BINOM:7
.= (Sum (g1 + (((@ ((FAdj (F,{a})),a)) ^2) * g2))) + ((@ ((FAdj (F,{a})),a)) * (Sum g3)) by BINOM:4
.= ((Sum g1) + (Sum (((@ ((FAdj (F,{a})),a)) ^2) * g2))) + ((@ ((FAdj (F,{a})),a)) * (Sum g3)) by A3, BINOM:7
.= ((Sum g1) + (((@ ((FAdj (F,{a})),a)) ^2) * (Sum g2))) + ((@ ((FAdj (F,{a})),a)) * (Sum g3)) by BINOM:4 ;
hence Sum f = ((Sum g1) + (((@ ((FAdj (F,{a})),a)) ^2) * (Sum g2))) + ((@ ((FAdj (F,{a})),a)) * (Sum g3)) ; :: thesis: verum