Theorem re1m1e0m0

Description: Equality of two left-additive identities. See resubidaddid1 . Uses ax-i2m1 . (Contributed by SN, 25-Dec-2023)

	Ref	Expression
Assertion	re1m1e0m0	$$⊢1{-}_{ℝ}1=0{-}_{ℝ}0$$

Proof

Step	Hyp	Ref	Expression
1		0red	$$⊢\top \to 0\in ℝ$$
2		1re	$$⊢1\in ℝ$$
3		rersubcl	$$⊢\left(1\in ℝ\wedge 1\in ℝ\right)\to 1{-}_{ℝ}1\in ℝ$$
4	2 2 3	mp2an	$$⊢1{-}_{ℝ}1\in ℝ$$
5	4	a1i	$$⊢\top \to 1{-}_{ℝ}1\in ℝ$$
6		ax-icn	$$⊢\mathrm{i}\in ℂ$$
7	6 6	mulcli	$$⊢\mathrm{i}\mathrm{i}\in ℂ$$
8		ax-1cn	$$⊢1\in ℂ$$
9	4	recni	$$⊢1{-}_{ℝ}1\in ℂ$$
10	7 8 9	addassi	$$⊢\mathrm{i}\mathrm{i}+1+\left(1{-}_{ℝ}1\right)=\mathrm{i}\mathrm{i}+1+\left(1{-}_{ℝ}1\right)$$
11		repncan3	$$⊢\left(1\in ℝ\wedge 1\in ℝ\right)\to 1+\left(1{-}_{ℝ}1\right)=1$$
12	2 2 11	mp2an	$$⊢1+\left(1{-}_{ℝ}1\right)=1$$
13	12	oveq2i	$$⊢\mathrm{i}\mathrm{i}+1+\left(1{-}_{ℝ}1\right)=\mathrm{i}\mathrm{i}+1$$
14	10 13	eqtri	$$⊢\mathrm{i}\mathrm{i}+1+\left(1{-}_{ℝ}1\right)=\mathrm{i}\mathrm{i}+1$$
15		ax-i2m1	$$⊢\mathrm{i}\mathrm{i}+1=0$$
16	15	oveq1i	$$⊢\mathrm{i}\mathrm{i}+1+\left(1{-}_{ℝ}1\right)=0+\left(1{-}_{ℝ}1\right)$$
17	14 16 15	3eqtr3i	$$⊢0+\left(1{-}_{ℝ}1\right)=0$$
18	17	a1i	$$⊢\top \to 0+\left(1{-}_{ℝ}1\right)=0$$
19	1 5 18	reladdrsub	$$⊢\top \to 1{-}_{ℝ}1=0{-}_{ℝ}0$$
20	19	mptru	$$⊢1{-}_{ℝ}1=0{-}_{ℝ}0$$