This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ( .g ‘ ℤring ) 𝐵 ) = ( 𝐴 · 𝐵 ) )

Proof

Step Hyp Ref Expression
1 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
2 zaddcl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 + 𝑦 ) ∈ ℤ )
3 znegcl ⊢ ( 𝑥 ∈ ℤ → - 𝑥 ∈ ℤ )
4 1z ⊢ 1 ∈ ℤ
5 1 2 3 4 cnsubglem ⊢ ℤ ∈ ( SubGrp ‘ ℂfld )
6 eqid ⊢ ( .g ‘ ℂfld ) = ( .g ‘ ℂfld )
7 df-zring ⊢ ℤring = ( ℂfld ↾s ℤ )
8 eqid ⊢ ( .g ‘ ℤring ) = ( .g ‘ ℤring )
9 6 7 8 subgmulg ⊢ ( ( ℤ ∈ ( SubGrp ‘ ℂfld ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝐴 ( .g ‘ ℤring ) 𝐵 ) )
10 5 9 mp3an1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝐴 ( .g ‘ ℤring ) 𝐵 ) )
11 simpr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℤ )
12 11 zcnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℂ )
13 cnfldmulg ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝐴 · 𝐵 ) )
14 12 13 syldan ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝐴 · 𝐵 ) )
15 10 14 eqtr3d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ( .g ‘ ℤring ) 𝐵 ) = ( 𝐴 · 𝐵 ) )