Metamath Proof Explorer

Theorem zlmodzxzldeplem1

Description: Lemma 1 for zlmodzxzldep . (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 >. }
zlmodzxzldeplem.f 
|- F = { <. A , 2 >. , <. B , -u 3 >. }
Assertion zlmodzxzldeplem1 
|- F e. ( ZZ ^m { 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 zlmodzxzldeplem.f 
 |-  F = { <. A , 2 >. , <. B , -u 3 >. }
5 zex 
 |-  ZZ e. _V
6 prex 
 |-  { A , B } e. _V
7 prex 
 |-  { <. 0 , 3 >. , <. 1 , 6 >. } e. _V
8 2 7 eqeltri 
 |-  A e. _V
9 prex 
 |-  { <. 0 , 2 >. , <. 1 , 4 >. } e. _V
10 3 9 eqeltri 
 |-  B e. _V
11 8 10 pm3.2i 
 |-  ( A e. _V /\ B e. _V )
12 11 a1i 
 |-  ( ( ZZ e. _V /\ { A , B } e. _V ) -> ( A e. _V /\ B e. _V ) )
13 2z 
 |-  2 e. ZZ
14 3nn0 
 |-  3 e. NN0
15 14 nn0negzi 
 |-  -u 3 e. ZZ
16 13 15 pm3.2i 
 |-  ( 2 e. ZZ /\ -u 3 e. ZZ )
17 16 a1i 
 |-  ( ( ZZ e. _V /\ { A , B } e. _V ) -> ( 2 e. ZZ /\ -u 3 e. ZZ ) )
18 1 2 3 zlmodzxzldeplem 
 |-  A =/= B
19 18 a1i 
 |-  ( ( ZZ e. _V /\ { A , B } e. _V ) -> A =/= B )
20 fprg 
 |-  ( ( ( A e. _V /\ B e. _V ) /\ ( 2 e. ZZ /\ -u 3 e. ZZ ) /\ A =/= B ) -> { <. A , 2 >. , <. B , -u 3 >. } : { A , B } --> { 2 , -u 3 } )
21 4 feq1i 
 |-  ( F : { A , B } --> { 2 , -u 3 } <-> { <. A , 2 >. , <. B , -u 3 >. } : { A , B } --> { 2 , -u 3 } )
22 20 21 sylibr 
 |-  ( ( ( A e. _V /\ B e. _V ) /\ ( 2 e. ZZ /\ -u 3 e. ZZ ) /\ A =/= B ) -> F : { A , B } --> { 2 , -u 3 } )
23 12 17 19 22 syl3anc 
 |-  ( ( ZZ e. _V /\ { A , B } e. _V ) -> F : { A , B } --> { 2 , -u 3 } )
24 prssi 
 |-  ( ( 2 e. ZZ /\ -u 3 e. ZZ ) -> { 2 , -u 3 } C_ ZZ )
25 13 15 24 mp2an 
 |-  { 2 , -u 3 } C_ ZZ
26 fss 
 |-  ( ( F : { A , B } --> { 2 , -u 3 } /\ { 2 , -u 3 } C_ ZZ ) -> F : { A , B } --> ZZ )
27 23 25 26 sylancl 
 |-  ( ( ZZ e. _V /\ { A , B } e. _V ) -> F : { A , B } --> ZZ )
28 elmapg 
 |-  ( ( ZZ e. _V /\ { A , B } e. _V ) -> ( F e. ( ZZ ^m { A , B } ) <-> F : { A , B } --> ZZ ) )
29 27 28 mpbird 
 |-  ( ( ZZ e. _V /\ { A , B } e. _V ) -> F e. ( ZZ ^m { A , B } ) )
30 5 6 29 mp2an 
 |-  F e. ( ZZ ^m { A , B } )