let V be finite-dimensional RealUnitarySpace; :: 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 RealUnitarySpace ;
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 RUSUB_2:16;
then consider I2 being Basis of W2 such that
A2: I c= I2 by ;
W1 /\ W2 is Subspace of W1 by RUSUB_2:16;
then consider I1 being Basis of W1 such that
A3: I c= I1 by ;
reconsider I2 = I2 as finite Subset of W2 by Th3;
reconsider I1 = I1 as finite Subset of W1 by Th3;
A4: now :: thesis: I1 /\ I2 c= I
I1 is linearly-independent by RUSUB_3:def 2;
then reconsider I19 = I1 as linearly-independent Subset of V by RUSUB_3:22;
the carrier of (W1 /\ W2) c= the carrier of V by RUSUB_1:def 1;
then reconsider I9 = I as Subset of V by XBOOLE_1:1;
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 ;
then x in Lin I1 by RUSUB_3:2;
then x in UNITSTR(# the carrier of W1, the ZeroF of W1, the addF of W1, the Mult of W1, the scalar of W1 #) by RUSUB_3:def 2;
then A7: x in the carrier of W1 ;
A8: the carrier of W1 c= the carrier of V by RUSUB_1:def 1;
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
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 RUSUB_1:def 1;
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 ;
hence y in the carrier of V by A7, A8; :: thesis: verum
end;
then reconsider Ix = I \/ {x} as Subset of V by TARSKI:def 3;
now :: thesis: for y being object st y in I \/ {x} holds
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 ;
hence y in I19 by ; :: thesis: verum
end;
then A10: Ix c= I19 ;
x in {x} by TARSKI:def 1;
then A11: x9 in Ix by XBOOLE_0:def 3;
x in I2 by ;
then x in Lin I2 by RUSUB_3:2;
then x in UNITSTR(# the carrier of W2, the ZeroF of W2, the addF of W2, the Mult of W2, the scalar of W2 #) by RUSUB_3:def 2;
then x in the carrier of W2 ;
then x in the carrier of W1 /\ the carrier of W2 by ;
then x in the carrier of (W1 /\ W2) by RUSUB_2:def 2;
then x in UNITSTR(# the carrier of (W1 /\ W2), the ZeroF of (W1 /\ W2), the addF of (W1 /\ W2), the Mult of (W1 /\ W2), the scalar of (W1 /\ W2) #) ;
then A12: x in Lin I by ;
Ix \ {x} = I \ {x} by XBOOLE_1:40
.= I by ;
then not x9 in Lin I9 by ;
hence contradiction by A12, RUSUB_3:28; :: thesis: verum
end;
set A = I1 \/ I2;
now :: thesis: for v being object st v in I1 \/ I2 holds
v in the carrier of (W1 + W2)
let v be object ; :: thesis: ( v in I1 \/ I2 implies v in the carrier of (W1 + W2) )
A13: ( the carrier of W1 c= the carrier of V & the carrier of W2 c= the carrier of V ) by RUSUB_1:def 1;
assume v in I1 \/ I2 ; :: thesis: v in the carrier of (W1 + W2)
then A14: ( 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 A13;
( v9 in W1 or v9 in W2 ) by A14;
then v9 in W1 + W2 by RUSUB_2:2;
hence v in the carrier of (W1 + W2) ; :: thesis: verum
end;
then reconsider A = I1 \/ I2 as finite Subset of (W1 + W2) by TARSKI:def 3;
I c= I1 /\ I2 by ;
then I = I1 /\ I2 by A4;
then A15: 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
( W1 is Subspace of W1 + W2 & I1 is linearly-independent ) by ;
then reconsider I19 = I1 as linearly-independent Subset of (W1 + W2) by RUSUB_3:22;
reconsider W29 = W2 as Subspace of W1 + W2 by RUSUB_2:7;
reconsider W19 = W1 as Subspace of W1 + W2 by RUSUB_2:7;
let L be Linear_Combination of A; :: thesis: ( Sum L = 0. (W1 + W2) implies Carrier L = {} )
assume A16: Sum L = 0. (W1 + W2) ; :: thesis:
A17: I1 misses () \ I1 by XBOOLE_1:79;
set B = () /\ I1;
consider F being FinSequence of the carrier of (W1 + W2) such that
A18: F is one-to-one and
A19: rng F = Carrier L and
A20: Sum L = Sum (L (#) F) by RLVECT_2:def 8;
reconsider B = () /\ I1 as Subset of (rng F) by ;
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
A21: Carrier L1 = (rng F1) /\ () and
A22: L1 (#) F1 = L (#) F1 by RLVECT_5:7;
F1 is one-to-one by ;
then A23: Sum (L (#) F1) = Sum L1 by ;
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
A24: Carrier L2 = (rng F2) /\ () and
A25: L2 (#) F2 = L (#) F2 by RLVECT_5:7;
F2 is one-to-one by ;
then A26: Sum (L (#) F2) = Sum L2 by ;
X \ (B `) = X /\ ((B `) `) by SUBSET_1:13
.= B by XBOOLE_1:28 ;
then rng F1 = B by FINSEQ_3:65;
then A27: Carrier L1 = I1 /\ (() /\ ()) by
.= () /\ I1 ;
then consider K1 being Linear_Combination of W19 such that
Carrier K1 = Carrier L1 and
A28: Sum K1 = Sum L1 by RUSUB_3:20;
rng F2 = () \ (() /\ I1) by
.= () \ I1 by XBOOLE_1:47 ;
then A29: Carrier L2 = () \ I1 by ;
then (Carrier L1) /\ (Carrier L2) = () /\ (I1 /\ (() \ I1)) by
.= () /\ {} by A17
.= {} ;
then A30: Carrier L1 misses Carrier L2 ;
A31: Carrier L c= I1 \/ I2 by RLVECT_2:def 6;
then A32: Carrier L2 c= I2 by ;
Carrier L2 c= I2 by ;
then consider K2 being Linear_Combination of W29 such that
Carrier K2 = Carrier L2 and
A33: Sum K2 = Sum L2 by ;
A34: Sum K1 in W1 ;
ex P being Permutation of (dom F) st (F - (B `)) ^ (F - B) = F * P by FINSEQ_3:115;
then A35: 0. (W1 + W2) = Sum (L (#) (F1 ^ F2)) by
.= Sum ((L (#) F1) ^ (L (#) F2)) by RLVECT_3:34
.= (Sum L1) + (Sum L2) by ;
then Sum L1 = - (Sum L2) by RLVECT_1:def 10
.= - (Sum K2) by ;
then Sum K1 in W2 by A28;
then Sum K1 in W1 /\ W2 by ;
then Sum K1 in Lin I by ;
then consider KI being Linear_Combination of I such that
A36: Sum K1 = Sum KI by RUSUB_3:1;
A37: Carrier L = (Carrier L1) \/ (Carrier L2) by ;
A38: now :: thesis: Carrier L c= Carrier (L1 + L2)
assume not Carrier L c= Carrier (L1 + L2) ; :: thesis: contradiction
then consider x being object such that
A39: x in Carrier L and
A40: not x in Carrier (L1 + L2) ;
reconsider x = x as VECTOR of (W1 + W2) by A39;
A41: 0 = (L1 + L2) . x by
.= (L1 . x) + (L2 . x) by RLVECT_2:def 10 ;
per cases ( x in Carrier L1 or x in Carrier L2 ) by ;
suppose A42: x in Carrier L1 ; :: thesis: contradiction
then not x in Carrier L2 by ;
then A43: L2 . x = 0 by RLVECT_2:19;
ex v being VECTOR of (W1 + W2) st
( x = v & L1 . v <> 0 ) by ;
hence contradiction by A41, A43; :: thesis: verum
end;
suppose A44: x in Carrier L2 ; :: thesis: contradiction
then not x in Carrier L1 by ;
then A45: L1 . x = 0 by RLVECT_2:19;
ex v being VECTOR of (W1 + W2) st
( x = v & L2 . v <> 0 ) by ;
hence contradiction by A41, A45; :: thesis: verum
end;
end;
end;
A46: I \/ I2 = I2 by ;
A47: I2 is linearly-independent by RUSUB_3:def 2;
A48: Carrier L1 c= I1 by ;
W1 /\ W2 is Subspace of W1 + W2 by RUSUB_2:22;
then consider LI being Linear_Combination of W1 + W2 such that
A49: Carrier LI = Carrier KI and
A50: Sum LI = Sum KI by RUSUB_3:19;
Carrier LI c= I by ;
then Carrier LI c= I19 by A3;
then A51: LI = L1 by ;
Carrier LI c= I by ;
then ( Carrier (LI + L2) c= (Carrier LI) \/ (Carrier L2) & (Carrier LI) \/ (Carrier L2) c= I2 ) by ;
then A52: Carrier (LI + L2) c= I2 ;
W2 is Subspace of W1 + W2 by RUSUB_2:7;
then consider K being Linear_Combination of W2 such that
A53: Carrier K = Carrier (LI + L2) and
A54: Sum K = Sum (LI + L2) by ;
reconsider K = K as Linear_Combination of I2 by ;
0. W2 = (Sum LI) + (Sum L2) by
.= Sum K by ;
then {} = Carrier (L1 + L2) by ;
hence Carrier L = {} by A38; :: thesis: verum
end;
then A55: A is linearly-independent by RLVECT_3:def 1;
the carrier of (W1 + W2) c= the carrier of V by RUSUB_1:def 1;
then reconsider A9 = A as Subset of V by XBOOLE_1:1;
A56: 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)
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 ;
then consider w1, w2 being VECTOR of V such that
A57: w1 in W1 and
A58: w2 in W2 and
A59: x = w1 + w2 by RUSUB_2:1;
reconsider w1 = w1 as VECTOR of W1 by A57;
w1 in Lin I1 by RUSUB_3:21;
then consider K1 being Linear_Combination of I1 such that
A60: w1 = Sum K1 by RUSUB_3:1;
reconsider w2 = w2 as VECTOR of W2 by A58;
w2 in Lin I2 by RUSUB_3:21;
then consider K2 being Linear_Combination of I2 such that
A61: w2 = Sum K2 by RUSUB_3:1;
consider L2 being Linear_Combination of V such that
A62: Carrier L2 = Carrier K2 and
A63: Sum L2 = Sum K2 by RUSUB_3:19;
A64: Carrier L2 c= I2 by ;
consider L1 being Linear_Combination of V such that
A65: Carrier L1 = Carrier K1 and
A66: Sum L1 = Sum K1 by RUSUB_3:19;
set L = L1 + L2;
Carrier L1 c= I1 by ;
then ( Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) & (Carrier L1) \/ (Carrier L2) c= I1 \/ I2 ) by ;
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 ;
then x in Lin A9 by RUSUB_3:1;
hence x in the carrier of (Lin A9) ; :: thesis: verum
end;
then the carrier of (W1 + W2) c= the carrier of (Lin A9) ;
then ( Lin A9 = Lin A & W1 + W2 is Subspace of Lin A9 ) by ;
then Lin A = W1 + W2 by RUSUB_1:20;
then A67: A is Basis of W1 + W2 by ;
card I = dim (W1 /\ W2) by ;
then (dim (W1 + W2)) + (dim (W1 /\ W2)) = (((card I1) + (card I2)) + (- (card I))) + (card I) by
.= (dim W1) + (dim W2) by ;
hence (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2) ; :: thesis: verum