Metamath Proof Explorer

Theorem zlmodzxzel

Description: An element of the (base set of the) ZZ-module ZZ X. ZZ . (Contributed by AV, 21-May-2019) (Revised by AV, 10-Jun-2019)

Ref Expression
Hypothesis zlmodzxz.z 
|- Z = ( ZZring freeLMod { 0 , 1 } )
Assertion zlmodzxzel 
|- ( ( A e. ZZ /\ B e. ZZ ) -> { <. 0 , A >. , <. 1 , B >. } e. ( Base ` Z ) )

Proof

Step Hyp Ref Expression
1 zlmodzxz.z 
 |-  Z = ( ZZring freeLMod { 0 , 1 } )
2 c0ex 
 |-  0 e. _V
3 1ex 
 |-  1 e. _V
4 2 3 pm3.2i 
 |-  ( 0 e. _V /\ 1 e. _V )
5 0ne1 
 |-  0 =/= 1
6 fprg 
 |-  ( ( ( 0 e. _V /\ 1 e. _V ) /\ ( A e. ZZ /\ B e. ZZ ) /\ 0 =/= 1 ) -> { <. 0 , A >. , <. 1 , B >. } : { 0 , 1 } --> { A , B } )
7 4 5 6 mp3an13 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> { <. 0 , A >. , <. 1 , B >. } : { 0 , 1 } --> { A , B } )
8 prssi 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> { A , B } C_ ZZ )
9 zringbas 
 |-  ZZ = ( Base ` ZZring )
10 8 9 sseqtrdi 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> { A , B } C_ ( Base ` ZZring ) )
11 7 10 fssd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> { <. 0 , A >. , <. 1 , B >. } : { 0 , 1 } --> ( Base ` ZZring ) )
12 fvex 
 |-  ( Base ` ZZring ) e. _V
13 prex 
 |-  { 0 , 1 } e. _V
14 12 13 pm3.2i 
 |-  ( ( Base ` ZZring ) e. _V /\ { 0 , 1 } e. _V )
15 elmapg 
 |-  ( ( ( Base ` ZZring ) e. _V /\ { 0 , 1 } e. _V ) -> ( { <. 0 , A >. , <. 1 , B >. } e. ( ( Base ` ZZring ) ^m { 0 , 1 } ) <-> { <. 0 , A >. , <. 1 , B >. } : { 0 , 1 } --> ( Base ` ZZring ) ) )
16 14 15 mp1i 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( { <. 0 , A >. , <. 1 , B >. } e. ( ( Base ` ZZring ) ^m { 0 , 1 } ) <-> { <. 0 , A >. , <. 1 , B >. } : { 0 , 1 } --> ( Base ` ZZring ) ) )
17 11 16 mpbird 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> { <. 0 , A >. , <. 1 , B >. } e. ( ( Base ` ZZring ) ^m { 0 , 1 } ) )
18 zringring 
 |-  ZZring e. Ring
19 prfi 
 |-  { 0 , 1 } e. Fin
20 18 19 pm3.2i 
 |-  ( ZZring e. Ring /\ { 0 , 1 } e. Fin )
21 eqid 
 |-  ( Base ` ZZring ) = ( Base ` ZZring )
22 1 21 frlmfibas 
 |-  ( ( ZZring e. Ring /\ { 0 , 1 } e. Fin ) -> ( ( Base ` ZZring ) ^m { 0 , 1 } ) = ( Base ` Z ) )
23 20 22 mp1i 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( Base ` ZZring ) ^m { 0 , 1 } ) = ( Base ` Z ) )
24 17 23 eleqtrd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> { <. 0 , A >. , <. 1 , B >. } e. ( Base ` Z ) )