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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
readdridaddlidd.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
readdridaddlidd.1 ⊢ ( 𝜑 → ( 𝐵 + 𝐴 ) = 𝐵 )
Assertion readdridaddlidd ( ( 𝜑 ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + 𝐶 ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 readdridaddlidd.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 readdridaddlidd.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 readdridaddlidd.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 ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + 𝐶 ) = 𝐶 )