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
A2:
I is Basis of W1 /\ W2
by Def1;
A3:
card I = dim (W1 /\ W2)
by A2, Def3;
W1 /\ W2 is Subspace of W1
by RUSUB_2:16;
then consider I1 being Basis of W1 such that
A4:
I c= I1
by A2, RUSUB_3:24;
reconsider I1 = I1 as finite Subset of W1 by Th3;
W1 /\ W2 is Subspace of W2
by RUSUB_2:16;
then consider I2 being Basis of W2 such that
A5:
I c= I2
by A2, RUSUB_3:24;
reconsider I2 = I2 as finite Subset of W2 by Th3;
A6:
card I2 = dim W2
by Def3;
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 RUSUB_3:2;
then
(
x in UNITSTR(# the
carrier of
W1,the
U2 of
W1,the
addF of
W1,the
Mult of
W1,the
scalar of
W1 #) &
x in UNITSTR(# the
carrier of
W2,the
U2 of
W2,the
addF of
W2,the
Mult of
W2,the
scalar of
W2 #) )
by RUSUB_3:def 2;
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 RUSUB_2:def 2;
then
x in UNITSTR(# the
carrier of
(W1 /\ W2),the
U2 of
(W1 /\ W2),the
addF of
(W1 /\ W2),the
Mult of
(W1 /\ W2),the
scalar of
(W1 /\ W2) #)
by STRUCT_0:def 5;
then A14:
x in Lin I
by A2, RUSUB_3:def 2;
A15:
the
carrier of
W1 c= the
carrier of
V
by RUSUB_1:def 1;
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 RUSUB_1:def 1;
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 RUSUB_3:def 2;
then reconsider I1' =
I1 as
linearly-independent Subset of
V by RUSUB_3:22;
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, Lm2
;
then
not
x' in Lin I'
by A17, A18, RLVECT_3:6, RUSUB_3:25;
hence
contradiction
by A14, RUSUB_3:28;
:: thesis: verum end;
then
I = I1 /\ I2
by A10, XBOOLE_0:def 10;
then A19:
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 RUSUB_1:def 1;
then reconsider A' = A as Subset of V by XBOOLE_1:1;
A20:
Lin A' = Lin A
by RUSUB_3:28;
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 A21:
w1 in W1
and A22:
w2 in W2
and A23:
x = w1 + w2
by RUSUB_2:1;
reconsider w1 =
w1 as
VECTOR of
W1 by A21, STRUCT_0:def 5;
reconsider w2 =
w2 as
VECTOR of
W2 by A22, STRUCT_0:def 5;
w1 in Lin I1
by RUSUB_3:21;
then consider K1 being
Linear_Combination of
I1 such that A24:
w1 = Sum K1
by RUSUB_3:1;
consider L1 being
Linear_Combination of
V such that A25:
(
Carrier L1 = Carrier K1 &
Sum L1 = Sum K1 )
by RUSUB_3:19;
w2 in Lin I2
by RUSUB_3:21;
then consider K2 being
Linear_Combination of
I2 such that A26:
w2 = Sum K2
by RUSUB_3:1;
consider L2 being
Linear_Combination of
V such that A27:
(
Carrier L2 = Carrier K2 &
Sum L2 = Sum K2 )
by RUSUB_3:19;
set L =
L1 + L2;
(
Carrier L1 c= I1 &
Carrier L2 c= I2 )
by A25, A27, RLVECT_2:def 8;
then
(
Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) &
(Carrier L1) \/ (Carrier L2) c= I1 \/ I2 )
by RLVECT_2:58, 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 RLVECT_2:def 8;
x = Sum L
by A23, A24, A25, A26, A27, RLVECT_3:1;
then
x in Lin A'
by RUSUB_3:1;
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 RUSUB_1:22;
then A28:
Lin A = W1 + W2
by A20, RUSUB_1:20;
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 A29:
Sum L = 0. (W1 + W2)
;
:: thesis: Carrier L = {}
A30:
(
W1 is
Subspace of
W1 + W2 &
W2 is
Subspace of
W1 + W2 )
by RUSUB_2:7;
reconsider W1' =
W1 as
Subspace of
W1 + W2 by RUSUB_2:7;
reconsider W2' =
W2 as
Subspace of
W1 + W2 by RUSUB_2:7;
A31:
Carrier L c= I1 \/ I2
by RLVECT_2:def 8;
consider F being
FinSequence of the
carrier of
(W1 + W2) such that A32:
F is
one-to-one
and A33:
rng F = Carrier L
and A34:
Sum L = Sum (L (#) F)
by RLVECT_2:def 10;
set B =
(Carrier L) /\ I1;
reconsider B =
(Carrier L) /\ I1 as
Subset of
(rng F) by A33, XBOOLE_1:17;
consider P being
Permutation of
(dom F) such that A35:
(F - (B ` )) ^ (F - B) = F * P
by A32, FINSEQ_3:124;
reconsider F1 =
F - (B ` ),
F2 =
F - B as
FinSequence of the
carrier of
(W1 + W2) by FINSEQ_3:93;
A36:
(
F1 is
one-to-one &
F2 is
one-to-one )
by A32, FINSEQ_3:94;
consider L1 being
Linear_Combination of
W1 + W2 such that A37:
Carrier L1 = (rng F1) /\ (Carrier L)
and A38:
L1 (#) F1 = L (#) F1
by RLVECT_5:8;
A39:
Sum (L (#) F1) = Sum L1
by A36, A37, A38, RLVECT_5:7, 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 A40:
Carrier L1 =
I1 /\ ((Carrier L) /\ (Carrier L))
by A37, XBOOLE_1:16
.=
(Carrier L) /\ I1
;
then A41:
(
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 A42:
Sum K1 = Sum L1
by A40, RUSUB_3:20;
consider L2 being
Linear_Combination of
W1 + W2 such that A43:
Carrier L2 = (rng F2) /\ (Carrier L)
and A44:
L2 (#) F2 = L (#) F2
by RLVECT_5:8;
A45:
Sum (L (#) F2) = Sum L2
by A36, A43, A44, RLVECT_5:7, XBOOLE_1:17;
rng F2 =
(Carrier L) \ ((Carrier L) /\ I1)
by A33, FINSEQ_3:72
.=
(Carrier L) \ I1
by XBOOLE_1:47
;
then A46:
Carrier L2 = (Carrier L) \ I1
by A43, XBOOLE_1:28, XBOOLE_1:36;
then
(
Carrier L2 c= I2 &
I2 c= the
carrier of
W2 )
by A31, 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 A47:
Sum K2 = Sum L2
by RUSUB_3:20;
A48:
0. (W1 + W2) =
Sum (L (#) (F1 ^ F2))
by A29, A34, A35, RLVECT_5:5
.=
Sum ((L (#) F1) ^ (L (#) F2))
by RLVECT_3:41
.=
(Sum L1) + (Sum L2)
by A39, A45, RLVECT_1:58
;
then Sum L1 =
- (Sum L2)
by RLVECT_1:def 11
.=
- (Sum K2)
by A47, RUSUB_1:9
;
then
(
Sum K1 in W2 &
Sum K1 in W1 )
by A42, STRUCT_0:def 5;
then
Sum K1 in W1 /\ W2
by RUSUB_2:3;
then
Sum K1 in Lin I
by A2, RUSUB_3:def 2;
then consider KI being
Linear_Combination of
I such that A49:
Sum K1 = Sum KI
by RUSUB_3:1;
W1 /\ W2 is
Subspace of
W1 + W2
by RUSUB_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 RUSUB_3:19;
A52:
Carrier (LI + L2) c= (Carrier LI) \/ (Carrier L2)
by RLVECT_2:58;
A53:
I \/ I2 = I2
by A5, XBOOLE_1:12;
(
Carrier LI c= I &
Carrier L2 c= I2 )
by A31, A46, A50, RLVECT_2:def 8, XBOOLE_1:43;
then
(Carrier LI) \/ (Carrier L2) c= I2
by A53, XBOOLE_1:13;
then A54:
(
Carrier (LI + L2) c= I2 &
I2 c= the
carrier of
W2 )
by A52, 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 A55:
Carrier K = Carrier (LI + L2)
and A56:
Sum K = Sum (LI + L2)
by A30, RUSUB_3:20;
reconsider K =
K as
Linear_Combination of
I2 by A54, A55, RLVECT_2:def 8;
(
I1 is
Subset of
W1 &
I1 is
linearly-independent )
by RUSUB_3:def 2;
then reconsider I1' =
I1 as
linearly-independent Subset of
(W1 + W2) by A30, RUSUB_3:22;
Carrier LI c= I
by A50, RLVECT_2:def 8;
then
Carrier LI c= I1'
by A4, XBOOLE_1:1;
then A57:
LI = L1
by A41, A42, A49, A51, RLVECT_5:1;
A58:
I2 is
linearly-independent
by RUSUB_3:def 2;
0. W2 =
(Sum LI) + (Sum L2)
by A42, A48, A49, A51, RUSUB_1:5
.=
Sum K
by A56, RLVECT_3:1
;
then A59:
{} = Carrier (L1 + L2)
by A55, A57, A58, RLVECT_3:def 1;
A60:
Carrier L = (Carrier L1) \/ (Carrier L2)
by A40, A46, XBOOLE_1:51;
A61:
I1 misses (Carrier L) \ I1
by XBOOLE_1:79;
(Carrier L1) /\ (Carrier L2) =
(Carrier L) /\ (I1 /\ ((Carrier L) \ I1))
by A40, A46, XBOOLE_1:16
.=
(Carrier L) /\ {}
by A61, XBOOLE_0:def 7
.=
{}
;
then A62:
Carrier L1 misses Carrier L2
by XBOOLE_0:def 7;
hence
Carrier L = {}
by A59;
:: thesis: verum
end;
then
A is linearly-independent
by RLVECT_3:def 1;
then
A is Basis of W1 + W2
by A28, RUSUB_3:def 2;
then (dim (W1 + W2)) + (dim (W1 /\ W2)) =
(((card I1) + (card I2)) + (- (card I))) + (card I)
by A3, A19, Def3
.=
(dim W1) + (dim W2)
by A6, Def3
;
hence
(dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2)
; :: thesis: verum