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 = ℤ ring freeLMod 0 1
Assertion zlmodzxzel ⊢ A ∈ ℤ ∧ B ∈ ℤ → 0 A 1 B ∈ Base Z

Proof

Step Hyp Ref Expression
1 zlmodzxz.z ⊢ Z = ℤ ring freeLMod 0 1
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 → 0 A 1 B : 0 1 ⟶ A B
7 4 5 6 mp3an13 ⊢ A ∈ ℤ ∧ B ∈ ℤ → 0 A 1 B : 0 1 ⟶ A B
8 prssi ⊢ A ∈ ℤ ∧ B ∈ ℤ → A B ⊆ ℤ
9 zringbas ⊢ ℤ = Base ℤ ring
10 8 9 sseqtrdi ⊢ A ∈ ℤ ∧ B ∈ ℤ → A B ⊆ Base ℤ ring
11 7 10 fssd ⊢ A ∈ ℤ ∧ B ∈ ℤ → 0 A 1 B : 0 1 ⟶ Base ℤ ring
12 fvex ⊢ Base ℤ ring ∈ V
13 prex ⊢ 0 1 ∈ V
14 12 13 pm3.2i ⊢ Base ℤ ring ∈ V ∧ 0 1 ∈ V
15 elmapg ⊢ Base ℤ ring ∈ V ∧ 0 1 ∈ V → 0 A 1 B ∈ Base ℤ ring 0 1 ↔ 0 A 1 B : 0 1 ⟶ Base ℤ ring
16 14 15 mp1i ⊢ A ∈ ℤ ∧ B ∈ ℤ → 0 A 1 B ∈ Base ℤ ring 0 1 ↔ 0 A 1 B : 0 1 ⟶ Base ℤ ring
17 11 16 mpbird ⊢ A ∈ ℤ ∧ B ∈ ℤ → 0 A 1 B ∈ Base ℤ ring 0 1
18 zringring ⊢ ℤ ring ∈ Ring
19 prfi ⊢ 0 1 ∈ Fin
20 18 19 pm3.2i ⊢ ℤ ring ∈ Ring ∧ 0 1 ∈ Fin
21 eqid ⊢ Base ℤ ring = Base ℤ ring
22 1 21 frlmfibas ⊢ ℤ ring ∈ Ring ∧ 0 1 ∈ Fin → Base ℤ ring 0 1 = Base Z
23 20 22 mp1i ⊢ A ∈ ℤ ∧ B ∈ ℤ → Base ℤ ring 0 1 = Base Z
24 17 23 eleqtrd ⊢ A ∈ ℤ ∧ B ∈ ℤ → 0 A 1 B ∈ Base Z