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}
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. INT.Ring) * u1 by A7, ZMODUL02:24
.= 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
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. INT.Ring) * u2 by A12, ZMODUL02:24
.= 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
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;
pp * lv is Linear_Combination of I by ZMODUL02:31;
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