Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 readdid1addid2d.a ⊢ φ → A ∈ ℝ
2 readdid1addid2d.b ⊢ φ → B ∈ ℝ
3 readdid1addid2d.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