Theorem ringadd2

Description: A ring element plus itself is two times the element. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Mario Carneiro, 22-Dec-2013) (Revised by AV, 24-Aug-2021) (Proof shortened by AV, 1-Feb-2025)

	Ref	Expression
Hypotheses	ringadd2.b	|- B = ( Base ` R )
	ringadd2.p	|- .+ = ( +g ` R )
	ringadd2.t	|- .x. = ( .r ` R )
Assertion	ringadd2	|- ( ( R e. Ring /\ X e. B ) -> E. x e. B ( X .+ X ) = ( ( x .+ x ) .x. X ) )

Proof

Step	Hyp	Ref	Expression
1		ringadd2.b	|- B = ( Base ` R )
2		ringadd2.p	|- .+ = ( +g ` R )
3		ringadd2.t	|- .x. = ( .r ` R )
4		eqid	|- ( 1r ` R ) = ( 1r ` R )
5	1 4	ringidcl	|- ( R e. Ring -> ( 1r ` R ) e. B )
6	5	adantr	|- ( ( R e. Ring /\ X e. B ) -> ( 1r ` R ) e. B )
7		simpr	|- ( ( ( R e. Ring /\ X e. B ) /\ x = ( 1r ` R ) ) -> x = ( 1r ` R ) )
8	7 7	oveq12d	|- ( ( ( R e. Ring /\ X e. B ) /\ x = ( 1r ` R ) ) -> ( x .+ x ) = ( ( 1r ` R ) .+ ( 1r ` R ) ) )
9	8	oveq1d	|- ( ( ( R e. Ring /\ X e. B ) /\ x = ( 1r ` R ) ) -> ( ( x .+ x ) .x. X ) = ( ( ( 1r ` R ) .+ ( 1r ` R ) ) .x. X ) )
10	9	eqeq2d	|- ( ( ( R e. Ring /\ X e. B ) /\ x = ( 1r ` R ) ) -> ( ( X .+ X ) = ( ( x .+ x ) .x. X ) <-> ( X .+ X ) = ( ( ( 1r ` R ) .+ ( 1r ` R ) ) .x. X ) ) )
11	1 2 3 4	ringo2times	|- ( ( R e. Ring /\ X e. B ) -> ( X .+ X ) = ( ( ( 1r ` R ) .+ ( 1r ` R ) ) .x. X ) )
12	6 10 11	rspcedvd	|- ( ( R e. Ring /\ X e. B ) -> E. x e. B ( X .+ X ) = ( ( x .+ x ) .x. X ) )