Theorem sn-00idlem1

Description: Lemma for sn-00id . (Contributed by SN, 25-Dec-2023)

	Ref	Expression
Assertion	sn-00idlem1	$$⊢A\in ℝ\to A\left(0{-}_{ℝ}0\right)=A{-}_{ℝ}A$$

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2		resubdi	$$⊢\left(A\in ℝ\wedge 1\in ℝ\wedge 1\in ℝ\right)\to A\left(1{-}_{ℝ}1\right)=A\cdot 1{-}_{ℝ}A\cdot 1$$
3	1 1 2	mp3an23	$$⊢A\in ℝ\to A\left(1{-}_{ℝ}1\right)=A\cdot 1{-}_{ℝ}A\cdot 1$$
4		re1m1e0m0	$$⊢1{-}_{ℝ}1=0{-}_{ℝ}0$$
5	4	oveq2i	$$⊢A\left(1{-}_{ℝ}1\right)=A\left(0{-}_{ℝ}0\right)$$
6	5	a1i	$$⊢A\in ℝ\to A\left(1{-}_{ℝ}1\right)=A\left(0{-}_{ℝ}0\right)$$
7		ax-1rid	$$⊢A\in ℝ\to A\cdot 1=A$$
8	7 7	oveq12d	$$⊢A\in ℝ\to A\cdot 1{-}_{ℝ}A\cdot 1=A{-}_{ℝ}A$$
9	3 6 8	3eqtr3d	$$⊢A\in ℝ\to A\left(0{-}_{ℝ}0\right)=A{-}_{ℝ}A$$