let V be finite-dimensional RealLinearSpace; :: thesis: for W1, W2 being Subspace of V holds (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2)

let W1, W2 be Subspace of V; :: thesis: (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2)

reconsider V = V as RealLinearSpace ;

reconsider W1 = W1, W2 = W2 as Subspace of V ;

consider I being finite Subset of (W1 /\ W2) such that

A1: I is Basis of W1 /\ W2 by Def1;

W1 /\ W2 is Subspace of W2 by RLSUB_2:16;

then consider I2 being Basis of W2 such that

A2: I c= I2 by A1, Th16;

W1 /\ W2 is Subspace of W1 by RLSUB_2:16;

then consider I1 being Basis of W1 such that

A3: I c= I1 by A1, Th16;

reconsider I2 = I2 as finite Subset of W2 by Th23;

reconsider I1 = I1 as finite Subset of W1 by Th23;

I c= I1 /\ I2 by A3, A2, XBOOLE_1:19;

then I = I1 /\ I2 by A4, XBOOLE_0:def 10;

then A16: card A = ((card I1) + (card I2)) - (card I) by CARD_2:45;

for L being Linear_Combination of A st Sum L = 0. (W1 + W2) holds

Carrier L = {}

the carrier of (W1 + W2) c= the carrier of V by RLSUB_1:def 2;

then reconsider A9 = A as Subset of V by XBOOLE_1:1;

A57: card I2 = dim W2 by Def2;

then A68: W1 + W2 is Subspace of Lin A9 by RLSUB_1:28;

Lin A9 = Lin A by Th20;

then Lin A = W1 + W2 by A68, RLSUB_1:26;

then A is Basis of W1 + W2 by A56, RLVECT_3:def 3;

then A69: card A = dim (W1 + W2) by Def2;

card I = dim (W1 /\ W2) by A1, Def2;

hence (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2) by A57, A16, A69, Def2; :: thesis: verum

let W1, W2 be Subspace of V; :: thesis: (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2)

reconsider V = V as RealLinearSpace ;

reconsider W1 = W1, W2 = W2 as Subspace of V ;

consider I being finite Subset of (W1 /\ W2) such that

A1: I is Basis of W1 /\ W2 by Def1;

W1 /\ W2 is Subspace of W2 by RLSUB_2:16;

then consider I2 being Basis of W2 such that

A2: I c= I2 by A1, Th16;

W1 /\ W2 is Subspace of W1 by RLSUB_2:16;

then consider I1 being Basis of W1 such that

A3: I c= I1 by A1, Th16;

reconsider I2 = I2 as finite Subset of W2 by Th23;

reconsider I1 = I1 as finite Subset of W1 by Th23;

A4: now :: thesis: I1 /\ I2 c= I

set A = I1 \/ I2;
I1 is linearly-independent
by RLVECT_3:def 3;

then reconsider I19 = I1 as linearly-independent Subset of V by Th14;

assume not I1 /\ I2 c= I ; :: thesis: contradiction

then consider x being object such that

A5: x in I1 /\ I2 and

A6: not x in I ;

x in I1 by A5, XBOOLE_0:def 4;

then x in Lin I1 by RLVECT_3:15;

then x in RLSStruct(# the carrier of W1, the ZeroF of W1, the U5 of W1, the Mult of W1 #) by RLVECT_3:def 3;

then A7: x in the carrier of W1 by STRUCT_0:def 5;

A8: the carrier of W1 c= the carrier of V by RLSUB_1:def 2;

then reconsider x9 = x as VECTOR of V by A7;

x in {x} by TARSKI:def 1;

then A11: x9 in Ix by XBOOLE_0:def 3;

x in I2 by A5, XBOOLE_0:def 4;

then x in Lin I2 by RLVECT_3:15;

then x in RLSStruct(# the carrier of W2, the ZeroF of W2, the U5 of W2, the Mult of W2 #) by RLVECT_3:def 3;

then x in the carrier of W2 by STRUCT_0:def 5;

then x in the carrier of W1 /\ the carrier of W2 by A7, XBOOLE_0:def 4;

then x in the carrier of (W1 /\ W2) by RLSUB_2:def 2;

then A12: x in RLSStruct(# the carrier of (W1 /\ W2), the ZeroF of (W1 /\ W2), the U5 of (W1 /\ W2), the Mult of (W1 /\ W2) #) by STRUCT_0:def 5;

the carrier of (W1 /\ W2) c= the carrier of V by RLSUB_1:def 2;

then reconsider I9 = I as Subset of V by XBOOLE_1:1;

A13: Lin I = Lin I9 by Th20;

Ix \ {x} = I \ {x} by XBOOLE_1:40

.= I by A6, ZFMISC_1:57 ;

then not x9 in Lin I9 by A10, A11, Th17, RLVECT_3:5;

hence contradiction by A1, A12, A13, RLVECT_3:def 3; :: thesis: verum

end;then reconsider I19 = I1 as linearly-independent Subset of V by Th14;

assume not I1 /\ I2 c= I ; :: thesis: contradiction

then consider x being object such that

A5: x in I1 /\ I2 and

A6: not x in I ;

x in I1 by A5, XBOOLE_0:def 4;

then x in Lin I1 by RLVECT_3:15;

then x in RLSStruct(# the carrier of W1, the ZeroF of W1, the U5 of W1, the Mult of W1 #) by RLVECT_3:def 3;

then A7: x in the carrier of W1 by STRUCT_0:def 5;

A8: the carrier of W1 c= the carrier of V by RLSUB_1:def 2;

then reconsider x9 = x as VECTOR of V by A7;

now :: thesis: for y being object st y in I \/ {x} holds

y in the carrier of V

then reconsider Ix = I \/ {x} as Subset of V by TARSKI:def 3;y in the carrier of V

let y be object ; :: thesis: ( y in I \/ {x} implies y in the carrier of V )

the carrier of (W1 /\ W2) c= the carrier of V by RLSUB_1:def 2;

then A9: I c= the carrier of V ;

assume y in I \/ {x} ; :: thesis: y in the carrier of V

then ( y in I or y in {x} ) by XBOOLE_0:def 3;

then ( y in the carrier of V or y = x ) by A9, TARSKI:def 1;

hence y in the carrier of V by A7, A8; :: thesis: verum

end;the carrier of (W1 /\ W2) c= the carrier of V by RLSUB_1:def 2;

then A9: I c= the carrier of V ;

assume y in I \/ {x} ; :: thesis: y in the carrier of V

then ( y in I or y in {x} ) by XBOOLE_0:def 3;

then ( y in the carrier of V or y = x ) by A9, TARSKI:def 1;

hence y in the carrier of V by A7, A8; :: thesis: verum

now :: thesis: for y being object st y in I \/ {x} holds

y in I19

then A10:
Ix c= I19
;y in I19

let y be object ; :: thesis: ( y in I \/ {x} implies y in I19 )

assume y in I \/ {x} ; :: thesis: y in I19

then ( y in I or y in {x} ) by XBOOLE_0:def 3;

then ( y in I1 or y = x ) by A3, TARSKI:def 1;

hence y in I19 by A5, XBOOLE_0:def 4; :: thesis: verum

end;assume y in I \/ {x} ; :: thesis: y in I19

then ( y in I or y in {x} ) by XBOOLE_0:def 3;

then ( y in I1 or y = x ) by A3, TARSKI:def 1;

hence y in I19 by A5, XBOOLE_0:def 4; :: thesis: verum

x in {x} by TARSKI:def 1;

then A11: x9 in Ix by XBOOLE_0:def 3;

x in I2 by A5, XBOOLE_0:def 4;

then x in Lin I2 by RLVECT_3:15;

then x in RLSStruct(# the carrier of W2, the ZeroF of W2, the U5 of W2, the Mult of W2 #) by RLVECT_3:def 3;

then x in the carrier of W2 by STRUCT_0:def 5;

then x in the carrier of W1 /\ the carrier of W2 by A7, XBOOLE_0:def 4;

then x in the carrier of (W1 /\ W2) by RLSUB_2:def 2;

then A12: x in RLSStruct(# the carrier of (W1 /\ W2), the ZeroF of (W1 /\ W2), the U5 of (W1 /\ W2), the Mult of (W1 /\ W2) #) by STRUCT_0:def 5;

the carrier of (W1 /\ W2) c= the carrier of V by RLSUB_1:def 2;

then reconsider I9 = I as Subset of V by XBOOLE_1:1;

A13: Lin I = Lin I9 by Th20;

Ix \ {x} = I \ {x} by XBOOLE_1:40

.= I by A6, ZFMISC_1:57 ;

then not x9 in Lin I9 by A10, A11, Th17, RLVECT_3:5;

hence contradiction by A1, A12, A13, RLVECT_3:def 3; :: thesis: verum

now :: thesis: for v being object st v in I1 \/ I2 holds

v in the carrier of (W1 + W2)

then reconsider A = I1 \/ I2 as finite Subset of (W1 + W2) by TARSKI:def 3;v in the carrier of (W1 + W2)

let v be object ; :: thesis: ( v in I1 \/ I2 implies v in the carrier of (W1 + W2) )

A14: ( the carrier of W1 c= the carrier of V & the carrier of W2 c= the carrier of V ) by RLSUB_1:def 2;

assume v in I1 \/ I2 ; :: thesis: v in the carrier of (W1 + W2)

then A15: ( v in I1 or v in I2 ) by XBOOLE_0:def 3;

then ( v in the carrier of W1 or v in the carrier of W2 ) ;

then reconsider v9 = v as VECTOR of V by A14;

( v9 in W1 or v9 in W2 ) by A15, STRUCT_0:def 5;

then v9 in W1 + W2 by RLSUB_2:2;

hence v in the carrier of (W1 + W2) by STRUCT_0:def 5; :: thesis: verum

end;A14: ( the carrier of W1 c= the carrier of V & the carrier of W2 c= the carrier of V ) by RLSUB_1:def 2;

assume v in I1 \/ I2 ; :: thesis: v in the carrier of (W1 + W2)

then A15: ( v in I1 or v in I2 ) by XBOOLE_0:def 3;

then ( v in the carrier of W1 or v in the carrier of W2 ) ;

then reconsider v9 = v as VECTOR of V by A14;

( v9 in W1 or v9 in W2 ) by A15, STRUCT_0:def 5;

then v9 in W1 + W2 by RLSUB_2:2;

hence v in the carrier of (W1 + W2) by STRUCT_0:def 5; :: thesis: verum

I c= I1 /\ I2 by A3, A2, XBOOLE_1:19;

then I = I1 /\ I2 by A4, XBOOLE_0:def 10;

then A16: card A = ((card I1) + (card I2)) - (card I) by CARD_2:45;

for L being Linear_Combination of A st Sum L = 0. (W1 + W2) holds

Carrier L = {}

proof

then A56:
A is linearly-independent
by RLVECT_3:def 1;
( W1 is Subspace of W1 + W2 & I1 is linearly-independent )
by RLSUB_2:7, RLVECT_3:def 3;

then reconsider I19 = I1 as linearly-independent Subset of (W1 + W2) by Th14;

reconsider W29 = W2 as Subspace of W1 + W2 by RLSUB_2:7;

reconsider W19 = W1 as Subspace of W1 + W2 by RLSUB_2:7;

let L be Linear_Combination of A; :: thesis: ( Sum L = 0. (W1 + W2) implies Carrier L = {} )

assume A17: Sum L = 0. (W1 + W2) ; :: thesis: Carrier L = {}

A18: I1 misses (Carrier L) \ I1 by XBOOLE_1:79;

set B = (Carrier L) /\ I1;

consider F being FinSequence of the carrier of (W1 + W2) such that

A19: F is one-to-one and

A20: rng F = Carrier L and

A21: Sum L = Sum (L (#) F) by RLVECT_2:def 8;

reconsider B = (Carrier L) /\ I1 as Subset of (rng F) by A20, XBOOLE_1:17;

reconsider F1 = F - (B `), F2 = F - B as FinSequence of the carrier of (W1 + W2) by FINSEQ_3:86;

consider L1 being Linear_Combination of W1 + W2 such that

A22: Carrier L1 = (rng F1) /\ (Carrier L) and

A23: L1 (#) F1 = L (#) F1 by Th7;

F1 is one-to-one by A19, FINSEQ_3:87;

then A24: Sum (L (#) F1) = Sum L1 by A22, A23, Th6, XBOOLE_1:17;

rng F c= rng F ;

then reconsider X = rng F as Subset of (rng F) ;

consider L2 being Linear_Combination of W1 + W2 such that

A25: Carrier L2 = (rng F2) /\ (Carrier L) and

A26: L2 (#) F2 = L (#) F2 by Th7;

F2 is one-to-one by A19, FINSEQ_3:87;

then A27: Sum (L (#) F2) = Sum L2 by A25, A26, Th6, XBOOLE_1:17;

X \ (B `) = X /\ ((B `) `) by SUBSET_1:13

.= B by XBOOLE_1:28 ;

then rng F1 = B by FINSEQ_3:65;

then A28: Carrier L1 = I1 /\ ((Carrier L) /\ (Carrier L)) by A22, XBOOLE_1:16

.= (Carrier L) /\ I1 ;

then consider K1 being Linear_Combination of W19 such that

Carrier K1 = Carrier L1 and

A29: Sum K1 = Sum L1 by Th12;

rng F2 = (Carrier L) \ ((Carrier L) /\ I1) by A20, FINSEQ_3:65

.= (Carrier L) \ I1 by XBOOLE_1:47 ;

then A30: Carrier L2 = (Carrier L) \ I1 by A25, XBOOLE_1:28, XBOOLE_1:36;

then (Carrier L1) /\ (Carrier L2) = (Carrier L) /\ (I1 /\ ((Carrier L) \ I1)) by A28, XBOOLE_1:16

.= (Carrier L) /\ {} by A18, XBOOLE_0:def 7

.= {} ;

then A31: Carrier L1 misses Carrier L2 by XBOOLE_0:def 7;

A32: Carrier L c= I1 \/ I2 by RLVECT_2:def 6;

then A33: Carrier L2 c= I2 by A30, XBOOLE_1:43;

Carrier L2 c= I2 by A32, A30, XBOOLE_1:43;

then consider K2 being Linear_Combination of W29 such that

Carrier K2 = Carrier L2 and

A34: Sum K2 = Sum L2 by Th12, XBOOLE_1:1;

A35: Sum K1 in W1 by STRUCT_0:def 5;

ex P being Permutation of (dom F) st (F - (B `)) ^ (F - B) = F * P by FINSEQ_3:115;

then A36: 0. (W1 + W2) = Sum (L (#) (F1 ^ F2)) by A17, A21, Th4

.= Sum ((L (#) F1) ^ (L (#) F2)) by RLVECT_3:34

.= (Sum L1) + (Sum L2) by A24, A27, RLVECT_1:41 ;

then Sum L1 = - (Sum L2) by RLVECT_1:def 10

.= - (Sum K2) by A34, RLSUB_1:15 ;

then Sum K1 in W2 by A29, STRUCT_0:def 5;

then Sum K1 in W1 /\ W2 by A35, RLSUB_2:3;

then Sum K1 in Lin I by A1, RLVECT_3:def 3;

then consider KI being Linear_Combination of I such that

A37: Sum K1 = Sum KI by RLVECT_3:14;

A38: Carrier L = (Carrier L1) \/ (Carrier L2) by A28, A30, XBOOLE_1:51;

A48: I2 is linearly-independent by RLVECT_3:def 3;

A49: Carrier L1 c= I1 by A28, XBOOLE_1:17;

W1 /\ W2 is Subspace of W1 + W2 by RLSUB_2:22;

then consider LI being Linear_Combination of W1 + W2 such that

A50: Carrier LI = Carrier KI and

A51: Sum LI = Sum KI by Th11;

Carrier LI c= I by A50, RLVECT_2:def 6;

then Carrier LI c= I19 by A3;

then A52: LI = L1 by A49, A29, A37, A51, Th1;

Carrier LI c= I by A50, RLVECT_2:def 6;

then ( Carrier (LI + L2) c= (Carrier LI) \/ (Carrier L2) & (Carrier LI) \/ (Carrier L2) c= I2 ) by A47, A33, RLVECT_2:37, XBOOLE_1:13;

then A53: Carrier (LI + L2) c= I2 ;

W2 is Subspace of W1 + W2 by RLSUB_2:7;

then consider K being Linear_Combination of W2 such that

A54: Carrier K = Carrier (LI + L2) and

A55: Sum K = Sum (LI + L2) by A53, Th12, XBOOLE_1:1;

reconsider K = K as Linear_Combination of I2 by A53, A54, RLVECT_2:def 6;

0. W2 = (Sum LI) + (Sum L2) by A29, A36, A37, A51, RLSUB_1:12

.= Sum K by A55, RLVECT_3:1 ;

then {} = Carrier (L1 + L2) by A54, A52, A48, RLVECT_3:def 1;

hence Carrier L = {} by A39; :: thesis: verum

end;then reconsider I19 = I1 as linearly-independent Subset of (W1 + W2) by Th14;

reconsider W29 = W2 as Subspace of W1 + W2 by RLSUB_2:7;

reconsider W19 = W1 as Subspace of W1 + W2 by RLSUB_2:7;

let L be Linear_Combination of A; :: thesis: ( Sum L = 0. (W1 + W2) implies Carrier L = {} )

assume A17: Sum L = 0. (W1 + W2) ; :: thesis: Carrier L = {}

A18: I1 misses (Carrier L) \ I1 by XBOOLE_1:79;

set B = (Carrier L) /\ I1;

consider F being FinSequence of the carrier of (W1 + W2) such that

A19: F is one-to-one and

A20: rng F = Carrier L and

A21: Sum L = Sum (L (#) F) by RLVECT_2:def 8;

reconsider B = (Carrier L) /\ I1 as Subset of (rng F) by A20, XBOOLE_1:17;

reconsider F1 = F - (B `), F2 = F - B as FinSequence of the carrier of (W1 + W2) by FINSEQ_3:86;

consider L1 being Linear_Combination of W1 + W2 such that

A22: Carrier L1 = (rng F1) /\ (Carrier L) and

A23: L1 (#) F1 = L (#) F1 by Th7;

F1 is one-to-one by A19, FINSEQ_3:87;

then A24: Sum (L (#) F1) = Sum L1 by A22, A23, Th6, XBOOLE_1:17;

rng F c= rng F ;

then reconsider X = rng F as Subset of (rng F) ;

consider L2 being Linear_Combination of W1 + W2 such that

A25: Carrier L2 = (rng F2) /\ (Carrier L) and

A26: L2 (#) F2 = L (#) F2 by Th7;

F2 is one-to-one by A19, FINSEQ_3:87;

then A27: Sum (L (#) F2) = Sum L2 by A25, A26, Th6, XBOOLE_1:17;

X \ (B `) = X /\ ((B `) `) by SUBSET_1:13

.= B by XBOOLE_1:28 ;

then rng F1 = B by FINSEQ_3:65;

then A28: Carrier L1 = I1 /\ ((Carrier L) /\ (Carrier L)) by A22, XBOOLE_1:16

.= (Carrier L) /\ I1 ;

then consider K1 being Linear_Combination of W19 such that

Carrier K1 = Carrier L1 and

A29: Sum K1 = Sum L1 by Th12;

rng F2 = (Carrier L) \ ((Carrier L) /\ I1) by A20, FINSEQ_3:65

.= (Carrier L) \ I1 by XBOOLE_1:47 ;

then A30: Carrier L2 = (Carrier L) \ I1 by A25, XBOOLE_1:28, XBOOLE_1:36;

then (Carrier L1) /\ (Carrier L2) = (Carrier L) /\ (I1 /\ ((Carrier L) \ I1)) by A28, XBOOLE_1:16

.= (Carrier L) /\ {} by A18, XBOOLE_0:def 7

.= {} ;

then A31: Carrier L1 misses Carrier L2 by XBOOLE_0:def 7;

A32: Carrier L c= I1 \/ I2 by RLVECT_2:def 6;

then A33: Carrier L2 c= I2 by A30, XBOOLE_1:43;

Carrier L2 c= I2 by A32, A30, XBOOLE_1:43;

then consider K2 being Linear_Combination of W29 such that

Carrier K2 = Carrier L2 and

A34: Sum K2 = Sum L2 by Th12, XBOOLE_1:1;

A35: Sum K1 in W1 by STRUCT_0:def 5;

ex P being Permutation of (dom F) st (F - (B `)) ^ (F - B) = F * P by FINSEQ_3:115;

then A36: 0. (W1 + W2) = Sum (L (#) (F1 ^ F2)) by A17, A21, Th4

.= Sum ((L (#) F1) ^ (L (#) F2)) by RLVECT_3:34

.= (Sum L1) + (Sum L2) by A24, A27, RLVECT_1:41 ;

then Sum L1 = - (Sum L2) by RLVECT_1:def 10

.= - (Sum K2) by A34, RLSUB_1:15 ;

then Sum K1 in W2 by A29, STRUCT_0:def 5;

then Sum K1 in W1 /\ W2 by A35, RLSUB_2:3;

then Sum K1 in Lin I by A1, RLVECT_3:def 3;

then consider KI being Linear_Combination of I such that

A37: Sum K1 = Sum KI by RLVECT_3:14;

A38: Carrier L = (Carrier L1) \/ (Carrier L2) by A28, A30, XBOOLE_1:51;

A39: now :: thesis: Carrier L c= Carrier (L1 + L2)

A47:
I \/ I2 = I2
by A2, XBOOLE_1:12;assume
not Carrier L c= Carrier (L1 + L2)
; :: thesis: contradiction

then consider x being object such that

A40: x in Carrier L and

A41: not x in Carrier (L1 + L2) ;

reconsider x = x as VECTOR of (W1 + W2) by A40;

A42: 0 = (L1 + L2) . x by A41, RLVECT_2:19

.= (L1 . x) + (L2 . x) by RLVECT_2:def 10 ;

end;then consider x being object such that

A40: x in Carrier L and

A41: not x in Carrier (L1 + L2) ;

reconsider x = x as VECTOR of (W1 + W2) by A40;

A42: 0 = (L1 + L2) . x by A41, RLVECT_2:19

.= (L1 . x) + (L2 . x) by RLVECT_2:def 10 ;

per cases
( x in Carrier L1 or x in Carrier L2 )
by A38, A40, XBOOLE_0:def 3;

end;

suppose A43:
x in Carrier L1
; :: thesis: contradiction

then
not x in Carrier L2
by A31, XBOOLE_0:3;

then A44: L2 . x = 0 by RLVECT_2:19;

ex v being VECTOR of (W1 + W2) st

( x = v & L1 . v <> 0 ) by A43, Th3;

hence contradiction by A42, A44; :: thesis: verum

end;then A44: L2 . x = 0 by RLVECT_2:19;

ex v being VECTOR of (W1 + W2) st

( x = v & L1 . v <> 0 ) by A43, Th3;

hence contradiction by A42, A44; :: thesis: verum

suppose A45:
x in Carrier L2
; :: thesis: contradiction

then
not x in Carrier L1
by A31, XBOOLE_0:3;

then A46: L1 . x = 0 by RLVECT_2:19;

ex v being VECTOR of (W1 + W2) st

( x = v & L2 . v <> 0 ) by A45, Th3;

hence contradiction by A42, A46; :: thesis: verum

end;then A46: L1 . x = 0 by RLVECT_2:19;

ex v being VECTOR of (W1 + W2) st

( x = v & L2 . v <> 0 ) by A45, Th3;

hence contradiction by A42, A46; :: thesis: verum

A48: I2 is linearly-independent by RLVECT_3:def 3;

A49: Carrier L1 c= I1 by A28, XBOOLE_1:17;

W1 /\ W2 is Subspace of W1 + W2 by RLSUB_2:22;

then consider LI being Linear_Combination of W1 + W2 such that

A50: Carrier LI = Carrier KI and

A51: Sum LI = Sum KI by Th11;

Carrier LI c= I by A50, RLVECT_2:def 6;

then Carrier LI c= I19 by A3;

then A52: LI = L1 by A49, A29, A37, A51, Th1;

Carrier LI c= I by A50, RLVECT_2:def 6;

then ( Carrier (LI + L2) c= (Carrier LI) \/ (Carrier L2) & (Carrier LI) \/ (Carrier L2) c= I2 ) by A47, A33, RLVECT_2:37, XBOOLE_1:13;

then A53: Carrier (LI + L2) c= I2 ;

W2 is Subspace of W1 + W2 by RLSUB_2:7;

then consider K being Linear_Combination of W2 such that

A54: Carrier K = Carrier (LI + L2) and

A55: Sum K = Sum (LI + L2) by A53, Th12, XBOOLE_1:1;

reconsider K = K as Linear_Combination of I2 by A53, A54, RLVECT_2:def 6;

0. W2 = (Sum LI) + (Sum L2) by A29, A36, A37, A51, RLSUB_1:12

.= Sum K by A55, RLVECT_3:1 ;

then {} = Carrier (L1 + L2) by A54, A52, A48, RLVECT_3:def 1;

hence Carrier L = {} by A39; :: thesis: verum

the carrier of (W1 + W2) c= the carrier of V by RLSUB_1:def 2;

then reconsider A9 = A as Subset of V by XBOOLE_1:1;

A57: card I2 = dim W2 by Def2;

now :: thesis: for x being object st x in the carrier of (W1 + W2) holds

x in the carrier of (Lin A9)

then
the carrier of (W1 + W2) c= the carrier of (Lin A9)
;x in the carrier of (Lin A9)

let x be object ; :: thesis: ( x in the carrier of (W1 + W2) implies x in the carrier of (Lin A9) )

assume x in the carrier of (W1 + W2) ; :: thesis: x in the carrier of (Lin A9)

then x in W1 + W2 by STRUCT_0:def 5;

then consider w1, w2 being VECTOR of V such that

A58: w1 in W1 and

A59: w2 in W2 and

A60: x = w1 + w2 by RLSUB_2:1;

reconsider w1 = w1 as VECTOR of W1 by A58, STRUCT_0:def 5;

w1 in Lin I1 by Th13;

then consider K1 being Linear_Combination of I1 such that

A61: w1 = Sum K1 by RLVECT_3:14;

reconsider w2 = w2 as VECTOR of W2 by A59, STRUCT_0:def 5;

w2 in Lin I2 by Th13;

then consider K2 being Linear_Combination of I2 such that

A62: w2 = Sum K2 by RLVECT_3:14;

consider L2 being Linear_Combination of V such that

A63: Carrier L2 = Carrier K2 and

A64: Sum L2 = Sum K2 by Th11;

A65: Carrier L2 c= I2 by A63, RLVECT_2:def 6;

consider L1 being Linear_Combination of V such that

A66: Carrier L1 = Carrier K1 and

A67: Sum L1 = Sum K1 by Th11;

set L = L1 + L2;

Carrier L1 c= I1 by A66, RLVECT_2:def 6;

then ( Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) & (Carrier L1) \/ (Carrier L2) c= I1 \/ I2 ) by A65, RLVECT_2:37, XBOOLE_1:13;

then Carrier (L1 + L2) c= I1 \/ I2 ;

then reconsider L = L1 + L2 as Linear_Combination of A9 by RLVECT_2:def 6;

x = Sum L by A60, A61, A67, A62, A64, RLVECT_3:1;

then x in Lin A9 by RLVECT_3:14;

hence x in the carrier of (Lin A9) by STRUCT_0:def 5; :: thesis: verum

end;assume x in the carrier of (W1 + W2) ; :: thesis: x in the carrier of (Lin A9)

then x in W1 + W2 by STRUCT_0:def 5;

then consider w1, w2 being VECTOR of V such that

A58: w1 in W1 and

A59: w2 in W2 and

A60: x = w1 + w2 by RLSUB_2:1;

reconsider w1 = w1 as VECTOR of W1 by A58, STRUCT_0:def 5;

w1 in Lin I1 by Th13;

then consider K1 being Linear_Combination of I1 such that

A61: w1 = Sum K1 by RLVECT_3:14;

reconsider w2 = w2 as VECTOR of W2 by A59, STRUCT_0:def 5;

w2 in Lin I2 by Th13;

then consider K2 being Linear_Combination of I2 such that

A62: w2 = Sum K2 by RLVECT_3:14;

consider L2 being Linear_Combination of V such that

A63: Carrier L2 = Carrier K2 and

A64: Sum L2 = Sum K2 by Th11;

A65: Carrier L2 c= I2 by A63, RLVECT_2:def 6;

consider L1 being Linear_Combination of V such that

A66: Carrier L1 = Carrier K1 and

A67: Sum L1 = Sum K1 by Th11;

set L = L1 + L2;

Carrier L1 c= I1 by A66, RLVECT_2:def 6;

then ( Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) & (Carrier L1) \/ (Carrier L2) c= I1 \/ I2 ) by A65, RLVECT_2:37, XBOOLE_1:13;

then Carrier (L1 + L2) c= I1 \/ I2 ;

then reconsider L = L1 + L2 as Linear_Combination of A9 by RLVECT_2:def 6;

x = Sum L by A60, A61, A67, A62, A64, RLVECT_3:1;

then x in Lin A9 by RLVECT_3:14;

hence x in the carrier of (Lin A9) by STRUCT_0:def 5; :: thesis: verum

then A68: W1 + W2 is Subspace of Lin A9 by RLSUB_1:28;

Lin A9 = Lin A by Th20;

then Lin A = W1 + W2 by A68, RLSUB_1:26;

then A is Basis of W1 + W2 by A56, RLVECT_3:def 3;

then A69: card A = dim (W1 + W2) by Def2;

card I = dim (W1 /\ W2) by A1, Def2;

hence (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2) by A57, A16, A69, Def2; :: thesis: verum