Theorem resubgval

Description: Subtraction in the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019)

	Ref	Expression
Hypothesis	resubgval.m	⊢ − = ( -g ‘ ℝfld )
Assertion	resubgval	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑋 − 𝑌 ) = ( 𝑋 − 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		resubgval.m	⊢ − = ( -g ‘ ℝfld )
2		resubdrg	⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) ∧ ℝfld ∈ DivRing )
3	2	simpli	⊢ ℝ ∈ ( SubRing ‘ ℂfld )
4		subrgsubg	⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) → ℝ ∈ ( SubGrp ‘ ℂfld ) )
5	3 4	ax-mp	⊢ ℝ ∈ ( SubGrp ‘ ℂfld )
6		cnfldsub	⊢ − = ( -g ‘ ℂfld )
7		df-refld	⊢ ℝfld = ( ℂfld ↾s ℝ )
8	6 7 1	subgsub	⊢ ( ( ℝ ∈ ( SubGrp ‘ ℂfld ) ∧ 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑋 − 𝑌 ) = ( 𝑋 − 𝑌 ) )
9	5 8	mp3an1	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑋 − 𝑌 ) = ( 𝑋 − 𝑌 ) )