let V be Z_Module; :: thesis: for W1, W2, W3 being free finite-rank Subspace of V
for a being Element of INT.Ring st a <> 0. INT.Ring & W3 = a (*) W1 holds
rank (W3 /\ W2) = rank (W1 /\ W2)
let W1, W2, W3 be free finite-rank Subspace of V; :: thesis: for a being Element of INT.Ring st a <> 0. INT.Ring & W3 = a (*) W1 holds
rank (W3 /\ W2) = rank (W1 /\ W2)
let a be Element of INT.Ring; :: thesis: ( a <> 0. INT.Ring & W3 = a (*) W1 implies rank (W3 /\ W2) = rank (W1 /\ W2) )
assume A1: ( a <> 0. INT.Ring & W3 = a (*) W1 ) ; :: thesis: rank (W3 /\ W2) = rank (W1 /\ W2)
W3 /\ W2 is Subspace of W1 /\ W2

proof

W3 /\ W2 is Subspace of W3 by ZMODUL01:105;
then B2: W3 /\ W2 is Subspace of W1 by A1, ZMODUL01:42;
W3 /\ W2 is Subspace of W2 by ZMODUL01:105;
hence W3 /\ W2 is Subspace of W1 /\ W2 by B2, ZMODUL02:75; :: thesis: verum

end;

then A2: rank (W3 /\ W2) <= rank (W1 /\ W2) by ZMODUL05:2;
a (*) (W1 /\ W2) is Subspace of W3 /\ W2

proof

reconsider WX = a (*) (W1 /\ W2) as Subspace of V by ZMODUL01:42;
for v being Vector of V st v in WX holds
v in W3 /\ W2

proof

let v be Vector of V; :: thesis: ( v in WX implies v in W3 /\ W2 )
assume C1: v in WX ; :: thesis: v in W3 /\ W2
consider vx being Vector of (W1 /\ W2) such that
C2: v = a * vx by C1;
reconsider vvx = vx as Vector of V by ZMODUL01:25;
CX: vvx in W1 /\ W2 ;
then vvx in W1 by ZMODUL01:94;
then reconsider vvvx = vvx as Vector of W1 ;
a * vvvx in a * W1 ;
then a * vvx in W3 by A1, ZMODUL01:29;
then C3: v in W3 by C2, ZMODUL01:29;
vvx in W2 by CX, ZMODUL01:94;
then a * vvx in W2 by ZMODUL01:37;
then v in W2 by C2, ZMODUL01:29;
hence v in W3 /\ W2 by C3, ZMODUL01:94; :: thesis: verum

end;

hence a (*) (W1 /\ W2) is Subspace of W3 /\ W2 by ZMODUL01:44; :: thesis: verum

end;

then rank (a (*) (W1 /\ W2)) <= rank (W3 /\ W2) by ZMODUL05:2;
then rank (W1 /\ W2) <= rank (W3 /\ W2) by A1, ThRankS1;
hence rank (W3 /\ W2) = rank (W1 /\ W2) by A2, XXREAL_0:1; :: thesis: verum