Metamath Proof Explorer

Theorem readdridaddlidd

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 readdridaddlidd.a ⊢φ→A∈ℝ
readdridaddlidd.b ⊢φ→B∈ℝ
readdridaddlidd.1 ⊢φ→B+A=B
Assertion readdridaddlidd ⊢φ∧C∈ℝ→A+C=C

Proof

Step Hyp Ref Expression
1 readdridaddlidd.a ⊢φ→A∈ℝ
2 readdridaddlidd.b ⊢φ→B∈ℝ
3 readdridaddlidd.1 ⊢φ→B+A=B
4 2 adantr ⊢φ∧C∈ℝ→B∈ℝ
5 4 recnd ⊢φ∧C∈ℝ→B∈ℂ
6 1 adantr ⊢φ∧C∈ℝ→A∈ℝ
7 6 recnd ⊢φ∧C∈ℝ→A∈ℂ
8 simpr ⊢φ∧C∈ℝ→C∈ℝ
9 8 recnd ⊢φ∧C∈ℝ→C∈ℂ
10 5 7 9 addassd ⊢φ∧C∈ℝ→B+A+C=B+A+C
11 3 adantr ⊢φ∧C∈ℝ→B+A=B
12 11 oveq1d ⊢φ∧C∈ℝ→B+A+C=B+C
13 10 12 eqtr3d ⊢φ∧C∈ℝ→B+A+C=B+C
14 6 8 readdcld ⊢φ∧C∈ℝ→A+C∈ℝ
15 readdcan ⊢A+C∈ℝ∧C∈ℝ∧B∈ℝ→B+A+C=B+C↔A+C=C
16 14 8 4 15 syl3anc ⊢φ∧C∈ℝ→B+A+C=B+C↔A+C=C
17 13 16 mpbid ⊢φ∧C∈ℝ→A+C=C