let p be Prime; :: thesis: for V being free Z_Module
for I being Basis of V
for u1, u2 being VECTOR of V st u1 <> u2 & u1 in I & u2 in I holds
ZMtoMQV (V,p,u1) <> ZMtoMQV (V,p,u2)
let V be free Z_Module; :: thesis: for I being Basis of V
for u1, u2 being VECTOR of V st u1 <> u2 & u1 in I & u2 in I holds
ZMtoMQV (V,p,u1) <> ZMtoMQV (V,p,u2)
let I be Basis of V; :: thesis: for u1, u2 being VECTOR of V st u1 <> u2 & u1 in I & u2 in I holds
ZMtoMQV (V,p,u1) <> ZMtoMQV (V,p,u2)
let u1, u2 be VECTOR of V; :: thesis: ( u1 <> u2 & u1 in I & u2 in I implies ZMtoMQV (V,p,u1) <> ZMtoMQV (V,p,u2) )
assume A1: ( u1 <> u2 & u1 in I & u2 in I ) ; :: thesis: ZMtoMQV (V,p,u1) <> ZMtoMQV (V,p,u2)
set uq1 = ZMtoMQV (V,p,u1);
set uq2 = ZMtoMQV (V,p,u2);
assume A2: ZMtoMQV (V,p,u1) = ZMtoMQV (V,p,u2) ; :: thesis: contradiction
consider u being VECTOR of V such that
A3: ( u in p (*) V & u1 + u = u2 ) by A2, ZMODUL01:75;
A4: ( I is linearly-independent & Lin I = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ) by Def2;
u in p * V by A3;
then consider v being VECTOR of V such that
A5: u = p * v ;
consider lv being Z_Linear_Combination of I such that
A6: v = Sum lv by A4, STRUCT_0:def 5, ZMODUL02:64;
consider lu1 being Z_Linear_Combination of V such that
A7: ( lu1 . u1 = 1 & ( for v being VECTOR of V st v <> u1 holds
lu1 . v = 0 ) ) by Th1;
A8: Carrier lu1 = {u1}

proof

for v being object st v in Carrier lu1 holds
v in {u1}

proof

assume ex v being object st
( v in Carrier lu1 & not v in {u1} ) ; :: thesis: contradiction
then consider v being VECTOR of V such that
A9: ( v in Carrier lu1 & not v in {u1} ) ;
v <> u1 by A9, TARSKI:def 1;
then lu1 . v = 0 by A7;
hence contradiction by A9, ZMODUL02:8; :: thesis: verum

end;

then A10: Carrier lu1 c= {u1} ;
u1 in Carrier lu1 by A7;
then {u1} c= Carrier lu1 by ZFMISC_1:31;
hence Carrier lu1 = {u1} by A10, XBOOLE_0:def 10; :: thesis: verum

end;

then A11: Sum lu1 = 1 * u1 by A7, ZMODUL02:24
.= u1 by ZMODUL01:def 5 ;
reconsider lu1 = lu1 as Z_Linear_Combination of {u1} by A8, ZMODUL02:def 21;
reconsider lu1 = lu1 as Z_Linear_Combination of I by A1, ZFMISC_1:31, ZMODUL02:10;
consider lu2 being Z_Linear_Combination of V such that
A12: ( lu2 . u2 = 1 & ( for v being VECTOR of V st v <> u2 holds
lu2 . v = 0 ) ) by Th1;
A13: Carrier lu2 = {u2}

proof

for v being object st v in Carrier lu2 holds
v in {u2}

proof

assume ex v being object st
( v in Carrier lu2 & not v in {u2} ) ; :: thesis: contradiction
then consider v being VECTOR of V such that
A14: ( v in Carrier lu2 & not v in {u2} ) ;
v <> u2 by A14, TARSKI:def 1;
then lu2 . v = 0 by A12;
hence contradiction by A14, ZMODUL02:8; :: thesis: verum

end;

then A15: Carrier lu2 c= {u2} ;
u2 in Carrier lu2 by A12;
then {u2} c= Carrier lu2 by ZFMISC_1:31;
hence Carrier lu2 = {u2} by A15, XBOOLE_0:def 10; :: thesis: verum

end;

then A16: Sum lu2 = 1 * u2 by A12, ZMODUL02:24
.= u2 by ZMODUL01:def 5 ;
reconsider lu2 = lu2 as Z_Linear_Combination of {u2} by A13, ZMODUL02:def 21;
reconsider lu2 = lu2 as Z_Linear_Combination of I by A1, ZFMISC_1:31, ZMODUL02:10;
A17: u = Sum (p * lv) by A5, A6, ZMODUL02:53;
A18: (p * lv) . u1 <> - 1

proof

assume A19: (p * lv) . u1 = - 1 ; :: thesis: contradiction
( - p < - 1 & 0 > - 1 ) by INT_2:def 4, XREAL_1:24;
then (- 1) mod p = p + (- 1) by NAT_D:63;
then ((p * lv) . u1) mod p = p - 1 by A19;
then A20: ((p * lv) . u1) mod p <> 0 by INT_2:def 4;
A21: (p * lv) . u1 = p * (lv . u1) by ZMODUL02:def 26;
p divides ((p * lv) . u1) - 0 by A21, INT_1:60, INT_1:def 4;
hence contradiction by A20, INT_1:62; :: thesis: verum

end;

p * lv is Z_Linear_Combination of I by ZMODUL02:31;
then lu1 + (p * lv) is Z_Linear_Combination of I by ZMODUL02:27;
then reconsider lx = (lu1 + (p * lv)) - lu2 as Z_Linear_Combination of I by ZMODUL02:41;
A22: 0. V = (Sum (lu1 + (p * lv))) - (Sum lu2) by A3, A17, A11, A16, VECTSP_1:19, ZMODUL02:52
.= Sum lx by ZMODUL02:55 ;
A23: lx . u1 = ((lu1 + (p * lv)) . u1) - (lu2 . u1) by ZMODUL02:39
.= ((lu1 . u1) + ((p * lv) . u1)) - (lu2 . u1) by ZMODUL02:def 25
.= (1 + ((p * lv) . u1)) - 0 by A1, A7, A12
.= 1 + ((p * lv) . u1) ;
lx . u1 <> 0 by A18, A23;
then u1 in Carrier lx ;
hence contradiction by A22, Def2, ZMODUL02:def 36; :: thesis: verum