let F be Field; :: thesis: ( F is formally_real iff for f being non empty quadratic FinSequence of F st Sum f = 0. F holds
f is trivial )
hereby :: thesis: ( ( for f being non empty quadratic FinSequence of F st Sum f = 0. F holds
f is trivial ) implies F is formally_real )
assume AS: F is formally_real ; :: thesis: for f being non empty quadratic FinSequence of F st Sum f = 0. F holds
f is trivial
now :: thesis: for f being non empty quadratic FinSequence of F st Sum f = 0. F holds
f is trivial
assume ex f being non empty quadratic FinSequence of F st
( Sum f = 0. F & not f is trivial ) ; :: thesis: contradiction
then consider f being non empty quadratic FinSequence of F such that
H1: ( Sum f = 0. F & not f is trivial ) ;
consider i being Element of dom f such that
H2: f . i <> 0. F by H1;
H7: len (Swap (f,i,(len f))) = len f by FINSEQ_7:18;
then reconsider g = Swap (f,i,(len f)) as non empty FinSequence of F ;
reconsider m = (len f) - 1 as Nat ;
reconsider p = g | (Seg m) as FinSequence of F by FINSEQ_1:18;
p ^ <*(f . i)*> = g
proof
m + 1 = len g by FINSEQ_7:18;
then m <= len g by NAT_1:13;
then X2: ( len p = m & dom p = Seg m ) by FINSEQ_1:17;
X1: len (p ^ <*(f . i)*>) = (len p) + (len <*(f . i)*>) by FINSEQ_1:22
.= m + 1 by X2, FINSEQ_1:40
.= len g by FINSEQ_7:18 ;
now :: thesis: for k being Nat st 1 <= k & k <= len g holds
(p ^ <*(f . i)*>) . k = g . k
let k be Nat; :: thesis: ( 1 <= k & k <= len g implies (p ^ <*(f . i)*>) . b1 = g . b1 )
assume X3: ( 1 <= k & k <= len g ) ; :: thesis: (p ^ <*(f . i)*>) . b1 = g . b1
per cases then ( k = len g or k < len g ) by XXREAL_0:1;
suppose X4: k = len g ; :: thesis: (p ^ <*(f . i)*>) . b1 = g . b1
then (len p) + 1 = k by X2, FINSEQ_7:18;
then X5: len p < k by NAT_1:13;
X7: ( 1 <= i & i <= len f & 1 <= len f ) by FINSEQ_1:20, FINSEQ_3:25;
thus (p ^ <*(f . i)*>) . k = <*(f . i)*> . (k - (len p)) by X1, X4, X5, FINSEQ_1:24
.= f . i by X2, X4, H7, FINSEQ_1:40
.= f /. i by X7, FINSEQ_4:15
.= g /. (len f) by X7, FINSEQ_7:31
.= g . k by X7, X4, H7, FINSEQ_4:15 ; :: thesis: verum
end;
suppose k < len g ; :: thesis: (p ^ <*(f . i)*>) . b1 = g . b1
then k + 1 <= len g by NAT_1:13;
then (k + 1) - 1 <= (len g) - 1 by XREAL_1:9;
then X4: k <= m by FINSEQ_7:18;
then k in dom p by X2, X3, FINSEQ_1:1;
hence (p ^ <*(f . i)*>) . k = p . k by FINSEQ_1:def 7
.= g . k by X2, X3, X4, FUNCT_1:47, FINSEQ_1:1 ;
:: thesis: verum
end;
end;
end;
hence p ^ <*(f . i)*> = g by X1, FINSEQ_1:14; :: thesis: verum
end;
then (Sum p) + (Sum <*(f . i)*>) = Sum g by RLVECT_1:41
.= 0. F by H1, GROEB_2:2 ;
then H4: (Sum p) * ((Sum <*(f . i)*>) ") = (- (Sum <*(f . i)*>)) * ((Sum <*(f . i)*>) ") by RLVECT_1:6
.= - ((Sum <*(f . i)*>) * ((Sum <*(f . i)*>) ")) by VECTSP_1:9
.= - ((Sum <*(f . i)*>) * ((f . i) ")) by RLVECT_1:44
.= - ((f . i) * ((f . i) ")) by RLVECT_1:44
.= - (1. F) by H2, VECTSP_1:def 10 ;
H5: Sum p in QS F
proof
now :: thesis: for j being Nat st j in dom p holds
ex a being Element of F st p . j = a ^2
let j be Nat; :: thesis: ( j in dom p implies ex a being Element of F st p . j = a ^2 )
assume I0: j in dom p ; :: thesis: ex a being Element of F st p . j = a ^2
ex k being Element of dom f st p . j = f . k
proof
I2: dom p c= dom g by RELAT_1:60;
p . j = g . j by I0, FUNCT_1:47;
then I1: p . j in rng g by I0, I2, FUNCT_1:def 3;
p . j in rng f by I1, FINSEQ_7:22;
then ex x being object st
( x in dom f & p . j = f . x ) by FUNCT_1:def 3;
hence ex k being Element of dom f st p . j = f . k ; :: thesis: verum
end;
then consider k being Element of dom f such that
I1: p . j = f . k ;
f . k is square by dq;
hence ex a being Element of F st p . j = a ^2 by I1; :: thesis: verum
end;
then Sum p is sum_of_squares ;
hence Sum p in QS F ; :: thesis: verum
end;
H6: (Sum <*(f . i)*>) " in QS F
proof
f . i is square by dq;
then consider a being Element of F such that
I1: f . i = a ^2 ;
I0: a <> 0. F by I1, H2;
(a ") |^ 2 = (a ") * (a ") by RING_5:3
.= (f . i) " by I1, VECTSP_2:11, I0 ;
then (f . i) " in QS F ;
hence (Sum <*(f . i)*>) " in QS F by RLVECT_1:44; :: thesis: verum
end;
QS F is mult-closed ;
hence contradiction by AS, H4, H5, H6; :: thesis: verum
end;
hence for f being non empty quadratic FinSequence of F st Sum f = 0. F holds
f is trivial ; :: thesis: verum
end;
assume AS: for f being non empty quadratic FinSequence of F st Sum f = 0. F holds
f is trivial ; :: thesis: F is formally_real
now :: thesis: not - (1. F) in QS F
assume - (1. F) in QS F ; :: thesis: contradiction
then consider e being Element of F such that
H1: ( e = - (1. F) & e is sum_of_squares ) ;
consider f being FinSequence of F such that
H2: ( Sum f = - (1. F) & ( for i being Nat st i in dom f holds
ex a being Element of F st f . i = a ^2 ) ) by H1;
set g = f ^ <*(1. F)*>;
H3: Sum (f ^ <*(1. F)*>) = (Sum f) + (Sum <*(1. F)*>) by RLVECT_1:41
.= (- (1. F)) + (1. F) by H2, RLVECT_1:44
.= 0. F by RLVECT_1:5 ;
H5b: len (f ^ <*(1. F)*>) = (len f) + (len <*(1. F)*>) by FINSEQ_1:22
.= (len f) + 1 by FINSEQ_1:39 ;
then len f < len (f ^ <*(1. F)*>) by NAT_1:19;
then H5: (f ^ <*(1. F)*>) . (len (f ^ <*(1. F)*>)) = <*(1. F)*> . ((len (f ^ <*(1. F)*>)) - (len f)) by FINSEQ_1:24
.= 1. F by H5b, FINSEQ_1:40 ;
H5a: 1 <= len (f ^ <*(1. F)*>) by H5b, NAT_1:11;
H4: f ^ <*(1. F)*> is quadratic
proof
now :: thesis: for i being Element of dom (f ^ <*(1. F)*>) holds (f ^ <*(1. F)*>) . i is square
let i be Element of dom (f ^ <*(1. F)*>); :: thesis: (f ^ <*(1. F)*>) . b1 is square
I1: ( 1 <= i & i <= len (f ^ <*(1. F)*>) ) by FINSEQ_3:25;
per cases ( i = len (f ^ <*(1. F)*>) or i <> len (f ^ <*(1. F)*>) ) ;
suppose i = len (f ^ <*(1. F)*>) ; :: thesis: (f ^ <*(1. F)*>) . b1 is square
hence (f ^ <*(1. F)*>) . i is square by H5; :: thesis: verum
end;
end;
end;
hence f ^ <*(1. F)*> is quadratic ; :: thesis: verum
end;
not f ^ <*(1. F)*> is trivial by H5, H5a, FINSEQ_3:25;
hence contradiction by H3, H4, AS; :: thesis: verum
end;
hence F is formally_real ; :: thesis: verum