let V be finite-dimensional RealUnitarySpace; 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 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 A1, RUSUB_3:24;
W1 /\ W2 is Subspace of W1
by RUSUB_2:16;
then consider I1 being Basis of W1 such that
A3:
I c= I1
by A1, RUSUB_3:24;
reconsider I2 = I2 as finite Subset of W2 by Th3;
reconsider I1 = I1 as finite Subset of W1 by Th3;
A4:
now 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
;
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 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;
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 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 A7, XBOOLE_0:def 4;
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 A1, RUSUB_3:def 2;
Ix \ {x} =
I \ {x}
by XBOOLE_1:40
.=
I
by A6, ZFMISC_1:57
;
then
not
x9 in Lin I9
by A10, A11, RLVECT_3:5, RUSUB_3:25;
hence
contradiction
by A12, RUSUB_3:28;
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;
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 RUSUB_2:7, RUSUB_3:def 2;
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;
( Sum L = 0. (W1 + W2) implies Carrier L = {} )
assume A16:
Sum L = 0. (W1 + W2)
;
Carrier L = {}
A17:
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 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 =
(Carrier L) /\ I1 as
Subset of
(rng F) by A19, 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 A21:
Carrier L1 = (rng F1) /\ (Carrier L)
and A22:
L1 (#) F1 = L (#) F1
by RLVECT_5:7;
F1 is
one-to-one
by A18, FINSEQ_3:87;
then A23:
Sum (L (#) F1) = Sum L1
by A21, A22, RLVECT_5:6, 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 A24:
Carrier L2 = (rng F2) /\ (Carrier L)
and A25:
L2 (#) F2 = L (#) F2
by RLVECT_5:7;
F2 is
one-to-one
by A18, FINSEQ_3:87;
then A26:
Sum (L (#) F2) = Sum L2
by A24, A25, RLVECT_5:6, 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 A27:
Carrier L1 =
I1 /\ ((Carrier L) /\ (Carrier L))
by A21, XBOOLE_1:16
.=
(Carrier L) /\ 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 =
(Carrier L) \ ((Carrier L) /\ I1)
by A19, FINSEQ_3:65
.=
(Carrier L) \ I1
by XBOOLE_1:47
;
then A29:
Carrier L2 = (Carrier L) \ I1
by A24, XBOOLE_1:28, XBOOLE_1:36;
then (Carrier L1) /\ (Carrier L2) =
(Carrier L) /\ (I1 /\ ((Carrier L) \ I1))
by A27, XBOOLE_1:16
.=
(Carrier L) /\ {}
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 A29, XBOOLE_1:43;
Carrier L2 c= I2
by A31, A29, XBOOLE_1:43;
then consider K2 being
Linear_Combination of
W29 such that
Carrier K2 = Carrier L2
and A33:
Sum K2 = Sum L2
by RUSUB_3:20, XBOOLE_1:1;
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 A16, A20, RLVECT_5:4
.=
Sum ((L (#) F1) ^ (L (#) F2))
by RLVECT_3:34
.=
(Sum L1) + (Sum L2)
by A23, A26, RLVECT_1:41
;
then Sum L1 =
- (Sum L2)
by RLVECT_1:def 10
.=
- (Sum K2)
by A33, RUSUB_1:9
;
then
Sum K1 in W2
by A28;
then
Sum K1 in W1 /\ W2
by A34, RUSUB_2:3;
then
Sum K1 in Lin I
by A1, RUSUB_3:def 2;
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 A27, A29, XBOOLE_1:51;
A46:
I \/ I2 = I2
by A2, XBOOLE_1:12;
A47:
I2 is
linearly-independent
by RUSUB_3:def 2;
A48:
Carrier L1 c= I1
by A27, XBOOLE_1:17;
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 A49, RLVECT_2:def 6;
then
Carrier LI c= I19
by A3;
then A51:
LI = L1
by A48, A28, A36, A50, RLVECT_5:1;
Carrier LI c= I
by A49, RLVECT_2:def 6;
then
(
Carrier (LI + L2) c= (Carrier LI) \/ (Carrier L2) &
(Carrier LI) \/ (Carrier L2) c= I2 )
by A46, A32, RLVECT_2:37, XBOOLE_1:13;
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 A52, RUSUB_3:20, XBOOLE_1:1;
reconsider K =
K as
Linear_Combination of
I2 by A52, A53, RLVECT_2:def 6;
0. W2 =
(Sum LI) + (Sum L2)
by A28, A35, A36, A50, RUSUB_1:5
.=
Sum K
by A54, RLVECT_3:1
;
then
{} = Carrier (L1 + L2)
by A53, A51, A47, RLVECT_3:def 1;
hence
Carrier L = {}
by A38;
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 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
;
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 A62, RLVECT_2:def 6;
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 A65, RLVECT_2:def 6;
then
(
Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) &
(Carrier L1) \/ (Carrier L2) c= I1 \/ I2 )
by A64, 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 A59, A60, A66, A61, A63, RLVECT_3:1;
then
x in Lin A9
by RUSUB_3:1;
hence
x in the
carrier of
(Lin A9)
;
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 RUSUB_1:22, RUSUB_3:28;
then
Lin A = W1 + W2
by RUSUB_1:20;
then A67:
A is Basis of W1 + W2
by A55, RUSUB_3:def 2;
card I = dim (W1 /\ W2)
by A1, Def2;
then (dim (W1 + W2)) + (dim (W1 /\ W2)) =
(((card I1) + (card I2)) + (- (card I))) + (card I)
by A15, A67, Def2
.=
(dim W1) + (dim W2)
by A56, Def2
;
hence
(dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2)
; verum