let p be prime Element of INT.Ring; :: 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 = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ) by VECTSP_7:def 3;

B1: u in p * V by A3;

reconsider pp = p as Element of INT.Ring ;

consider v being Vector of V such that

A5: u = pp * v by B1;

consider lv being Linear_Combination of I such that

A6: v = Sum lv by A4, STRUCT_0:def 5, ZMODUL02:64;

consider lu1 being 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}

.= u1 by VECTSP_1:def 17 ;

reconsider lu1 = lu1 as Linear_Combination of {u1} by A8, VECTSP_6:def 4;

reconsider lu1 = lu1 as Linear_Combination of I by A1, ZFMISC_1:31, ZMODUL02:10;

consider lu2 being 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}

.= u2 by VECTSP_1:def 17 ;

reconsider lu2 = lu2 as Linear_Combination of {u2} by A13, VECTSP_6:def 4;

reconsider lu2 = lu2 as 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

then lu1 + (pp * lv) is Linear_Combination of I by ZMODUL02:27;

then reconsider lx = (lu1 + (pp * lv)) - lu2 as Linear_Combination of I by ZMODUL02:41;

A22: 0. V = (Sum (lu1 + (pp * lv))) - (Sum lu2) by A3, A17, A11, A16, VECTSP_1:19, ZMODUL02:52

.= Sum lx by ZMODUL02:55 ;

A23: lx . u1 = ((lu1 + (pp * lv)) . u1) - (lu2 . u1) by ZMODUL02:39

.= ((lu1 . u1) + ((pp * lv) . u1)) - (lu2 . u1) by VECTSP_6:22

.= ((1. INT.Ring) + ((pp * lv) . u1)) - (0. INT.Ring) by A1, A7, A12

.= (1. INT.Ring) + ((pp * lv) . u1) ;

lx . u1 <> 0 by A18, A23;

then u1 in Carrier lx ;

hence contradiction by A22, VECTSP_7:def 3, VECTSP_7:def 1; :: thesis: verum

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 = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ) by VECTSP_7:def 3;

B1: u in p * V by A3;

reconsider pp = p as Element of INT.Ring ;

consider v being Vector of V such that

A5: u = pp * v by B1;

consider lv being Linear_Combination of I such that

A6: v = Sum lv by A4, STRUCT_0:def 5, ZMODUL02:64;

consider lu1 being 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

then A11: Sum lu1 =
(1. INT.Ring) * u1
by A7, ZMODUL02:24
for v being object st v in Carrier lu1 holds

v in {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;v in {u1}

proof

then A10:
Carrier lu1 c= {u1}
;
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;( 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

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

.= u1 by VECTSP_1:def 17 ;

reconsider lu1 = lu1 as Linear_Combination of {u1} by A8, VECTSP_6:def 4;

reconsider lu1 = lu1 as Linear_Combination of I by A1, ZFMISC_1:31, ZMODUL02:10;

consider lu2 being 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

then A16: Sum lu2 =
(1. INT.Ring) * u2
by A12, ZMODUL02:24
for v being object st v in Carrier lu2 holds

v in {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;v in {u2}

proof

then A15:
Carrier lu2 c= {u2}
;
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;( 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

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

.= u2 by VECTSP_1:def 17 ;

reconsider lu2 = lu2 as Linear_Combination of {u2} by A13, VECTSP_6:def 4;

reconsider lu2 = lu2 as 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

pp * lv is Linear_Combination of I
by ZMODUL02:31;
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;

reconsider pp = p as Element of INT.Ring ;

A21: (pp * lv) . u1 = pp * (lv . u1) by VECTSP_6:def 9;

pp divides ((pp * lv) . u1) - 0 by A21, INT_1:60, INT_1:def 4;

hence contradiction by A20, INT_1:62; :: thesis: verum

end;( - 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;

reconsider pp = p as Element of INT.Ring ;

A21: (pp * lv) . u1 = pp * (lv . u1) by VECTSP_6:def 9;

pp divides ((pp * lv) . u1) - 0 by A21, INT_1:60, INT_1:def 4;

hence contradiction by A20, INT_1:62; :: thesis: verum

then lu1 + (pp * lv) is Linear_Combination of I by ZMODUL02:27;

then reconsider lx = (lu1 + (pp * lv)) - lu2 as Linear_Combination of I by ZMODUL02:41;

A22: 0. V = (Sum (lu1 + (pp * lv))) - (Sum lu2) by A3, A17, A11, A16, VECTSP_1:19, ZMODUL02:52

.= Sum lx by ZMODUL02:55 ;

A23: lx . u1 = ((lu1 + (pp * lv)) . u1) - (lu2 . u1) by ZMODUL02:39

.= ((lu1 . u1) + ((pp * lv) . u1)) - (lu2 . u1) by VECTSP_6:22

.= ((1. INT.Ring) + ((pp * lv) . u1)) - (0. INT.Ring) by A1, A7, A12

.= (1. INT.Ring) + ((pp * lv) . u1) ;

lx . u1 <> 0 by A18, A23;

then u1 in Carrier lx ;

hence contradiction by A22, VECTSP_7:def 3, VECTSP_7:def 1; :: thesis: verum