Theorem readdid1addid2d

Description: Given some real number B where A acts like a right additive identity, derive that A is a left additive identity. Note that the hypothesis is weaker than proving that A is a right additive identity (for all numbers). Although, if there is a right additive identity, then by readdcan , A is the right additive identity. (Contributed by Steven Nguyen, 14-Jan-2023)

	Ref	Expression
Hypotheses	readdid1addid2d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	readdid1addid2d.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	readdid1addid2d.1	⊢ ( 𝜑 → ( 𝐵 + 𝐴 ) = 𝐵 )
Assertion	readdid1addid2d	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + 𝐶 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		readdid1addid2d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		readdid1addid2d.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		readdid1addid2d.1	⊢ ( 𝜑 → ( 𝐵 + 𝐴 ) = 𝐵 )
4	2	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
5	4	recnd	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
6	1	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
7	6	recnd	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℂ )
8		simpr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
9	8	recnd	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℂ )
10	5 7 9	addassd	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℝ ) → ( ( 𝐵 + 𝐴 ) + 𝐶 ) = ( 𝐵 + ( 𝐴 + 𝐶 ) ) )
11	3	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℝ ) → ( 𝐵 + 𝐴 ) = 𝐵 )
12	11	oveq1d	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℝ ) → ( ( 𝐵 + 𝐴 ) + 𝐶 ) = ( 𝐵 + 𝐶 ) )
13	10 12	eqtr3d	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℝ ) → ( 𝐵 + ( 𝐴 + 𝐶 ) ) = ( 𝐵 + 𝐶 ) )
14	6 8	readdcld	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + 𝐶 ) ∈ ℝ )
15		readdcan	⊢ ( ( ( 𝐴 + 𝐶 ) ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐵 + ( 𝐴 + 𝐶 ) ) = ( 𝐵 + 𝐶 ) ↔ ( 𝐴 + 𝐶 ) = 𝐶 ) )
16	14 8 4 15	syl3anc	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℝ ) → ( ( 𝐵 + ( 𝐴 + 𝐶 ) ) = ( 𝐵 + 𝐶 ) ↔ ( 𝐴 + 𝐶 ) = 𝐶 ) )
17	13 16	mpbid	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + 𝐶 ) = 𝐶 )