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 ) 𝐵 ) = ( 𝐴 · 𝐵 ) )