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 
|- ( ph -> A e. RR )
readdridaddlidd.b 
|- ( ph -> B e. RR )
readdridaddlidd.1 
|- ( ph -> ( B + A ) = B )
Assertion readdridaddlidd 
|- ( ( ph /\ C e. RR ) -> ( A + C ) = C )

Proof

Step Hyp Ref Expression
1 readdridaddlidd.a 
 |-  ( ph -> A e. RR )
2 readdridaddlidd.b 
 |-  ( ph -> B e. RR )
3 readdridaddlidd.1 
 |-  ( ph -> ( B + A ) = B )
4 2 adantr 
 |-  ( ( ph /\ C e. RR ) -> B e. RR )
5 4 recnd 
 |-  ( ( ph /\ C e. RR ) -> B e. CC )
6 1 adantr 
 |-  ( ( ph /\ C e. RR ) -> A e. RR )
7 6 recnd 
 |-  ( ( ph /\ C e. RR ) -> A e. CC )
8 simpr 
 |-  ( ( ph /\ C e. RR ) -> C e. RR )
9 8 recnd 
 |-  ( ( ph /\ C e. RR ) -> C e. CC )
10 5 7 9 addassd 
 |-  ( ( ph /\ C e. RR ) -> ( ( B + A ) + C ) = ( B + ( A + C ) ) )
11 3 adantr 
 |-  ( ( ph /\ C e. RR ) -> ( B + A ) = B )
12 11 oveq1d 
 |-  ( ( ph /\ C e. RR ) -> ( ( B + A ) + C ) = ( B + C ) )
13 10 12 eqtr3d 
 |-  ( ( ph /\ C e. RR ) -> ( B + ( A + C ) ) = ( B + C ) )
14 6 8 readdcld 
 |-  ( ( ph /\ C e. RR ) -> ( A + C ) e. RR )
15 readdcan 
 |-  ( ( ( A + C ) e. RR /\ C e. RR /\ B e. RR ) -> ( ( B + ( A + C ) ) = ( B + C ) <-> ( A + C ) = C ) )
16 14 8 4 15 syl3anc 
 |-  ( ( ph /\ C e. RR ) -> ( ( B + ( A + C ) ) = ( B + C ) <-> ( A + C ) = C ) )
17 13 16 mpbid 
 |-  ( ( ph /\ C e. RR ) -> ( A + C ) = C )