Metamath Proof Explorer

Theorem zlmodzxznm

Description: Example of a linearly dependent set whose elements are not linear combinations of the others, see note in Roman p. 112). (Contributed by AV, 23-May-2019) (Revised by AV, 10-Jun-2019)

Ref Expression
Hypotheses zlmodzxzequa.z 
|- Z = ( ZZring freeLMod { 0 , 1 } )
zlmodzxzequa.o 
|- .0. = { <. 0 , 0 >. , <. 1 , 0 >. }
zlmodzxzequa.t 
|- .xb = ( .s ` Z )
zlmodzxzequa.m 
|- .- = ( -g ` Z )
zlmodzxzequa.a 
|- A = { <. 0 , 3 >. , <. 1 , 6 >. }
zlmodzxzequa.b 
|- B = { <. 0 , 2 >. , <. 1 , 4 >. }
Assertion zlmodzxznm 
|- A. i e. ZZ ( ( i .xb A ) =/= B /\ ( i .xb B ) =/= A )

Proof

Step Hyp Ref Expression
1 zlmodzxzequa.z 
 |-  Z = ( ZZring freeLMod { 0 , 1 } )
2 zlmodzxzequa.o 
 |-  .0. = { <. 0 , 0 >. , <. 1 , 0 >. }
3 zlmodzxzequa.t 
 |-  .xb = ( .s ` Z )
4 zlmodzxzequa.m 
 |-  .- = ( -g ` Z )
5 zlmodzxzequa.a 
 |-  A = { <. 0 , 3 >. , <. 1 , 6 >. }
6 zlmodzxzequa.b 
 |-  B = { <. 0 , 2 >. , <. 1 , 4 >. }
7 3prm 
 |-  3 e. Prime
8 2prm 
 |-  2 e. Prime
9 ztprmneprm 
 |-  ( ( i e. ZZ /\ 3 e. Prime /\ 2 e. Prime ) -> ( ( i x. 3 ) = 2 -> 3 = 2 ) )
10 7 8 9 mp3an23 
 |-  ( i e. ZZ -> ( ( i x. 3 ) = 2 -> 3 = 2 ) )
11 2re 
 |-  2 e. RR
12 2lt3 
 |-  2 < 3
13 11 12 ltneii 
 |-  2 =/= 3
14 eqneqall 
 |-  ( 2 = 3 -> ( 2 =/= 3 -> ( i x. 3 ) =/= 2 ) )
15 13 14 mpi 
 |-  ( 2 = 3 -> ( i x. 3 ) =/= 2 )
16 15 eqcoms 
 |-  ( 3 = 2 -> ( i x. 3 ) =/= 2 )
17 10 16 syl6com 
 |-  ( ( i x. 3 ) = 2 -> ( i e. ZZ -> ( i x. 3 ) =/= 2 ) )
18 ax-1 
 |-  ( ( i x. 3 ) =/= 2 -> ( i e. ZZ -> ( i x. 3 ) =/= 2 ) )
19 17 18 pm2.61ine 
 |-  ( i e. ZZ -> ( i x. 3 ) =/= 2 )
20 19 olcd 
 |-  ( i e. ZZ -> ( 0 =/= 0 \/ ( i x. 3 ) =/= 2 ) )
21 c0ex 
 |-  0 e. _V
22 ovex 
 |-  ( i x. 3 ) e. _V
23 21 22 pm3.2i 
 |-  ( 0 e. _V /\ ( i x. 3 ) e. _V )
24 opthneg 
 |-  ( ( 0 e. _V /\ ( i x. 3 ) e. _V ) -> ( <. 0 , ( i x. 3 ) >. =/= <. 0 , 2 >. <-> ( 0 =/= 0 \/ ( i x. 3 ) =/= 2 ) ) )
25 23 24 mp1i 
 |-  ( i e. ZZ -> ( <. 0 , ( i x. 3 ) >. =/= <. 0 , 2 >. <-> ( 0 =/= 0 \/ ( i x. 3 ) =/= 2 ) ) )
26 20 25 mpbird 
 |-  ( i e. ZZ -> <. 0 , ( i x. 3 ) >. =/= <. 0 , 2 >. )
27 0ne1 
 |-  0 =/= 1
28 27 a1i 
 |-  ( i e. ZZ -> 0 =/= 1 )
29 28 orcd 
 |-  ( i e. ZZ -> ( 0 =/= 1 \/ ( i x. 3 ) =/= 4 ) )
30 opthneg 
 |-  ( ( 0 e. _V /\ ( i x. 3 ) e. _V ) -> ( <. 0 , ( i x. 3 ) >. =/= <. 1 , 4 >. <-> ( 0 =/= 1 \/ ( i x. 3 ) =/= 4 ) ) )
31 23 30 mp1i 
 |-  ( i e. ZZ -> ( <. 0 , ( i x. 3 ) >. =/= <. 1 , 4 >. <-> ( 0 =/= 1 \/ ( i x. 3 ) =/= 4 ) ) )
32 29 31 mpbird 
 |-  ( i e. ZZ -> <. 0 , ( i x. 3 ) >. =/= <. 1 , 4 >. )
33 26 32 jca 
 |-  ( i e. ZZ -> ( <. 0 , ( i x. 3 ) >. =/= <. 0 , 2 >. /\ <. 0 , ( i x. 3 ) >. =/= <. 1 , 4 >. ) )
34 33 orcd 
 |-  ( i e. ZZ -> ( ( <. 0 , ( i x. 3 ) >. =/= <. 0 , 2 >. /\ <. 0 , ( i x. 3 ) >. =/= <. 1 , 4 >. ) \/ ( <. 1 , ( i x. 6 ) >. =/= <. 0 , 2 >. /\ <. 1 , ( i x. 6 ) >. =/= <. 1 , 4 >. ) ) )
35 opex 
 |-  <. 0 , ( i x. 3 ) >. e. _V
36 opex 
 |-  <. 1 , ( i x. 6 ) >. e. _V
37 35 36 pm3.2i 
 |-  ( <. 0 , ( i x. 3 ) >. e. _V /\ <. 1 , ( i x. 6 ) >. e. _V )
38 37 a1i 
 |-  ( i e. ZZ -> ( <. 0 , ( i x. 3 ) >. e. _V /\ <. 1 , ( i x. 6 ) >. e. _V ) )
39 opex 
 |-  <. 0 , 2 >. e. _V
40 opex 
 |-  <. 1 , 4 >. e. _V
41 39 40 pm3.2i 
 |-  ( <. 0 , 2 >. e. _V /\ <. 1 , 4 >. e. _V )
42 41 a1i 
 |-  ( i e. ZZ -> ( <. 0 , 2 >. e. _V /\ <. 1 , 4 >. e. _V ) )
43 28 orcd 
 |-  ( i e. ZZ -> ( 0 =/= 1 \/ ( i x. 3 ) =/= ( i x. 6 ) ) )
44 opthneg 
 |-  ( ( 0 e. _V /\ ( i x. 3 ) e. _V ) -> ( <. 0 , ( i x. 3 ) >. =/= <. 1 , ( i x. 6 ) >. <-> ( 0 =/= 1 \/ ( i x. 3 ) =/= ( i x. 6 ) ) ) )
45 23 44 mp1i 
 |-  ( i e. ZZ -> ( <. 0 , ( i x. 3 ) >. =/= <. 1 , ( i x. 6 ) >. <-> ( 0 =/= 1 \/ ( i x. 3 ) =/= ( i x. 6 ) ) ) )
46 43 45 mpbird 
 |-  ( i e. ZZ -> <. 0 , ( i x. 3 ) >. =/= <. 1 , ( i x. 6 ) >. )
47 prnebg 
 |-  ( ( ( <. 0 , ( i x. 3 ) >. e. _V /\ <. 1 , ( i x. 6 ) >. e. _V ) /\ ( <. 0 , 2 >. e. _V /\ <. 1 , 4 >. e. _V ) /\ <. 0 , ( i x. 3 ) >. =/= <. 1 , ( i x. 6 ) >. ) -> ( ( ( <. 0 , ( i x. 3 ) >. =/= <. 0 , 2 >. /\ <. 0 , ( i x. 3 ) >. =/= <. 1 , 4 >. ) \/ ( <. 1 , ( i x. 6 ) >. =/= <. 0 , 2 >. /\ <. 1 , ( i x. 6 ) >. =/= <. 1 , 4 >. ) ) <-> { <. 0 , ( i x. 3 ) >. , <. 1 , ( i x. 6 ) >. } =/= { <. 0 , 2 >. , <. 1 , 4 >. } ) )
48 47 bicomd 
 |-  ( ( ( <. 0 , ( i x. 3 ) >. e. _V /\ <. 1 , ( i x. 6 ) >. e. _V ) /\ ( <. 0 , 2 >. e. _V /\ <. 1 , 4 >. e. _V ) /\ <. 0 , ( i x. 3 ) >. =/= <. 1 , ( i x. 6 ) >. ) -> ( { <. 0 , ( i x. 3 ) >. , <. 1 , ( i x. 6 ) >. } =/= { <. 0 , 2 >. , <. 1 , 4 >. } <-> ( ( <. 0 , ( i x. 3 ) >. =/= <. 0 , 2 >. /\ <. 0 , ( i x. 3 ) >. =/= <. 1 , 4 >. ) \/ ( <. 1 , ( i x. 6 ) >. =/= <. 0 , 2 >. /\ <. 1 , ( i x. 6 ) >. =/= <. 1 , 4 >. ) ) ) )
49 38 42 46 48 syl3anc 
 |-  ( i e. ZZ -> ( { <. 0 , ( i x. 3 ) >. , <. 1 , ( i x. 6 ) >. } =/= { <. 0 , 2 >. , <. 1 , 4 >. } <-> ( ( <. 0 , ( i x. 3 ) >. =/= <. 0 , 2 >. /\ <. 0 , ( i x. 3 ) >. =/= <. 1 , 4 >. ) \/ ( <. 1 , ( i x. 6 ) >. =/= <. 0 , 2 >. /\ <. 1 , ( i x. 6 ) >. =/= <. 1 , 4 >. ) ) ) )
50 34 49 mpbird 
 |-  ( i e. ZZ -> { <. 0 , ( i x. 3 ) >. , <. 1 , ( i x. 6 ) >. } =/= { <. 0 , 2 >. , <. 1 , 4 >. } )
51 5 oveq2i 
 |-  ( i .xb A ) = ( i .xb { <. 0 , 3 >. , <. 1 , 6 >. } )
52 3z 
 |-  3 e. ZZ
53 6nn 
 |-  6 e. NN
54 53 nnzi 
 |-  6 e. ZZ
55 1 3 zlmodzxzscm 
 |-  ( ( i e. ZZ /\ 3 e. ZZ /\ 6 e. ZZ ) -> ( i .xb { <. 0 , 3 >. , <. 1 , 6 >. } ) = { <. 0 , ( i x. 3 ) >. , <. 1 , ( i x. 6 ) >. } )
56 52 54 55 mp3an23 
 |-  ( i e. ZZ -> ( i .xb { <. 0 , 3 >. , <. 1 , 6 >. } ) = { <. 0 , ( i x. 3 ) >. , <. 1 , ( i x. 6 ) >. } )
57 51 56 syl5eq 
 |-  ( i e. ZZ -> ( i .xb A ) = { <. 0 , ( i x. 3 ) >. , <. 1 , ( i x. 6 ) >. } )
58 6 a1i 
 |-  ( i e. ZZ -> B = { <. 0 , 2 >. , <. 1 , 4 >. } )
59 50 57 58 3netr4d 
 |-  ( i e. ZZ -> ( i .xb A ) =/= B )
60 ztprmneprm 
 |-  ( ( i e. ZZ /\ 2 e. Prime /\ 3 e. Prime ) -> ( ( i x. 2 ) = 3 -> 2 = 3 ) )
61 8 7 60 mp3an23 
 |-  ( i e. ZZ -> ( ( i x. 2 ) = 3 -> 2 = 3 ) )
62 eqneqall 
 |-  ( 2 = 3 -> ( 2 =/= 3 -> ( i x. 2 ) =/= 3 ) )
63 13 62 mpi 
 |-  ( 2 = 3 -> ( i x. 2 ) =/= 3 )
64 61 63 syl6com 
 |-  ( ( i x. 2 ) = 3 -> ( i e. ZZ -> ( i x. 2 ) =/= 3 ) )
65 ax-1 
 |-  ( ( i x. 2 ) =/= 3 -> ( i e. ZZ -> ( i x. 2 ) =/= 3 ) )
66 64 65 pm2.61ine 
 |-  ( i e. ZZ -> ( i x. 2 ) =/= 3 )
67 66 olcd 
 |-  ( i e. ZZ -> ( 0 =/= 0 \/ ( i x. 2 ) =/= 3 ) )
68 ovex 
 |-  ( i x. 2 ) e. _V
69 21 68 pm3.2i 
 |-  ( 0 e. _V /\ ( i x. 2 ) e. _V )
70 opthneg 
 |-  ( ( 0 e. _V /\ ( i x. 2 ) e. _V ) -> ( <. 0 , ( i x. 2 ) >. =/= <. 0 , 3 >. <-> ( 0 =/= 0 \/ ( i x. 2 ) =/= 3 ) ) )
71 69 70 mp1i 
 |-  ( i e. ZZ -> ( <. 0 , ( i x. 2 ) >. =/= <. 0 , 3 >. <-> ( 0 =/= 0 \/ ( i x. 2 ) =/= 3 ) ) )
72 67 71 mpbird 
 |-  ( i e. ZZ -> <. 0 , ( i x. 2 ) >. =/= <. 0 , 3 >. )
73 28 orcd 
 |-  ( i e. ZZ -> ( 0 =/= 1 \/ ( i x. 2 ) =/= 6 ) )
74 opthneg 
 |-  ( ( 0 e. _V /\ ( i x. 2 ) e. _V ) -> ( <. 0 , ( i x. 2 ) >. =/= <. 1 , 6 >. <-> ( 0 =/= 1 \/ ( i x. 2 ) =/= 6 ) ) )
75 69 74 mp1i 
 |-  ( i e. ZZ -> ( <. 0 , ( i x. 2 ) >. =/= <. 1 , 6 >. <-> ( 0 =/= 1 \/ ( i x. 2 ) =/= 6 ) ) )
76 73 75 mpbird 
 |-  ( i e. ZZ -> <. 0 , ( i x. 2 ) >. =/= <. 1 , 6 >. )
77 72 76 jca 
 |-  ( i e. ZZ -> ( <. 0 , ( i x. 2 ) >. =/= <. 0 , 3 >. /\ <. 0 , ( i x. 2 ) >. =/= <. 1 , 6 >. ) )
78 77 orcd 
 |-  ( i e. ZZ -> ( ( <. 0 , ( i x. 2 ) >. =/= <. 0 , 3 >. /\ <. 0 , ( i x. 2 ) >. =/= <. 1 , 6 >. ) \/ ( <. 1 , ( i x. 4 ) >. =/= <. 0 , 3 >. /\ <. 1 , ( i x. 4 ) >. =/= <. 1 , 6 >. ) ) )
79 opex 
 |-  <. 0 , ( i x. 2 ) >. e. _V
80 opex 
 |-  <. 1 , ( i x. 4 ) >. e. _V
81 79 80 pm3.2i 
 |-  ( <. 0 , ( i x. 2 ) >. e. _V /\ <. 1 , ( i x. 4 ) >. e. _V )
82 81 a1i 
 |-  ( i e. ZZ -> ( <. 0 , ( i x. 2 ) >. e. _V /\ <. 1 , ( i x. 4 ) >. e. _V ) )
83 opex 
 |-  <. 0 , 3 >. e. _V
84 opex 
 |-  <. 1 , 6 >. e. _V
85 83 84 pm3.2i 
 |-  ( <. 0 , 3 >. e. _V /\ <. 1 , 6 >. e. _V )
86 85 a1i 
 |-  ( i e. ZZ -> ( <. 0 , 3 >. e. _V /\ <. 1 , 6 >. e. _V ) )
87 28 orcd 
 |-  ( i e. ZZ -> ( 0 =/= 1 \/ ( i x. 2 ) =/= ( i x. 4 ) ) )
88 opthneg 
 |-  ( ( 0 e. _V /\ ( i x. 2 ) e. _V ) -> ( <. 0 , ( i x. 2 ) >. =/= <. 1 , ( i x. 4 ) >. <-> ( 0 =/= 1 \/ ( i x. 2 ) =/= ( i x. 4 ) ) ) )
89 69 88 mp1i 
 |-  ( i e. ZZ -> ( <. 0 , ( i x. 2 ) >. =/= <. 1 , ( i x. 4 ) >. <-> ( 0 =/= 1 \/ ( i x. 2 ) =/= ( i x. 4 ) ) ) )
90 87 89 mpbird 
 |-  ( i e. ZZ -> <. 0 , ( i x. 2 ) >. =/= <. 1 , ( i x. 4 ) >. )
91 prnebg 
 |-  ( ( ( <. 0 , ( i x. 2 ) >. e. _V /\ <. 1 , ( i x. 4 ) >. e. _V ) /\ ( <. 0 , 3 >. e. _V /\ <. 1 , 6 >. e. _V ) /\ <. 0 , ( i x. 2 ) >. =/= <. 1 , ( i x. 4 ) >. ) -> ( ( ( <. 0 , ( i x. 2 ) >. =/= <. 0 , 3 >. /\ <. 0 , ( i x. 2 ) >. =/= <. 1 , 6 >. ) \/ ( <. 1 , ( i x. 4 ) >. =/= <. 0 , 3 >. /\ <. 1 , ( i x. 4 ) >. =/= <. 1 , 6 >. ) ) <-> { <. 0 , ( i x. 2 ) >. , <. 1 , ( i x. 4 ) >. } =/= { <. 0 , 3 >. , <. 1 , 6 >. } ) )
92 91 bicomd 
 |-  ( ( ( <. 0 , ( i x. 2 ) >. e. _V /\ <. 1 , ( i x. 4 ) >. e. _V ) /\ ( <. 0 , 3 >. e. _V /\ <. 1 , 6 >. e. _V ) /\ <. 0 , ( i x. 2 ) >. =/= <. 1 , ( i x. 4 ) >. ) -> ( { <. 0 , ( i x. 2 ) >. , <. 1 , ( i x. 4 ) >. } =/= { <. 0 , 3 >. , <. 1 , 6 >. } <-> ( ( <. 0 , ( i x. 2 ) >. =/= <. 0 , 3 >. /\ <. 0 , ( i x. 2 ) >. =/= <. 1 , 6 >. ) \/ ( <. 1 , ( i x. 4 ) >. =/= <. 0 , 3 >. /\ <. 1 , ( i x. 4 ) >. =/= <. 1 , 6 >. ) ) ) )
93 82 86 90 92 syl3anc 
 |-  ( i e. ZZ -> ( { <. 0 , ( i x. 2 ) >. , <. 1 , ( i x. 4 ) >. } =/= { <. 0 , 3 >. , <. 1 , 6 >. } <-> ( ( <. 0 , ( i x. 2 ) >. =/= <. 0 , 3 >. /\ <. 0 , ( i x. 2 ) >. =/= <. 1 , 6 >. ) \/ ( <. 1 , ( i x. 4 ) >. =/= <. 0 , 3 >. /\ <. 1 , ( i x. 4 ) >. =/= <. 1 , 6 >. ) ) ) )
94 78 93 mpbird 
 |-  ( i e. ZZ -> { <. 0 , ( i x. 2 ) >. , <. 1 , ( i x. 4 ) >. } =/= { <. 0 , 3 >. , <. 1 , 6 >. } )
95 6 oveq2i 
 |-  ( i .xb B ) = ( i .xb { <. 0 , 2 >. , <. 1 , 4 >. } )
96 2z 
 |-  2 e. ZZ
97 4z 
 |-  4 e. ZZ
98 1 3 zlmodzxzscm 
 |-  ( ( i e. ZZ /\ 2 e. ZZ /\ 4 e. ZZ ) -> ( i .xb { <. 0 , 2 >. , <. 1 , 4 >. } ) = { <. 0 , ( i x. 2 ) >. , <. 1 , ( i x. 4 ) >. } )
99 96 97 98 mp3an23 
 |-  ( i e. ZZ -> ( i .xb { <. 0 , 2 >. , <. 1 , 4 >. } ) = { <. 0 , ( i x. 2 ) >. , <. 1 , ( i x. 4 ) >. } )
100 95 99 syl5eq 
 |-  ( i e. ZZ -> ( i .xb B ) = { <. 0 , ( i x. 2 ) >. , <. 1 , ( i x. 4 ) >. } )
101 5 a1i 
 |-  ( i e. ZZ -> A = { <. 0 , 3 >. , <. 1 , 6 >. } )
102 94 100 101 3netr4d 
 |-  ( i e. ZZ -> ( i .xb B ) =/= A )
103 59 102 jca 
 |-  ( i e. ZZ -> ( ( i .xb A ) =/= B /\ ( i .xb B ) =/= A ) )
104 103 rgen 
 |-  A. i e. ZZ ( ( i .xb A ) =/= B /\ ( i .xb B ) =/= A )