let V be free finite-rank Mult-cancelable Z_Module; for W1, W2 being free finite-rank Subspace of V holds (rank (W1 + W2)) + (rank (W1 /\ W2)) = (rank W1) + (rank W2)
let W1, W2 be free finite-rank Subspace of V; (rank (W1 + W2)) + (rank (W1 /\ W2)) = (rank W1) + (rank W2)
consider I1 being finite Subset of V such that
P1:
( I1 is finite Subset of W1 & I1 is linearly-independent & Lin I1 = (Omega). W1 & card I1 = rank W1 )
by LmFree2;
reconsider I1 = I1 as linearly-independent Subset of V by P1;
reconsider I10 = I1 as Basis of (Lin I1) by ThLin7;
consider I2 being finite Subset of V such that
P2:
( I2 is finite Subset of W2 & I2 is linearly-independent & Lin I2 = (Omega). W2 & card I2 = rank W2 )
by LmFree2;
reconsider I2 = I2 as linearly-independent Subset of V by P2;
reconsider I20 = I2 as Basis of (Lin I2) by ThLin7;
consider I1I2 being finite Subset of V such that
P3:
( I1I2 is finite Subset of (W1 + W2) & I1I2 is linearly-independent & Lin I1I2 = (Omega). (W1 + W2) & card I1I2 = rank (W1 + W2) )
by LmFree2;
reconsider I1I2 = I1I2 as linearly-independent Subset of V by P3;
reconsider I1I20 = I1I2 as Basis of (Lin I1I2) by ThLin7;
consider I12 being finite Subset of V such that
P4:
( I12 is finite Subset of (W1 /\ W2) & I12 is linearly-independent & Lin I12 = (Omega). (W1 /\ W2) & card I12 = rank (W1 /\ W2) )
by LmFree2;
set Iq1 = (MorphsZQ V) .: I1;
set Iq2 = (MorphsZQ V) .: I2;
set IIq12 = (MorphsZQ V) .: I1I2;
set Iq12 = (MorphsZQ V) .: I12;
reconsider Iq10 = (MorphsZQ V) .: I1 as Basis of (Lin ((MorphsZQ V) .: I1)) by ZMODUL04:11, VECT9Th26;
reconsider Iq20 = (MorphsZQ V) .: I2 as Basis of (Lin ((MorphsZQ V) .: I2)) by ZMODUL04:11, VECT9Th26;
reconsider IIq120 = (MorphsZQ V) .: I1I2 as Basis of (Lin ((MorphsZQ V) .: I1I2)) by ZMODUL04:11, VECT9Th26;
reconsider Iq120 = (MorphsZQ V) .: I12 as Basis of (Lin ((MorphsZQ V) .: I12)) by P4, ZMODUL04:11, VECT9Th26;
R1:
dim (Lin ((MorphsZQ V) .: I1)) = card ((MorphsZQ V) .: I1)
by VECTSP_9:26, ZMODUL04:11;
R2:
dim (Lin ((MorphsZQ V) .: I2)) = card ((MorphsZQ V) .: I2)
by VECTSP_9:26, ZMODUL04:11;
R3:
dim (Lin ((MorphsZQ V) .: I1I2)) = card ((MorphsZQ V) .: I1I2)
by VECTSP_9:26, ZMODUL04:11;
R4:
dim (Lin ((MorphsZQ V) .: I12)) = card ((MorphsZQ V) .: I12)
by P4, VECTSP_9:26, ZMODUL04:11;
Z0:
MorphsZQ V is one-to-one
by ZMODUL04:def 6;
S2:
dom (MorphsZQ V) = the carrier of V
by FUNCT_2:def 1;
D1:
dim (Lin ((MorphsZQ V) .: I1)) = rank W1
by P1, S2, CARD_1:5, Z0, CARD_1:33, R1;
D2:
dim (Lin ((MorphsZQ V) .: I2)) = rank W2
by P2, CARD_1:5, Z0, CARD_1:33, S2, R2;
D3:
dim (Lin ((MorphsZQ V) .: I1I2)) = rank (W1 + W2)
by P3, CARD_1:5, Z0, CARD_1:33, S2, R3;
D4:
dim (Lin ((MorphsZQ V) .: I12)) = rank (W1 /\ W2)
by P4, CARD_1:5, Z0, CARD_1:33, S2, R4;
for v being Vector of (Z_MQ_VectSp V) holds
( v in (Lin ((MorphsZQ V) .: I1)) + (Lin ((MorphsZQ V) .: I2)) iff v in Lin ((MorphsZQ V) .: I1I2) )
proof
let v be
Vector of
(Z_MQ_VectSp V);
( v in (Lin ((MorphsZQ V) .: I1)) + (Lin ((MorphsZQ V) .: I2)) iff v in Lin ((MorphsZQ V) .: I1I2) )
hereby ( v in Lin ((MorphsZQ V) .: I1I2) implies v in (Lin ((MorphsZQ V) .: I1)) + (Lin ((MorphsZQ V) .: I2)) )
assume
v in (Lin ((MorphsZQ V) .: I1)) + (Lin ((MorphsZQ V) .: I2))
;
v in Lin ((MorphsZQ V) .: I1I2)then consider v1,
v2 being
Vector of
(Z_MQ_VectSp V) such that PP1:
(
v1 in Lin ((MorphsZQ V) .: I1) &
v2 in Lin ((MorphsZQ V) .: I2) &
v = v1 + v2 )
by VECTSP_5:1;
consider lq1 being
Linear_Combination of
(MorphsZQ V) .: I1 such that PP2:
v1 = Sum lq1
by VECTSP_7:7, PP1;
consider lq2 being
Linear_Combination of
(MorphsZQ V) .: I2 such that PP3:
v2 = Sum lq2
by VECTSP_7:7, PP1;
consider m1 being
Element of
INT.Ring,
a1 being
Element of
F_Rat,
l1 being
Linear_Combination of
I1 such that PP4:
(
m1 <> 0 &
m1 = a1 &
l1 = (a1 * lq1) * (MorphsZQ V) &
(MorphsZQ V) " (Carrier lq1) = Carrier l1 )
by ZMODUL04:9;
PP5:
a1 * v1 = (MorphsZQ V) . (Sum l1)
by PP4, ZMODUL04:10, PP2;
consider m2 being
Element of
INT.Ring,
a2 being
Element of
F_Rat,
l2 being
Linear_Combination of
I2 such that PP6:
(
m2 <> 0 &
m2 = a2 &
l2 = (a2 * lq2) * (MorphsZQ V) &
(MorphsZQ V) " (Carrier lq2) = Carrier l2 )
by ZMODUL04:9;
PP7:
a2 * v2 = (MorphsZQ V) . (Sum l2)
by PP6, ZMODUL04:10, PP3;
PP8:
(a1 * a2) * v1 =
a2 * (a1 * v1)
by VECTSP_1:def 16
.=
(MorphsZQ V) . (m2 * (Sum l1))
by PP6, ZMODUL04:def 6, PP5
;
PP9:
(a1 * a2) * v2 =
a1 * (a2 * v2)
by VECTSP_1:def 16
.=
(MorphsZQ V) . (m1 * (Sum l2))
by PP4, ZMODUL04:def 6, PP7
;
PP10:
(a1 * a2) * (v1 + v2) =
((a1 * a2) * v1) + ((a1 * a2) * v2)
by VECTSP_1:def 14
.=
(MorphsZQ V) . ((m2 * (Sum l1)) + (m1 * (Sum l2)))
by ZMODUL04:def 6, PP8, PP9
;
Sum l1 in (Omega). W1
by P1, ZMODUL02:64;
then
Sum l1 in W1
;
then PP11:
m2 * (Sum l1) in W1
by ZMODUL01:37;
Sum l2 in Lin I2
by ZMODUL02:64;
then
Sum l2 in W2
by P2;
then
m1 * (Sum l2) in W2
by ZMODUL01:37;
then consider l12 being
Linear_Combination of
I1I2 such that PP13:
(m2 * (Sum l1)) + (m1 * (Sum l2)) = Sum l12
by ZMODUL02:64, P3, PP11, ZMODUL01:92;
reconsider r1 = 1 as
Element of
F_Rat ;
reconsider i1 = 1 as
Element of
INT.Ring ;
consider lq12 being
Linear_Combination of
(MorphsZQ V) .: I1I2 such that PP14:
(
l12 = lq12 * (MorphsZQ V) &
Carrier lq12 = (MorphsZQ V) .: (Carrier l12) )
by ZMODUL04:12;
r1 = 1. F_Rat
;
then
(
l12 = (r1 * lq12) * (MorphsZQ V) &
0 <> i1 &
r1 = i1 )
by PP14;
then Y1:
r1 * (Sum lq12) = (MorphsZQ V) . (Sum l12)
by ZMODUL04:10;
reconsider ra1 =
a1,
ra2 =
a2 as
Rational ;
Y3:
((ra1 * ra2) ") * (ra1 * ra2) = 1
by XCMPLX_0:def 7, PP4, PP6;
(a1 * a2) " = (ra1 * ra2) "
by GAUSSINT:15, PP4, PP6;
then Y2:
((a1 * a2) ") * (a1 * a2) = 1. F_Rat
by Y3;
X1X:
r1 * (Sum lq12) =
(1. F_Rat) * (Sum lq12)
.=
Sum lq12
by VECTSP_1:def 17
;
((a1 * a2) ") * ((a1 * a2) * (v1 + v2)) =
(((a1 * a2) ") * (a1 * a2)) * (v1 + v2)
by VECTSP_1:def 16
.=
v1 + v2
by VECTSP_1:def 17, Y2
;
hence
v in Lin ((MorphsZQ V) .: I1I2)
by X1X, PP1, VECTSP_4:21, VECTSP_7:7, PP13, PP10, Y1;
verum
end;
assume
v in Lin ((MorphsZQ V) .: I1I2)
;
v in (Lin ((MorphsZQ V) .: I1)) + (Lin ((MorphsZQ V) .: I2))
then consider lq12 being
Linear_Combination of
(MorphsZQ V) .: I1I2 such that PP2:
v = Sum lq12
by VECTSP_7:7;
consider m12 being
Element of
INT.Ring,
a12 being
Element of
F_Rat,
l12 being
Linear_Combination of
I1I2 such that PP4:
(
m12 <> 0 &
m12 = a12 &
l12 = (a12 * lq12) * (MorphsZQ V) &
(MorphsZQ V) " (Carrier lq12) = Carrier l12 )
by ZMODUL04:9;
PP5:
a12 * v = (MorphsZQ V) . (Sum l12)
by PP4, ZMODUL04:10, PP2;
consider v1,
v2 being
Vector of
V such that PP1:
(
v1 in W1 &
v2 in W2 &
Sum l12 = v1 + v2 )
by ZMODUL01:92, P3, ZMODUL02:64;
v1 in (Omega). W1
by PP1;
then consider l1 being
Linear_Combination of
I1 such that PP13:
v1 = Sum l1
by ZMODUL02:64, P1;
v2 in (Omega). W2
by PP1;
then consider l2 being
Linear_Combination of
I2 such that PP14:
v2 = Sum l2
by ZMODUL02:64, P2;
Y1:
a12 * v = ((MorphsZQ V) . (Sum l1)) + ((MorphsZQ V) . (Sum l2))
by ZMODUL04:def 6, PP1, PP5, PP13, PP14;
consider lq1 being
Linear_Combination of
(MorphsZQ V) .: I1 such that PP15:
(
l1 = lq1 * (MorphsZQ V) &
Carrier lq1 = (MorphsZQ V) .: (Carrier l1) )
by ZMODUL04:12;
consider lq2 being
Linear_Combination of
(MorphsZQ V) .: I2 such that PP16:
(
l2 = lq2 * (MorphsZQ V) &
Carrier lq2 = (MorphsZQ V) .: (Carrier l2) )
by ZMODUL04:12;
Y3:
Sum lq2 = (MorphsZQ V) . (Sum l2)
by PP16, ZMODUL04:7;
Y4:
a12 * v = (Sum lq1) + (Sum lq2)
by Y1, PP15, ZMODUL04:7, Y3;
reconsider w1 =
Sum lq1 as
Vector of
(Z_MQ_VectSp V) ;
reconsider w2 =
Sum lq2 as
Vector of
(Z_MQ_VectSp V) ;
(
w1 in Lin ((MorphsZQ V) .: I1) &
w2 in Lin ((MorphsZQ V) .: I2) )
by VECTSP_7:7;
then Y5:
a12 * v in (Lin ((MorphsZQ V) .: I1)) + (Lin ((MorphsZQ V) .: I2))
by Y4, VECTSP_5:1;
reconsider ra12 =
a12 as
Rational ;
Y7:
(ra12 ") * ra12 = 1
by XCMPLX_0:def 7, PP4;
a12 " = ra12 "
by PP4, GAUSSINT:15;
then Y8:
(a12 ") * a12 = 1. F_Rat
by Y7;
(a12 ") * (a12 * v) in (Lin ((MorphsZQ V) .: I1)) + (Lin ((MorphsZQ V) .: I2))
by Y5, VECTSP_4:21;
then
(1. F_Rat) * v in (Lin ((MorphsZQ V) .: I1)) + (Lin ((MorphsZQ V) .: I2))
by Y8, VECTSP_1:def 16;
hence
v in (Lin ((MorphsZQ V) .: I1)) + (Lin ((MorphsZQ V) .: I2))
by VECTSP_1:def 17;
verum
end;
then E1:
(Lin ((MorphsZQ V) .: I1)) + (Lin ((MorphsZQ V) .: I2)) = Lin ((MorphsZQ V) .: I1I2)
by VECTSP_4:30;
for v being Vector of (Z_MQ_VectSp V) holds
( v in (Lin ((MorphsZQ V) .: I1)) /\ (Lin ((MorphsZQ V) .: I2)) iff v in Lin ((MorphsZQ V) .: I12) )
proof
let v be
Vector of
(Z_MQ_VectSp V);
( v in (Lin ((MorphsZQ V) .: I1)) /\ (Lin ((MorphsZQ V) .: I2)) iff v in Lin ((MorphsZQ V) .: I12) )
hereby ( v in Lin ((MorphsZQ V) .: I12) implies v in (Lin ((MorphsZQ V) .: I1)) /\ (Lin ((MorphsZQ V) .: I2)) )
assume
v in (Lin ((MorphsZQ V) .: I1)) /\ (Lin ((MorphsZQ V) .: I2))
;
v in Lin ((MorphsZQ V) .: I12)then PP1:
(
v in Lin ((MorphsZQ V) .: I1) &
v in Lin ((MorphsZQ V) .: I2) )
by VECTSP_5:3;
consider lq1 being
Linear_Combination of
(MorphsZQ V) .: I1 such that PP2:
v = Sum lq1
by VECTSP_7:7, PP1;
consider lq2 being
Linear_Combination of
(MorphsZQ V) .: I2 such that PP3:
v = Sum lq2
by VECTSP_7:7, PP1;
consider m1 being
Element of
INT.Ring,
a1 being
Element of
F_Rat,
l1 being
Linear_Combination of
I1 such that PP4:
(
m1 <> 0 &
m1 = a1 &
l1 = (a1 * lq1) * (MorphsZQ V) &
(MorphsZQ V) " (Carrier lq1) = Carrier l1 )
by ZMODUL04:9;
PP5:
a1 * v = (MorphsZQ V) . (Sum l1)
by PP4, ZMODUL04:10, PP2;
consider m2 being
Element of
INT.Ring,
a2 being
Element of
F_Rat,
l2 being
Linear_Combination of
I2 such that PP6:
(
m2 <> 0 &
m2 = a2 &
l2 = (a2 * lq2) * (MorphsZQ V) &
(MorphsZQ V) " (Carrier lq2) = Carrier l2 )
by ZMODUL04:9;
PP7:
a2 * v = (MorphsZQ V) . (Sum l2)
by PP6, ZMODUL04:10, PP3;
PP8:
(a1 * a2) * v =
a2 * (a1 * v)
by VECTSP_1:def 16
.=
(MorphsZQ V) . (m2 * (Sum l1))
by PP6, ZMODUL04:def 6, PP5
;
PP9:
(a1 * a2) * v =
a1 * (a2 * v)
by VECTSP_1:def 16
.=
(MorphsZQ V) . (m1 * (Sum l2))
by PP4, ZMODUL04:def 6, PP7
;
MorphsZQ V is
one-to-one
by ZMODUL04:def 6;
then PP10:
m1 * (Sum l2) = m2 * (Sum l1)
by FUNCT_2:19, PP8, PP9;
Sum l1 in Lin I1
by ZMODUL02:64;
then
Sum l1 in W1
by P1;
then PP11:
m2 * (Sum l1) in W1
by ZMODUL01:37;
Sum l2 in (Omega). W2
by P2, ZMODUL02:64;
then
Sum l2 in W2
;
then
m1 * (Sum l2) in W2
by ZMODUL01:37;
then consider l12 being
Linear_Combination of
I12 such that PP13:
m2 * (Sum l1) = Sum l12
by ZMODUL02:64, P4, PP10, PP11, ZMODUL01:94;
reconsider r1 = 1 as
Element of
F_Rat ;
reconsider i1 = 1 as
Element of
INT.Ring ;
consider lq12 being
Linear_Combination of
(MorphsZQ V) .: I12 such that PP14:
(
l12 = lq12 * (MorphsZQ V) &
Carrier lq12 = (MorphsZQ V) .: (Carrier l12) )
by ZMODUL04:12;
r1 = 1. F_Rat
;
then
(
l12 = (r1 * lq12) * (MorphsZQ V) &
0 <> i1 &
r1 = i1 )
by PP14;
then Y1:
r1 * (Sum lq12) = (MorphsZQ V) . (Sum l12)
by ZMODUL04:10;
reconsider ra1 =
a1,
ra2 =
a2 as
Rational ;
Y3:
((ra1 * ra2) ") * (ra1 * ra2) = 1
by XCMPLX_0:def 7, PP4, PP6;
(a1 * a2) " = (ra1 * ra2) "
by PP4, PP6, GAUSSINT:15;
then Y2:
((a1 * a2) ") * (a1 * a2) = 1. F_Rat
by Y3;
X1X:
r1 * (Sum lq12) =
(1. F_Rat) * (Sum lq12)
.=
Sum lq12
by VECTSP_1:def 17
;
((a1 * a2) ") * ((a1 * a2) * v) =
(((a1 * a2) ") * (a1 * a2)) * v
by VECTSP_1:def 16
.=
v
by VECTSP_1:def 17, Y2
;
hence
v in Lin ((MorphsZQ V) .: I12)
by X1X, VECTSP_4:21, VECTSP_7:7, PP8, PP13, Y1;
verum
end;
assume
v in Lin ((MorphsZQ V) .: I12)
;
v in (Lin ((MorphsZQ V) .: I1)) /\ (Lin ((MorphsZQ V) .: I2))
then consider lq12 being
Linear_Combination of
(MorphsZQ V) .: I12 such that PP2:
v = Sum lq12
by VECTSP_7:7;
consider m12 being
Element of
INT.Ring,
a12 being
Element of
F_Rat,
l12 being
Linear_Combination of
I12 such that PP4:
(
m12 <> 0 &
m12 = a12 &
l12 = (a12 * lq12) * (MorphsZQ V) &
(MorphsZQ V) " (Carrier lq12) = Carrier l12 )
by ZMODUL04:9;
PP5:
a12 * v = (MorphsZQ V) . (Sum l12)
by PP4, ZMODUL04:10, PP2;
Sum l12 in (Omega). (W1 /\ W2)
by P4, ZMODUL02:64;
then PP1:
(
Sum l12 in W1 &
Sum l12 in W2 )
by ZMODUL01:94;
Sum l12 in (Omega). W1
by PP1;
then consider l1 being
Linear_Combination of
I1 such that PP13:
Sum l12 = Sum l1
by ZMODUL02:64, P1;
Sum l12 in (Omega). W2
by PP1;
then consider l2 being
Linear_Combination of
I2 such that PP14:
Sum l12 = Sum l2
by ZMODUL02:64, P2;
consider lq1 being
Linear_Combination of
(MorphsZQ V) .: I1 such that PP15:
(
l1 = lq1 * (MorphsZQ V) &
Carrier lq1 = (MorphsZQ V) .: (Carrier l1) )
by ZMODUL04:12;
consider lq2 being
Linear_Combination of
(MorphsZQ V) .: I2 such that PP16:
(
l2 = lq2 * (MorphsZQ V) &
Carrier lq2 = (MorphsZQ V) .: (Carrier l2) )
by ZMODUL04:12;
Y4:
(
a12 * v = Sum lq1 &
a12 * v = Sum lq2 )
by PP5, PP13, PP14, PP15, PP16, ZMODUL04:7;
reconsider w1 =
Sum lq1 as
Vector of
(Z_MQ_VectSp V) ;
reconsider w2 =
Sum lq2 as
Vector of
(Z_MQ_VectSp V) ;
(
w1 in Lin ((MorphsZQ V) .: I1) &
w2 in Lin ((MorphsZQ V) .: I2) )
by VECTSP_7:7;
then Y5:
a12 * v in (Lin ((MorphsZQ V) .: I1)) /\ (Lin ((MorphsZQ V) .: I2))
by Y4, VECTSP_5:3;
reconsider ra12 =
a12 as
Rational ;
Y7:
(ra12 ") * ra12 = 1
by XCMPLX_0:def 7, PP4;
a12 " = ra12 "
by PP4, GAUSSINT:15;
then Y8:
(a12 ") * a12 = 1. F_Rat
by Y7;
(a12 ") * (a12 * v) in (Lin ((MorphsZQ V) .: I1)) /\ (Lin ((MorphsZQ V) .: I2))
by Y5, VECTSP_4:21;
then
((a12 ") * a12) * v in (Lin ((MorphsZQ V) .: I1)) /\ (Lin ((MorphsZQ V) .: I2))
by VECTSP_1:def 16;
hence
v in (Lin ((MorphsZQ V) .: I1)) /\ (Lin ((MorphsZQ V) .: I2))
by VECTSP_1:def 17, Y8;
verum
end;
then
(Lin ((MorphsZQ V) .: I1)) /\ (Lin ((MorphsZQ V) .: I2)) = Lin ((MorphsZQ V) .: I12)
by VECTSP_4:30;
hence
(rank (W1 + W2)) + (rank (W1 /\ W2)) = (rank W1) + (rank W2)
by VECTSP_9:32, E1, D1, D2, D3, D4; verum