let GF be Field; :: thesis: for V being finite-dimensional VectSp of GF
for W1, W2 being Subspace of V holds (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2)
let V be finite-dimensional VectSp of GF; :: 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 VectSp of GF ;
reconsider W1 = W1, W2 = W2 as Subspace of V ;
consider I being finite Subset of (W1 /\ W2) such that
A2:
I is Basis of W1 /\ W2
by MATRLIN:def 3;
A3:
card I = dim (W1 /\ W2)
by A2, Def2;
W1 /\ W2 is Subspace of W1
by VECTSP_5:20;
then consider I1 being Basis of W1 such that
A4:
I c= I1
by A2, Th17;
reconsider I1 = I1 as finite Subset of W1 by Th24;
W1 /\ W2 is Subspace of W2
by VECTSP_5:20;
then consider I2 being Basis of W2 such that
A5:
I c= I2
by A2, Th17;
reconsider I2 = I2 as finite Subset of W2 by Th24;
A6:
card I2 = dim W2
by Def2;
set A = I1 \/ I2;
then reconsider A = I1 \/ I2 as finite Subset of (W1 + W2) by TARSKI:def 3;
A10:
I c= I1 /\ I2
by A4, A5, XBOOLE_1:19;
now assume
not
I1 /\ I2 c= I
;
:: thesis: contradictionthen consider x being
set such that A11:
x in I1 /\ I2
and A12:
not
x in I
by TARSKI:def 3;
(
x in I1 &
x in I2 )
by A11, XBOOLE_0:def 4;
then
(
x in Lin I1 &
x in Lin I2 )
by VECTSP_7:13;
then
(
x in VectSpStr(# the
carrier of
W1,the
U5 of
W1,the
U2 of
W1,the
lmult of
W1 #) &
x in VectSpStr(# the
carrier of
W2,the
U5 of
W2,the
U2 of
W2,the
lmult of
W2 #) )
by VECTSP_7:def 3;
then A13:
(
x in the
carrier of
W1 &
x in the
carrier of
W2 )
by STRUCT_0:def 5;
then
x in the
carrier of
W1 /\ the
carrier of
W2
by XBOOLE_0:def 4;
then
x in the
carrier of
(W1 /\ W2)
by VECTSP_5:def 2;
then A14:
x in VectSpStr(# the
carrier of
(W1 /\ W2),the
U5 of
(W1 /\ W2),the
U2 of
(W1 /\ W2),the
lmult of
(W1 /\ W2) #)
by STRUCT_0:def 5;
A15:
the
carrier of
W1 c= the
carrier of
V
by VECTSP_4:def 2;
then reconsider x' =
x as
Vector of
V by A13;
(
I c= the
carrier of
(W1 /\ W2) & the
carrier of
(W1 /\ W2) c= the
carrier of
V )
by VECTSP_4:def 2;
then reconsider I' =
I as
Subset of
V by XBOOLE_1:1;
then reconsider Ix =
I \/ {x} as
Subset of
V by TARSKI:def 3;
(
I1 is
linearly-independent &
I1 is
Subset of
W1 )
by VECTSP_7:def 3;
then reconsider I1' =
I1 as
linearly-independent Subset of
V by Th15;
then A17:
Ix c= I1'
by TARSKI:def 3;
x in {x}
by TARSKI:def 1;
then A18:
x' in Ix
by XBOOLE_0:def 3;
Ix \ {x} =
I \ {x}
by XBOOLE_1:40
.=
I
by A12, ZFMISC_1:65
;
then A19:
not
x' in Lin I'
by A17, A18, Th18, VECTSP_7:2;
Lin I = Lin I'
by Th21;
hence
contradiction
by A2, A14, A19, VECTSP_7:def 3;
:: thesis: verum end;
then
I = I1 /\ I2
by A10, XBOOLE_0:def 10;
then A20:
card A = ((card I1) + (card I2)) - (card I)
by CARD_2:64;
( A c= the carrier of (W1 + W2) & the carrier of (W1 + W2) c= the carrier of V )
by VECTSP_4:def 2;
then reconsider A' = A as Subset of V by XBOOLE_1:1;
A21:
Lin A' = Lin A
by Th21;
now let x be
set ;
:: thesis: ( x in the carrier of (W1 + W2) implies x in the carrier of (Lin A') )assume
x in the
carrier of
(W1 + W2)
;
:: thesis: x in the carrier of (Lin A')then
x in W1 + W2
by STRUCT_0:def 5;
then consider w1,
w2 being
Vector of
V such that A22:
w1 in W1
and A23:
w2 in W2
and A24:
x = w1 + w2
by VECTSP_5:5;
reconsider w1 =
w1 as
Vector of
W1 by A22, STRUCT_0:def 5;
reconsider w2 =
w2 as
Vector of
W2 by A23, STRUCT_0:def 5;
w1 in Lin I1
by Th14;
then consider K1 being
Linear_Combination of
I1 such that A25:
w1 = Sum K1
by VECTSP_7:12;
consider L1 being
Linear_Combination of
V such that A26:
(
Carrier L1 = Carrier K1 &
Sum L1 = Sum K1 )
by Th12;
w2 in Lin I2
by Th14;
then consider K2 being
Linear_Combination of
I2 such that A27:
w2 = Sum K2
by VECTSP_7:12;
consider L2 being
Linear_Combination of
V such that A28:
(
Carrier L2 = Carrier K2 &
Sum L2 = Sum K2 )
by Th12;
set L =
L1 + L2;
(
Carrier L1 c= I1 &
Carrier L2 c= I2 )
by A26, A28, VECTSP_6:def 7;
then
(
Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) &
(Carrier L1) \/ (Carrier L2) c= I1 \/ I2 )
by VECTSP_6:51, XBOOLE_1:13;
then
Carrier (L1 + L2) c= I1 \/ I2
by XBOOLE_1:1;
then reconsider L =
L1 + L2 as
Linear_Combination of
A' by VECTSP_6:def 7;
x = Sum L
by A24, A25, A26, A27, A28, VECTSP_6:77;
then
x in Lin A'
by VECTSP_7:12;
hence
x in the
carrier of
(Lin A')
by STRUCT_0:def 5;
:: thesis: verum end;
then
the carrier of (W1 + W2) c= the carrier of (Lin A')
by TARSKI:def 3;
then
W1 + W2 is Subspace of Lin A'
by VECTSP_4:35;
then A29:
Lin A = W1 + W2
by A21, VECTSP_4:33;
for L being Linear_Combination of A st Sum L = 0. (W1 + W2) holds
Carrier L = {}
proof
let L be
Linear_Combination of
A;
:: thesis: ( Sum L = 0. (W1 + W2) implies Carrier L = {} )
assume A30:
Sum L = 0. (W1 + W2)
;
:: thesis: Carrier L = {}
A31:
(
W1 is
Subspace of
W1 + W2 &
W2 is
Subspace of
W1 + W2 )
by VECTSP_5:11;
reconsider W1' =
W1 as
Subspace of
W1 + W2 by VECTSP_5:11;
reconsider W2' =
W2 as
Subspace of
W1 + W2 by VECTSP_5:11;
A32:
Carrier L c= I1 \/ I2
by VECTSP_6:def 7;
consider F being
FinSequence of the
carrier of
(W1 + W2) such that A33:
F is
one-to-one
and A34:
rng F = Carrier L
and A35:
Sum L = Sum (L (#) F)
by VECTSP_6:def 9;
set B =
(Carrier L) /\ I1;
reconsider B =
(Carrier L) /\ I1 as
Subset of
(rng F) by A34, XBOOLE_1:17;
consider P being
Permutation of
(dom F) such that A36:
(F - (B ` )) ^ (F - B) = F * P
by A33, FINSEQ_3:124;
reconsider F1 =
F - (B ` ),
F2 =
F - B as
FinSequence of the
carrier of
(W1 + W2) by FINSEQ_3:93;
A37:
(
F1 is
one-to-one &
F2 is
one-to-one )
by A33, FINSEQ_3:94;
consider L1 being
Linear_Combination of
W1 + W2 such that A38:
Carrier L1 = (rng F1) /\ (Carrier L)
and A39:
L1 (#) F1 = L (#) F1
by Th8;
A40:
Sum (L (#) F1) = Sum L1
by A37, A38, A39, Th7, XBOOLE_1:17;
rng F c= rng F
;
then reconsider X =
rng F as
Subset of
(rng F) ;
X \ (B ` ) =
X /\ ((B ` ) ` )
by SUBSET_1:32
.=
B
by XBOOLE_1:28
;
then
rng F1 = B
by FINSEQ_3:72;
then A41:
Carrier L1 =
I1 /\ ((Carrier L) /\ (Carrier L))
by A38, XBOOLE_1:16
.=
(Carrier L) /\ I1
;
then A42:
(
Carrier L1 c= I1 &
I1 c= the
carrier of
W1 )
by XBOOLE_1:17;
consider K1 being
Linear_Combination of
W1' such that
Carrier K1 = Carrier L1
and A43:
Sum K1 = Sum L1
by A41, Th13;
consider L2 being
Linear_Combination of
W1 + W2 such that A44:
Carrier L2 = (rng F2) /\ (Carrier L)
and A45:
L2 (#) F2 = L (#) F2
by Th8;
A46:
Sum (L (#) F2) = Sum L2
by A37, A44, A45, Th7, XBOOLE_1:17;
rng F2 =
(Carrier L) \ ((Carrier L) /\ I1)
by A34, FINSEQ_3:72
.=
(Carrier L) \ I1
by XBOOLE_1:47
;
then A47:
Carrier L2 = (Carrier L) \ I1
by A44, XBOOLE_1:28, XBOOLE_1:36;
then
(
Carrier L2 c= I2 &
I2 c= the
carrier of
W2 )
by A32, XBOOLE_1:43;
then
Carrier L2 c= the
carrier of
W2'
by XBOOLE_1:1;
then consider K2 being
Linear_Combination of
W2' such that
Carrier K2 = Carrier L2
and A48:
Sum K2 = Sum L2
by Th13;
A49:
0. (W1 + W2) =
Sum (L (#) (F1 ^ F2))
by A30, A35, A36, Th5
.=
Sum ((L (#) F1) ^ (L (#) F2))
by VECTSP_6:37
.=
(Sum L1) + (Sum L2)
by A40, A46, RLVECT_1:58
;
then Sum L1 =
- (Sum L2)
by VECTSP_1:63
.=
- (Sum K2)
by A48, VECTSP_4:23
;
then
(
Sum K1 in W2 &
Sum K1 in W1 )
by A43, STRUCT_0:def 5;
then
Sum K1 in W1 /\ W2
by VECTSP_5:7;
then
Sum K1 in Lin I
by A2, VECTSP_7:def 3;
then consider KI being
Linear_Combination of
I such that A50:
Sum K1 = Sum KI
by VECTSP_7:12;
W1 /\ W2 is
Subspace of
W1 + W2
by VECTSP_5:29;
then consider LI being
Linear_Combination of
W1 + W2 such that A51:
Carrier LI = Carrier KI
and A52:
Sum LI = Sum KI
by Th12;
A53:
Carrier (LI + L2) c= (Carrier LI) \/ (Carrier L2)
by VECTSP_6:51;
A54:
I \/ I2 = I2
by A5, XBOOLE_1:12;
(
Carrier LI c= I &
Carrier L2 c= I2 )
by A32, A47, A51, VECTSP_6:def 7, XBOOLE_1:43;
then
(Carrier LI) \/ (Carrier L2) c= I2
by A54, XBOOLE_1:13;
then A55:
(
Carrier (LI + L2) c= I2 &
I2 c= the
carrier of
W2 )
by A53, XBOOLE_1:1;
then
Carrier (LI + L2) c= the
carrier of
W2
by XBOOLE_1:1;
then consider K being
Linear_Combination of
W2 such that A56:
Carrier K = Carrier (LI + L2)
and A57:
Sum K = Sum (LI + L2)
by A31, Th13;
reconsider K =
K as
Linear_Combination of
I2 by A55, A56, VECTSP_6:def 7;
(
I1 is
Subset of
W1 &
I1 is
linearly-independent )
by VECTSP_7:def 3;
then reconsider I1' =
I1 as
linearly-independent Subset of
(W1 + W2) by A31, Th15;
Carrier LI c= I
by A51, VECTSP_6:def 7;
then
Carrier LI c= I1'
by A4, XBOOLE_1:1;
then A58:
LI = L1
by A42, A43, A50, A52, MATRLIN:9;
A59:
I2 is
linearly-independent
by VECTSP_7:def 3;
0. W2 =
(Sum LI) + (Sum L2)
by A43, A49, A50, A52, VECTSP_4:20
.=
Sum K
by A57, VECTSP_6:77
;
then A60:
{} = Carrier (L1 + L2)
by A56, A58, A59, VECTSP_7:def 1;
A61:
Carrier L = (Carrier L1) \/ (Carrier L2)
by A41, A47, XBOOLE_1:51;
A62:
I1 misses (Carrier L) \ I1
by XBOOLE_1:79;
(Carrier L1) /\ (Carrier L2) =
(Carrier L) /\ (I1 /\ ((Carrier L) \ I1))
by A41, A47, XBOOLE_1:16
.=
(Carrier L) /\ {}
by A62, XBOOLE_0:def 7
.=
{}
;
then A63:
Carrier L1 misses Carrier L2
by XBOOLE_0:def 7;
hence
Carrier L = {}
by A60;
:: thesis: verum
end;
then
A is linearly-independent
by VECTSP_7:def 1;
then
A is Basis of W1 + W2
by A29, VECTSP_7:def 3;
then (dim (W1 + W2)) + (dim (W1 /\ W2)) =
(((card I1) + (card I2)) + (- (card I))) + (card I)
by A3, A20, Def2
.=
(dim W1) + (dim W2)
by A6, Def2
;
hence
(dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2)
; :: thesis: verum