let F be Field; :: thesis:
let E be FieldExtension of F; :: thesis:
let K be F -extending FieldExtension of F; :: thesis:
let BE be non empty finite linearly-independent Subset of (VecSp (E,F)); :: thesis:
let BK be non empty finite linearly-independent Subset of (VecSp (K,E)); :: thesis:
let l be Linear_Combination of Base (BE,BK); :: thesis:
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;
H2: ( 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;
assume card (Carrier l) = 1 ; :: thesis:
then consider o being object such that
D1: Carrier l = {o} by CARD_2:42;
D2: o in Carrier l by D1, TARSKI:def 1;
then reconsider v = o as Element of (VecSp (K,F)) ;
Carrier l c= Base (BE,BK) by VECTSP_6:def 4;
then o in Base (BE,BK) by D2;
then consider a, b being Element of K such that
D3: ( o = a * b & a in BE & b in BK ) ;
reconsider vab = a * b as Element of (VecSp (K,F)) by D2, D3;
reconsider vb = b as Element of (VecSp (K,E)) by FIELD_4:def 6;
reconsider va = a as Element of (VecSp (E,F)) by D3;
reconsider aE = va as Element of E by FIELD_4:def 6;
a * b is Element of (VecSp (K,F)) by FIELD_4:def 6;
then B0: l . (a * b) is Element of F by FUNCT_2:5;
then reconsider labE = l . (a * b) as Element of E by H3;
reconsider lab = l . (a * b) as Element of K by B0, H3;
{va} c= BE by D3, TARSKI:def 1;
then a <> 0. (VecSp (E,F)) by VECTSP_7:3, VECTSP_7:1;
then D7a: a <> 0. E by FIELD_4:def 6;
{vb} c= BK by D3, TARSKI:def 1;
then b <> 0. (VecSp (K,E)) by VECTSP_7:3, VECTSP_7:1;
then D6a: b <> 0. K by FIELD_4:def 6;
D6: Carrier (down (l,b)) = {a}

proof

C1: now :: thesis:

let u be object ; :: thesis:
assume u in {a} ; :: thesis:
then C2: u = a by TARSKI:def 1;
C3: (down (l,b)) . a = l . v by D3, down1;
(down (l,b)) . va <> 0. F by C3, D2, VECTSP_6:2;
hence u in Carrier (down (l,b)) by C2, VECTSP_6:2; :: thesis:

end;

now :: thesis:

let u be object ; :: thesis:
assume C2: u in Carrier (down (l,b)) ; :: thesis:
then reconsider aE = u as Element of E by FIELD_4:def 6;
reconsider aK = aE as Element of K by H3;
reconsider abV = aK * b as Element of (VecSp (K,F)) by FIELD_4:def 6;
C3: (down (l,b)) . aE <> 0. F by C2, VECTSP_6:2;
then ( aE in BE & b in BK ) by down1;
then (down (l,b)) . aK = l . (aK * b) by down1;
then abV in Carrier l by C3, VECTSP_6:2;
then aK * b = a * b by D1, D3, TARSKI:def 1
.= b * a by GROUP_1:def 12 ;
then b * aK = b * a by GROUP_1:def 12;
then aK = a by D6a, VECTSP_2:8;
hence u in {a} by TARSKI:def 1; :: thesis:

end;

hence Carrier (down (l,b)) = {a} by C1, TARSKI:2; :: thesis:

end;

then D7: Sum (down (l,b)) = ((down (l,b)) . va) * va by VECTSP_6:20;
D9: ( (down (l,b)) . a = l . (a * b) & l . (a * b) = l . v ) by D3, down1;
then (down (l,b)) . va <> 0. F by D2, VECTSP_6:2;
then D8: labE <> 0. E by D9, H2, C0SP1:def 3;
D10a: for b1 being Element of K st b1 in BK & b1 <> b holds
Carrier (down (l,b1)) = {}

proof

let b1 be Element of K; :: thesis:
assume E0: ( b1 in BK & b1 <> b ) ; :: thesis:

now :: thesis:

let o be object ; :: thesis:
assume E1: o in Carrier (down (l,b1)) ; :: thesis:
E2: Carrier (down (l,b1)) c= BE by VECTSP_6:def 4;
reconsider v = o as Element of (VecSp (E,F)) by E1;
reconsider vE = v as Element of E by FIELD_4:def 6;
reconsider vb1 = (@ (vE,K)) * b1 as Element of (VecSp (K,F)) by FIELD_4:def 6;
E3: (down (l,b1)) . v = l . ((@ (vE,K)) * b1) by E1, E2, E0, down1;
E4: (down (l,b1)) . v <> 0. F by E1, VECTSP_6:2;
vb1 in Carrier l by E3, E4, VECTSP_6:2;
then (@ (vE,K)) * b1 = a * b by D1, D3, TARSKI:def 1;
hence contradiction by D3, E0, E1, E2, BE0; :: thesis:

end;

hence Carrier (down (l,b1)) = {} by XBOOLE_0:def 1; :: thesis:

end;

D10: for b1 being Element of K st b1 in BK & b1 <> b holds
(down l) . b1 = 0. E

proof

let b1 be Element of K; :: thesis:
assume E1: ( b1 in BK & b1 <> b ) ; :: thesis:
then E2: (down l) . b1 = Sum (down (l,b1)) by down2;
Carrier (down (l,b1)) = {} by E1, D10a;
then Sum (down (l,b1)) = 0. (VecSp (E,F)) by VECTSP_6:19;
hence (down l) . b1 = 0. E by E2, FIELD_4:def 6; :: thesis:

end;

D5: Carrier (down l) = {b}

proof

C0: [labE,aE] in [: the carrier of F, the carrier of E:] by B0, ZFMISC_1:def 2;

C1: now :: thesis:

let u be object ; :: thesis:
assume C2: u in {b} ; :: thesis:
C3: (down l) . b = the lmult of (VecSp (E,F)) . [lab,a] by D9, D3, D7, down2
.= ( the multF of E | [: the carrier of F, the carrier of E:]) . [labE,aE] by FIELD_4:def 6
.= the multF of E . [labE,aE] by C0, FUNCT_1:49 ;
labE * aE <> 0. E by D7a, D8, VECTSP_2:def 1;
then vb in Carrier (down l) by C3, VECTSP_6:2;
hence u in Carrier (down l) by C2, TARSKI:def 1; :: thesis:

end;

now :: thesis:

let u be object ; :: thesis:
assume C2: u in Carrier (down l) ; :: thesis:
C3: Carrier (down l) c= BK by VECTSP_6:def 4;
reconsider bK = u as Element of K by C2, FIELD_4:def 6;
reconsider bV = bK as Element of (VecSp (K,E)) by FIELD_4:def 6;
(down l) . bK <> 0. E by C2, VECTSP_6:2;
then bK = b by C3, C2, D10;
hence u in {b} by TARSKI:def 1; :: thesis:

end;

hence Carrier (down l) = {b} by C1, TARSKI:2; :: thesis:

end;

B2: (down (l,b)) . a = l . (a * b) by D3, down1;
B3: [(l . (a * b)),a] in [: the carrier of F, the carrier of E:] by H1, D3, B0, ZFMISC_1:def 2;
l . (a * b) is Element of the carrier of E by B0, H3;
then B4: [(l . (a * b)),a] in [: the carrier of E, the carrier of E:] by H1, D3, ZFMISC_1:def 2;
B6: (down l) . vb = Sum (down (l,b)) by D3, down2
.= ((down (l,b)) . va) * va by D6, VECTSP_6:20
.= ( the multF of E | [: the carrier of F, the carrier of E:]) . ((l . (a * b)),a) by B2, FIELD_4:def 6
.= the multF of E . ((l . (a * b)),a) by B3, FUNCT_1:49
.= ( the multF of K || the carrier of E) . ((l . (a * b)),a) by H2, C0SP1:def 3
.= lab * a by B4, FUNCT_1:49 ;
then B7: [(lab * a),b] in [: the carrier of E, the carrier of K:] by ZFMISC_1:def 2;
B: Sum (down l) = ((down l) . vb) * vb by D5, VECTSP_6:20
.= ( the multF of K | [: the carrier of E, the carrier of K:]) . ((lab * a),b) by B6, FIELD_4:def 6
.= the multF of K . ((lab * a),b) by B7, FUNCT_1:49 ;
B1: [(l . (a * b)),(a * b)] in [: the carrier of F, the carrier of K:] by B0, ZFMISC_1:def 2;
Sum l = (l . vab) * vab by D1, D3, VECTSP_6:20
.= ( the multF of K | [: the carrier of F, the carrier of K:]) . ((l . (a * b)),(a * b)) by FIELD_4:def 6
.= lab * (a * b) by B1, FUNCT_1:49
.= (lab * a) * b by GROUP_1:def 3 ;
hence Sum l = Sum (down l) by B; :: thesis: