let V be finite-dimensional RealLinearSpace; 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; (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 I1 /\ I2 c= I
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
;
contradictionthen 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;
then reconsider Ix =
I \/ {x} as
Subset of
V by TARSKI:def 3;
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 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;
verum end;
set A = I1 \/ I2;
then reconsider A = I1 \/ I2 as finite Subset of (W1 + W2) by TARSKI:def 3;
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
(
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;
( Sum L = 0. (W1 + W2) implies Carrier L = {} )
assume A17:
Sum L = 0. (W1 + W2)
;
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;
A47:
I \/ I2 = I2
by A2, XBOOLE_1:12;
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;
verum
end;
then A56:
A is linearly-independent
by RLVECT_3:def 1;
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 for x being object st x in the carrier of (W1 + W2) holds
x in the carrier of (Lin A9)let x be
object ;
( x in the carrier of (W1 + W2) implies x in the carrier of (Lin A9) )assume
x in the
carrier of
(W1 + W2)
;
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;
verum end;
then
the carrier of (W1 + W2) c= the carrier of (Lin A9)
;
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; verum