Metamath Proof Explorer

Theorem zlmodzxzldeplem

Description: A and B are not equal. (Contributed by AV, 24-May-2019) (Revised by AV, 10-Jun-2019)

Ref Expression
Hypotheses zlmodzxzldep.z 
|- Z = ( ZZring freeLMod { 0 , 1 } )
zlmodzxzldep.a 
|- A = { <. 0 , 3 >. , <. 1 , 6 >. }
zlmodzxzldep.b 
|- B = { <. 0 , 2 >. , <. 1 , 4 >. }
Assertion zlmodzxzldeplem 
|- A =/= B

Proof

Step Hyp Ref Expression
1 zlmodzxzldep.z 
 |-  Z = ( ZZring freeLMod { 0 , 1 } )
2 zlmodzxzldep.a 
 |-  A = { <. 0 , 3 >. , <. 1 , 6 >. }
3 zlmodzxzldep.b 
 |-  B = { <. 0 , 2 >. , <. 1 , 4 >. }
4 opex 
 |-  <. 0 , 3 >. e. _V
5 opex 
 |-  <. 1 , 6 >. e. _V
6 4 5 pm3.2i 
 |-  ( <. 0 , 3 >. e. _V /\ <. 1 , 6 >. e. _V )
7 opex 
 |-  <. 0 , 2 >. e. _V
8 opex 
 |-  <. 1 , 4 >. e. _V
9 7 8 pm3.2i 
 |-  ( <. 0 , 2 >. e. _V /\ <. 1 , 4 >. e. _V )
10 6 9 pm3.2i 
 |-  ( ( <. 0 , 3 >. e. _V /\ <. 1 , 6 >. e. _V ) /\ ( <. 0 , 2 >. e. _V /\ <. 1 , 4 >. e. _V ) )
11 2re 
 |-  2 e. RR
12 2lt3 
 |-  2 < 3
13 11 12 gtneii 
 |-  3 =/= 2
14 13 olci 
 |-  ( 0 =/= 0 \/ 3 =/= 2 )
15 c0ex 
 |-  0 e. _V
16 3ex 
 |-  3 e. _V
17 15 16 opthne 
 |-  ( <. 0 , 3 >. =/= <. 0 , 2 >. <-> ( 0 =/= 0 \/ 3 =/= 2 ) )
18 14 17 mpbir 
 |-  <. 0 , 3 >. =/= <. 0 , 2 >.
19 0ne1 
 |-  0 =/= 1
20 19 orci 
 |-  ( 0 =/= 1 \/ 3 =/= 4 )
21 15 16 opthne 
 |-  ( <. 0 , 3 >. =/= <. 1 , 4 >. <-> ( 0 =/= 1 \/ 3 =/= 4 ) )
22 20 21 mpbir 
 |-  <. 0 , 3 >. =/= <. 1 , 4 >.
23 18 22 pm3.2i 
 |-  ( <. 0 , 3 >. =/= <. 0 , 2 >. /\ <. 0 , 3 >. =/= <. 1 , 4 >. )
24 23 orci 
 |-  ( ( <. 0 , 3 >. =/= <. 0 , 2 >. /\ <. 0 , 3 >. =/= <. 1 , 4 >. ) \/ ( <. 1 , 6 >. =/= <. 0 , 2 >. /\ <. 1 , 6 >. =/= <. 1 , 4 >. ) )
25 prneimg 
 |-  ( ( ( <. 0 , 3 >. e. _V /\ <. 1 , 6 >. e. _V ) /\ ( <. 0 , 2 >. e. _V /\ <. 1 , 4 >. e. _V ) ) -> ( ( ( <. 0 , 3 >. =/= <. 0 , 2 >. /\ <. 0 , 3 >. =/= <. 1 , 4 >. ) \/ ( <. 1 , 6 >. =/= <. 0 , 2 >. /\ <. 1 , 6 >. =/= <. 1 , 4 >. ) ) -> { <. 0 , 3 >. , <. 1 , 6 >. } =/= { <. 0 , 2 >. , <. 1 , 4 >. } ) )
26 10 24 25 mp2 
 |-  { <. 0 , 3 >. , <. 1 , 6 >. } =/= { <. 0 , 2 >. , <. 1 , 4 >. }
27 2 3 neeq12i 
 |-  ( A =/= B <-> { <. 0 , 3 >. , <. 1 , 6 >. } =/= { <. 0 , 2 >. , <. 1 , 4 >. } )
28 26 27 mpbir 
 |-  A =/= B