Theorem re1m1e0m0

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

	Ref	Expression
Assertion	re1m1e0m0	⊢ ( 1 −ℝ 1 ) = ( 0 −ℝ 0 )

Proof

Step	Hyp	Ref	Expression
1		0red	⊢ ( ⊤ → 0 ∈ ℝ )
2		1re	⊢ 1 ∈ ℝ
3		rersubcl	⊢ ( ( 1 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 1 −ℝ 1 ) ∈ ℝ )
4	2 2 3	mp2an	⊢ ( 1 −ℝ 1 ) ∈ ℝ
5	4	a1i	⊢ ( ⊤ → ( 1 −ℝ 1 ) ∈ ℝ )
6		ax-icn	⊢ i ∈ ℂ
7	6 6	mulcli	⊢ ( i · i ) ∈ ℂ
8		ax-1cn	⊢ 1 ∈ ℂ
9	4	recni	⊢ ( 1 −ℝ 1 ) ∈ ℂ
10	7 8 9	addassi	⊢ ( ( ( i · i ) + 1 ) + ( 1 −ℝ 1 ) ) = ( ( i · i ) + ( 1 + ( 1 −ℝ 1 ) ) )
11		repncan3	⊢ ( ( 1 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 1 + ( 1 −ℝ 1 ) ) = 1 )
12	2 2 11	mp2an	⊢ ( 1 + ( 1 −ℝ 1 ) ) = 1
13	12	oveq2i	⊢ ( ( i · i ) + ( 1 + ( 1 −ℝ 1 ) ) ) = ( ( i · i ) + 1 )
14	10 13	eqtri	⊢ ( ( ( i · i ) + 1 ) + ( 1 −ℝ 1 ) ) = ( ( i · i ) + 1 )
15		ax-i2m1	⊢ ( ( i · i ) + 1 ) = 0
16	15	oveq1i	⊢ ( ( ( i · i ) + 1 ) + ( 1 −ℝ 1 ) ) = ( 0 + ( 1 −ℝ 1 ) )
17	14 16 15	3eqtr3i	⊢ ( 0 + ( 1 −ℝ 1 ) ) = 0
18	17	a1i	⊢ ( ⊤ → ( 0 + ( 1 −ℝ 1 ) ) = 0 )
19	1 5 18	reladdrsub	⊢ ( ⊤ → ( 1 −ℝ 1 ) = ( 0 −ℝ 0 ) )
20	19	mptru	⊢ ( 1 −ℝ 1 ) = ( 0 −ℝ 0 )