let V be Z_Module; for z1, z2 being Element of V
for i1, i2 being Element of INT.Ring st V is Mult-cancelable holds
( [[z1,i1],[z2,i2]] in EQRZM V iff ( i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) )
let z1, z2 be Element of V; for i1, i2 being Element of INT.Ring st V is Mult-cancelable holds
( [[z1,i1],[z2,i2]] in EQRZM V iff ( i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) )
let i1, i2 be Element of INT.Ring; ( V is Mult-cancelable implies ( [[z1,i1],[z2,i2]] in EQRZM V iff ( i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ) )
assume AS:
V is Mult-cancelable
; ( [[z1,i1],[z2,i2]] in EQRZM V iff ( i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) )
hereby ( i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 implies [[z1,i1],[z2,i2]] in EQRZM V )
assume
[[z1,i1],[z2,i2]] in EQRZM V
;
( i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 )then consider zz1,
zz2 being
Element of
V,
ii1,
ii2 being
Element of
INT.Ring such that P2:
(
[z1,i1] = [zz1,ii1] &
[z2,i2] = [zz2,ii2] &
ii1 <> 0 &
ii2 <> 0 &
ii2 * zz1 = ii1 * zz2 )
by AS, defEQRZM;
(
z1 = zz1 &
i1 = ii1 &
z2 = zz2 &
i2 = ii2 )
by P2, XTUPLE_0:1;
hence
(
i1 <> 0 &
i2 <> 0 &
i2 * z1 = i1 * z2 )
by P2;
verum
end;
assume A2:
( i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 )
; [[z1,i1],[z2,i2]] in EQRZM V
then A21:
( not i1 in {0} & not i2 in {0} )
by TARSKI:def 1;
( i1 in INT \ {0} & i2 in INT \ {0} )
by XBOOLE_0:def 5, A21;
then
( [z1,i1] in [: the carrier of V,(INT \ {0}):] & [z2,i2] in [: the carrier of V,(INT \ {0}):] )
by ZFMISC_1:87;
hence
[[z1,i1],[z2,i2]] in EQRZM V
by A2, AS, defEQRZM; verum