Theorem zringsub

Description: The subtraction of elements in the ring of integers. (Contributed by AV, 24-Mar-2025)

	Ref	Expression
Hypothesis	zringsub.p	⊢ − = ( -g ‘ ℤring )
Assertion	zringsub	⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( 𝑋 − 𝑌 ) = ( 𝑋 − 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		zringsub.p	⊢ − = ( -g ‘ ℤring )
2		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
3		zaddcl	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 + 𝑦 ) ∈ ℤ )
4		znegcl	⊢ ( 𝑥 ∈ ℤ → - 𝑥 ∈ ℤ )
5		0z	⊢ 0 ∈ ℤ
6	2 3 4 5	cnsubglem	⊢ ℤ ∈ ( SubGrp ‘ ℂfld )
7		cnfldsub	⊢ − = ( -g ‘ ℂfld )
8		df-zring	⊢ ℤring = ( ℂfld ↾s ℤ )
9	7 8 1	subgsub	⊢ ( ( ℤ ∈ ( SubGrp ‘ ℂfld ) ∧ 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( 𝑋 − 𝑌 ) = ( 𝑋 − 𝑌 ) )
10	6 9	mp3an1	⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( 𝑋 − 𝑌 ) = ( 𝑋 − 𝑌 ) )
11	10	eqcomd	⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( 𝑋 − 𝑌 ) = ( 𝑋 − 𝑌 ) )