Metamath Proof Explorer

Theorem zringmulg

Description: The multiplication (group power) operation of the group of integers. (Contributed by Thierry Arnoux, 31-Oct-2017) (Revised by AV, 9-Jun-2019)

Ref Expression
Assertion zringmulg ⊢ A ∈ ℤ ∧ B ∈ ℤ → A ⋅ ℤ ring B = A ⁢ B

Proof

Step Hyp Ref Expression
1 zcn ⊢ x ∈ ℤ → x ∈ ℂ
2 zaddcl ⊢ x ∈ ℤ ∧ y ∈ ℤ → x + y ∈ ℤ
3 znegcl ⊢ x ∈ ℤ → − x ∈ ℤ
4 1z ⊢ 1 ∈ ℤ
5 1 2 3 4 cnsubglem ⊢ ℤ ∈ SubGrp ⁡ ℂ fld
6 eqid ⊢ ⋅ ℂ fld = ⋅ ℂ fld
7 df-zring ⊢ ℤ ring = ℂ fld ↾ 𝑠 ℤ
8 eqid ⊢ ⋅ ℤ ring = ⋅ ℤ ring
9 6 7 8 subgmulg ⊢ ℤ ∈ SubGrp ⁡ ℂ fld ∧ A ∈ ℤ ∧ B ∈ ℤ → A ⋅ ℂ fld B = A ⋅ ℤ ring B
10 5 9 mp3an1 ⊢ A ∈ ℤ ∧ B ∈ ℤ → A ⋅ ℂ fld B = A ⋅ ℤ ring B
11 simpr ⊢ A ∈ ℤ ∧ B ∈ ℤ → B ∈ ℤ
12 11 zcnd ⊢ A ∈ ℤ ∧ B ∈ ℤ → B ∈ ℂ
13 cnfldmulg ⊢ A ∈ ℤ ∧ B ∈ ℂ → A ⋅ ℂ fld B = A ⁢ B
14 12 13 syldan ⊢ A ∈ ℤ ∧ B ∈ ℤ → A ⋅ ℂ fld B = A ⁢ B
15 10 14 eqtr3d ⊢ A ∈ ℤ ∧ B ∈ ℤ → A ⋅ ℤ ring B = A ⁢ B