let V be torsion-free Z_Module; :: thesis: 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; :: thesis: (rank (W1 + W2)) + (rank (W1 /\ W2)) = (rank W1) + (rank W2)
set W1W2 = W1 + W2;
reconsider W10 = W1 as free finite-rank Subspace of W1 + W2 by ZMODUL01:97;
reconsider W20 = W2 as free finite-rank Subspace of W1 + W2 by ZMODUL01:97;
R0: (rank (W10 + W20)) + (rank (W10 /\ W20)) = (rank W10) + (rank W20) by LmISRank501;
SB1: W10 + W20 is strict Subspace of V by ZMODUL01:42;
for v being Vector of V holds
( v in W10 + W20 iff v in W1 + W2 )
proof
let v be Vector of V; :: thesis: ( v in W10 + W20 iff v in W1 + W2 )
hereby :: thesis: ( v in W1 + W2 implies v in W10 + W20 )
assume v in W10 + W20 ; :: thesis: v in W1 + W2
then consider v1, v2 being Vector of (W1 + W2) such that
S11: ( v1 in W10 & v2 in W20 & v = v1 + v2 ) by ZMODUL01:92;
thus v in W1 + W2 by S11; :: thesis: verum
end;
assume v in W1 + W2 ; :: thesis: v in W10 + W20
then consider v1, v2 being Vector of V such that
S11: ( v1 in W1 & v2 in W2 & v = v1 + v2 ) by ZMODUL01:92;
( v1 in the carrier of W10 & v2 in the carrier of W20 ) by S11;
then reconsider v11 = v1, v22 = v2 as Vector of (W1 + W2) by ZMODUL01:25;
v11 + v22 = v1 + v2 by ZMODUL01:28;
hence v in W10 + W20 by S11, ZMODUL01:92; :: thesis: verum
end;
then R1: rank (W10 + W20) = rank (W1 + W2) by SB1, ZMODUL01:46;
SB2: W10 /\ W20 is strict Subspace of V by ZMODUL01:42;
for v being Vector of V holds
( v in W10 /\ W20 iff v in W1 /\ W2 )
proof
let v be Vector of V; :: thesis: ( v in W10 /\ W20 iff v in W1 /\ W2 )
hereby :: thesis: ( v in W1 /\ W2 implies v in W10 /\ W20 )
assume X1: v in W10 /\ W20 ; :: thesis: v in W1 /\ W2
then reconsider v0 = v as Vector of (W10 /\ W20) ;
( v0 in W10 & v0 in W20 ) by X1, ZMODUL01:94;
hence v in W1 /\ W2 by ZMODUL01:94; :: thesis: verum
end;
assume X1: v in W1 /\ W2 ; :: thesis: v in W10 /\ W20
then reconsider v0 = v as Vector of (W1 /\ W2) ;
( v in W1 & v in W2 ) by X1, ZMODUL01:94;
hence v in W10 /\ W20 by ZMODUL01:94; :: thesis: verum
end;
hence (rank (W1 + W2)) + (rank (W1 /\ W2)) = (rank W1) + (rank W2) by R1, R0, SB2, ZMODUL01:46; :: thesis: verum