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

Proof

Step	Hyp	Ref	Expression
1		readdid1addid2d.a	|- ( ph -> A e. RR )
2		readdid1addid2d.b	|- ( ph -> B e. RR )
3		readdid1addid2d.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 )