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=ℤringfreeLMod01
Assertion zlmodzxzel ⊢A∈ℤ∧B∈ℤ→0A1B∈BaseZ

Proof

Step Hyp Ref Expression
1 zlmodzxz.z ⊢Z=ℤringfreeLMod01
2 c0ex ⊢0∈V
3 1ex ⊢1∈V
4 2 3 pm3.2i ⊢0∈V∧1∈V
5 0ne1 ⊢0≠1
6 fprg ⊢0∈V∧1∈V∧A∈ℤ∧B∈ℤ∧0≠1→0A1B:01⟶AB
7 4 5 6 mp3an13 ⊢A∈ℤ∧B∈ℤ→0A1B:01⟶AB
8 prssi ⊢A∈ℤ∧B∈ℤ→AB⊆ℤ
9 zringbas ⊢ℤ=Baseℤring
10 8 9 sseqtrdi ⊢A∈ℤ∧B∈ℤ→AB⊆Baseℤring
11 7 10 fssd ⊢A∈ℤ∧B∈ℤ→0A1B:01⟶Baseℤring
12 fvex ⊢Baseℤring∈V
13 prex ⊢01∈V
14 12 13 pm3.2i ⊢Baseℤring∈V∧01∈V
15 elmapg ⊢Baseℤring∈V∧01∈V→0A1B∈Baseℤring01↔0A1B:01⟶Baseℤring
16 14 15 mp1i ⊢A∈ℤ∧B∈ℤ→0A1B∈Baseℤring01↔0A1B:01⟶Baseℤring
17 11 16 mpbird ⊢A∈ℤ∧B∈ℤ→0A1B∈Baseℤring01
18 zringring ⊢ℤring∈Ring
19 prfi ⊢01∈Fin
20 18 19 pm3.2i ⊢ℤring∈Ring∧01∈Fin
21 eqid ⊢Baseℤring=Baseℤring
22 1 21 frlmfibas ⊢ℤring∈Ring∧01∈Fin→Baseℤring01=BaseZ
23 20 22 mp1i ⊢A∈ℤ∧B∈ℤ→Baseℤring01=BaseZ
24 17 23 eleqtrd ⊢A∈ℤ∧B∈ℤ→0A1B∈BaseZ