This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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