let F be Field; :: thesis: for E being F -finite FieldExtension of F
for K being F -extending b₁ -finite FieldExtension of F
for BE being Basis of (VecSp (E,F))
for BK being Basis of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK) holds Sum l = Sum (down l)
let E be F -finite FieldExtension of F; :: thesis: for K being F -extending E -finite FieldExtension of F
for BE being Basis of (VecSp (E,F))
for BK being Basis of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK) holds Sum l = Sum (down l)
let K be F -extending E -finite FieldExtension of F; :: thesis: for BE being Basis of (VecSp (E,F))
for BK being Basis of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK) holds Sum l = Sum (down l)
let BE be Basis of (VecSp (E,F)); :: thesis: for BK being Basis of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK) holds Sum l = Sum (down l)
let BK be Basis of (VecSp (K,E)); :: thesis: for l being Linear_Combination of Base (BE,BK) holds Sum l = Sum (down l)
let l be Linear_Combination of Base (BE,BK); :: thesis: Sum l = Sum (down l)
defpred S₁[ Nat] means for l being Linear_Combination of Base (BE,BK) st card (Carrier l) = $1 holds
Sum l = Sum (down l);
IA: S₁[ 0 ]

proof

now :: thesis: for l being Linear_Combination of Base (BE,BK) st card (Carrier l) = 0 holds
Sum l = Sum (down l)

let l be Linear_Combination of Base (BE,BK); :: thesis: ( card (Carrier l) = 0 implies Sum l = Sum (down l) )
assume A: card (Carrier l) = 0 ; :: thesis: Sum l = Sum (down l)
then Carrier l = {} ;
then A0: Sum l = 0. (VecSp (K,F)) by VECTSP_6:19
.= 0. K by FIELD_4:def 6 ;

A1: now :: thesis: for b being Element of K holds Sum (down (l,b)) = 0. E

let b be Element of K; :: thesis: Sum (down (l,b)) = 0. E

now :: thesis: for o being object holds not o in Carrier (down (l,b))

let o be object ; :: thesis: not o in Carrier (down (l,b))
assume B2: o in Carrier (down (l,b)) ; :: thesis: contradiction
reconsider a = o as Element of E by B2, FIELD_4:def 6;
reconsider abV = (@ (a,K)) * b as Element of (VecSp (K,F)) by FIELD_4:def 6;
B3: (down (l,b)) . a <> 0. F by B2, VECTSP_6:2;
then ( a in BE & b in BK ) by down1;
then (down (l,b)) . a = l . ((@ (a,K)) * b) by down1;
then abV in Carrier l by B3, VECTSP_6:2;
hence contradiction by A; :: thesis: verum

end;

then Carrier (down (l,b)) = {} by XBOOLE_0:def 1;
hence Sum (down (l,b)) = 0. (VecSp (E,F)) by VECTSP_6:19
.= 0. E by FIELD_4:def 6 ;
:: thesis: verum

end;

A2: for b being Element of K holds (down l) . b = 0. E

proof

let b be Element of K; :: thesis: (down l) . b = 0. E

per cases ( b in BK or not b in BK ) ;

suppose b in BK ; :: thesis: (down l) . b = 0. E

hence (down l) . b = Sum (down (l,b)) by down2
.= 0. E by A1 ;
:: thesis: verum

end;

suppose B0: not b in BK ; :: thesis: (down l) . b = 0. E

B1: Carrier (down l) c= BK by VECTSP_6:def 4;
reconsider bV = b as Element of (VecSp (K,E)) by FIELD_4:def 6;
thus (down l) . b = (down l) . bV
.= 0. E by B0, B1, VECTSP_6:2 ; :: thesis: verum

end;

end;

end;

now :: thesis: for o being object holds not o in Carrier (down l)

let o be object ; :: thesis: not o in Carrier (down l)
assume B0: o in Carrier (down l) ; :: thesis: contradiction
reconsider bV = o as Element of (VecSp (K,E)) by B0;
reconsider b = o as Element of K by B0, FIELD_4:def 6;
(down l) . b <> 0. E by B0, VECTSP_6:2;
hence contradiction by A2; :: thesis: verum

end;

then Carrier (down l) = {} by XBOOLE_0:def 1;
then Sum (down l) = 0. (VecSp (K,E)) by VECTSP_6:19
.= 0. K by FIELD_4:def 6 ;
hence Sum l = Sum (down l) by A0; :: thesis: verum

end;

hence S₁[ 0 ] ; :: thesis: verum

end;

H1: ( the carrier of (VecSp (E,F)) = the carrier of E & the carrier of (VecSp (K,E)) = the carrier of K & the carrier of (VecSp (K,F)) = the carrier of K ) by FIELD_4:def 6;
( E is Subring of K & F is Subring of E ) by FIELD_4:def 1;
then H3: ( the carrier of E c= the carrier of K & the carrier of F c= the carrier of E ) by C0SP1:def 3;

IS: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for l being Linear_Combination of Base (BE,BK) st card (Carrier l) = k + 1 holds
Sum l = Sum (down l)

let l be Linear_Combination of Base (BE,BK); :: thesis: ( card (Carrier l) = k + 1 implies Sum l = Sum (down l) )
assume A0: card (Carrier l) = k + 1 ; :: thesis: Sum l = Sum (down l)
then A1: Carrier l <> {} ;
set o = the Element of Carrier l;
A2: the Element of Carrier l in Carrier l by A1;
A6: Carrier l c= Base (BE,BK) by VECTSP_6:def 4;
then A3: the Element of Carrier l in Base (BE,BK) by A1;
then consider a, b being Element of K such that
A4: ( the Element of Carrier l = a * b & a in BE & b in BK ) ;
reconsider abv = a * b as Element of (VecSp (K,F)) by FIELD_4:def 6;
defpred S₂[ Element of K, Element of F] means ( ( $1 = a * b & $2 = l . (a * b) ) or ( $1 <> a * b & $2 = 0. F ) );

G0: now :: thesis: for x being Element of K ex y being Element of F st S₂[x,y]

let x be Element of K; :: thesis: ex y being Element of F st S₂[y,b₂]

per cases ( x = a * b or x <> a * b ) ;

suppose G: x = a * b ; :: thesis: ex y being Element of F st S₂[y,b₂]

l . (a * b) in the carrier of F by H1, FUNCT_2:5;
hence ex y being Element of F st S₂[x,y] by G; :: thesis: verum

end;

suppose x <> a * b ; :: thesis: ex y being Element of F st S₂[y,b₂]

hence ex y being Element of F st S₂[x,y] ; :: thesis: verum

end;

end;

end;

consider f being Function of the carrier of K, the carrier of F such that
G1: for x being Element of K holds S₂[x,f . x] from FUNCT_2:sch 3(G0);
( dom f = the carrier of (VecSp (K,F)) & rng f c= the carrier of F ) by H1, FUNCT_2:def 1;
then reconsider f = f as Element of Funcs ( the carrier of (VecSp (K,F)), the carrier of F) by FUNCT_2:def 2;

now :: thesis: for v being Element of (VecSp (K,F)) st not v in Base (BE,BK) holds
f . v = 0. F

let v be Element of (VecSp (K,F)); :: thesis: ( not v in Base (BE,BK) implies f . v = 0. F )
assume not v in Base (BE,BK) ; :: thesis: f . v = 0. F
then v <> a * b by A4;
hence f . v = 0. F by H1, G1; :: thesis: verum

end;

then reconsider h = f as Linear_Combination of VecSp (K,F) by VECTSP_6:def 1;

Z: now :: thesis: for o being object st o in Carrier h holds
o in {abv}

let o be object ; :: thesis: ( o in Carrier h implies o in {abv} )
assume C1: o in Carrier h ; :: thesis: o in {abv}
then reconsider v = o as Element of (VecSp (K,F)) ;
reconsider x = v as Element of K by FIELD_4:def 6;
h . x <> 0. F by C1, VECTSP_6:2;
then v = a * b by G1;
hence o in {abv} by TARSKI:def 1; :: thesis: verum

end;

then Carrier h c= {abv} ;
then Y: h is Linear_Combination of {abv} by VECTSP_6:def 4;
{abv} c= Base (BE,BK) by A3, A4, TARSKI:def 1;
then reconsider h = h as Linear_Combination of Base (BE,BK) by Y, VECTSP_6:4;
Carrier h = {abv}

proof

now :: thesis: for o being object st o in {abv} holds
o in Carrier h

let o be object ; :: thesis: ( o in {abv} implies o in Carrier h )
assume o in {abv} ; :: thesis: o in Carrier h
then B2: o = abv by TARSKI:def 1;
h . abv = l . (a * b) by G1;
then h . abv <> 0. F by A1, A4, VECTSP_6:2;
hence o in Carrier h by B2, VECTSP_6:2; :: thesis: verum

end;

hence Carrier h = {abv} by Z, TARSKI:2; :: thesis: verum

end;

then A12: card (Carrier h) = 1 by CARD_2:42;
l . (a * b) is Element of the carrier of F by H1, FUNCT_2:5;
then reconsider lab = l . (a * b) as Element of K by H3;
reconsider labF = l . (a * b) as Element of F by H1, FUNCT_2:5;
set li = l - h;
(l - h) - (l - h) = ZeroLC (VecSp (K,F)) by VECTSP_6:43;
then B: l = ((l - h) - (l - h)) + l by VECTSP_6:27
.= ((l - h) + (- (l - h))) + l by VECTSP_6:def 11
.= ((l - h) + (- (l + (- h)))) + l by VECTSP_6:def 11
.= (l - h) + ((- (l + (- h))) + l) by VECTSP_6:26
.= (l - h) + (((- (1. F)) * (l + (- h))) + l) by VECTSP_6:def 10
.= (l - h) + ((((- (1. F)) * l) + ((- (1. F)) * (- h))) + l) by VECTSP_6:33
.= (l - h) + ((((- (1. F)) * l) + ((- (1. F)) * ((- (1. F)) * h))) + l) by VECTSP_6:def 10
.= (l - h) + ((((- (1. F)) * l) + (((- (1. F)) * (- (1. F))) * h)) + l) by VECTSP_6:34
.= (l - h) + ((((- (1. F)) * l) + (((1. F) * (1. F)) * h)) + l) by VECTSP_1:10
.= (l - h) + ((((- (1. F)) * l) + h) + l) by VECTSP_6:35
.= (l - h) + (((- l) + h) + l) by VECTSP_6:def 10
.= (l - h) + ((h + (- l)) + l) by VECTSP_6:25
.= (l - h) + (h + ((- l) + l)) by VECTSP_6:26
.= (l - h) + (h + (l + (- l))) by VECTSP_6:25
.= (l - h) + (h + (l - l)) by VECTSP_6:def 11
.= (l - h) + (h + (ZeroLC (VecSp (K,F)))) by VECTSP_6:43
.= (l - h) + h by VECTSP_6:27 ;
A8: (l - h) . (a * b) = (l . abv) - (h . abv) by VECTSP_6:40
.= labF + (- labF) by G1
.= 0. F by RLVECT_1:5 ;
A9: for x being Element of K st x <> a * b holds
(l - h) . x = l . x

proof

let x be Element of K; :: thesis: ( x <> a * b implies (l - h) . x = l . x )
reconsider v = x as Element of (VecSp (K,F)) by FIELD_4:def 6;
assume x <> a * b ; :: thesis: (l - h) . x = l . x
then not v in {abv} by TARSKI:def 1;
then h . v = 0. F by Z, VECTSP_6:1;
then (l - h) . v = (l . v) - (0. F) by VECTSP_6:40;
hence (l - h) . x = l . x ; :: thesis: verum

end;

A10: now :: thesis: for o being object st o in Carrier (l - h) holds
o in Carrier l

let o be object ; :: thesis: ( o in Carrier (l - h) implies o in Carrier l )
assume B0: o in Carrier (l - h) ; :: thesis: o in Carrier l
then reconsider v = o as Element of (VecSp (K,F)) ;
reconsider vK = v as Element of K by FIELD_4:def 6;
B1: (l - h) . v <> 0. F by B0, VECTSP_6:2;
then (l - h) . vK = l . vK by A9, A8;
hence o in Carrier l by B1, VECTSP_6:2; :: thesis: verum

end;

then Carrier (l - h) c= Base (BE,BK) by A6;
then reconsider li = l - h as Linear_Combination of Base (BE,BK) by VECTSP_6:def 4;
A11: not a * b in Carrier li by A8, VECTSP_6:2;
Carrier l = (Carrier li) \/ {(a * b)}

proof

B1: now :: thesis: for o being object st o in Carrier l holds
o in (Carrier li) \/ {(a * b)}

let o be object ; :: thesis: ( o in Carrier l implies b₁ in (Carrier li) \/ {(a * b)} )
assume B2: o in Carrier l ; :: thesis: b₁ in (Carrier li) \/ {(a * b)}
then reconsider ab = o as Element of K by FIELD_4:def 6;
reconsider abV = ab as Element of (VecSp (K,F)) by FIELD_4:def 6;

per cases ( o = a * b or o <> a * b ) ;

suppose o = a * b ; :: thesis: b₁ in (Carrier li) \/ {(a * b)}

then o in {(a * b)} by TARSKI:def 1;
hence o in (Carrier li) \/ {(a * b)} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose o <> a * b ; :: thesis: b₁ in (Carrier li) \/ {(a * b)}

then l . ab = li . ab by A9;
then li . ab <> 0. F by B2, VECTSP_6:2;
then abV in Carrier li by VECTSP_6:2;
hence o in (Carrier li) \/ {(a * b)} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

now :: thesis: for o being object st o in (Carrier li) \/ {(a * b)} holds
o in Carrier l

let o be object ; :: thesis: ( o in (Carrier li) \/ {(a * b)} implies b₁ in Carrier l )
assume o in (Carrier li) \/ {(a * b)} ; :: thesis: b₁ in Carrier l

per cases then ( o in Carrier li or o in {(a * b)} ) by XBOOLE_0:def 3;

suppose o in Carrier li ; :: thesis: b₁ in Carrier l

hence o in Carrier l by A10; :: thesis: verum

end;

suppose o in {(a * b)} ; :: thesis: b₁ in Carrier l

hence o in Carrier l by A2, A4, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence Carrier l = (Carrier li) \/ {(a * b)} by B1, TARSKI:2; :: thesis: verum

end;

then (card (Carrier li)) + 1 = k + 1 by A0, A11, CARD_2:41;
then G2: Sum li = Sum (down li) by IV;
G3: Sum h = Sum (down h) by A12, LSum2;
G4a: [(h . abv),abv] in [: the carrier of F, the carrier of K:] by ZFMISC_1:def 2;
G4: Sum h = (h . abv) * abv by Y, VECTSP_6:17
.= ( the multF of K | [: the carrier of F, the carrier of K:]) . [(h . abv),abv] by FIELD_4:def 6
.= the multF of K . [(h . abv),abv] by G4a, FUNCT_1:49
.= lab * (a * b) by G1 ;
G5: down l = (down li) + (down h) by B, LSum1;
reconsider Sdli = Sum (down li) as Element of K by FIELD_4:def 6;
G6: Sdli + (lab * (a * b)) = (Sum (down li)) + (Sum (down h)) by G3, G4, FIELD_4:def 6
.= Sum (down l) by G5, VECTSP_6:44 ;
thus Sum l = (Sum li) + (Sum h) by B, VECTSP_6:44
.= Sum (down l) by G6, G4, G2, FIELD_4:def 6 ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
consider n being Nat such that
H: card (Carrier l) = n ;
thus Sum l = Sum (down l) by I, H; :: thesis: verum