Theorem rngo2

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) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ringi.1	|- G = ( 1st ` R )
	ringi.2	|- H = ( 2nd ` R )
	ringi.3	|- X = ran G
Assertion	rngo2	|- ( ( R e. RingOps /\ A e. X ) -> E. x e. X ( A G A ) = ( ( x G x ) H A ) )

Proof

Step	Hyp	Ref	Expression
1		ringi.1	|- G = ( 1st ` R )
2		ringi.2	|- H = ( 2nd ` R )
3		ringi.3	|- X = ran G
4	1 2 3	rngoid	|- ( ( R e. RingOps /\ A e. X ) -> E. x e. X ( ( x H A ) = A /\ ( A H x ) = A ) )
5		oveq12	|- ( ( ( x H A ) = A /\ ( x H A ) = A ) -> ( ( x H A ) G ( x H A ) ) = ( A G A ) )
6	5	anidms	|- ( ( x H A ) = A -> ( ( x H A ) G ( x H A ) ) = ( A G A ) )
7	6	eqcomd	|- ( ( x H A ) = A -> ( A G A ) = ( ( x H A ) G ( x H A ) ) )
8		simpll	|- ( ( ( R e. RingOps /\ A e. X ) /\ x e. X ) -> R e. RingOps )
9		simpr	|- ( ( ( R e. RingOps /\ A e. X ) /\ x e. X ) -> x e. X )
10		simplr	|- ( ( ( R e. RingOps /\ A e. X ) /\ x e. X ) -> A e. X )
11	1 2 3	rngodir	|- ( ( R e. RingOps /\ ( x e. X /\ x e. X /\ A e. X ) ) -> ( ( x G x ) H A ) = ( ( x H A ) G ( x H A ) ) )
12	8 9 9 10 11	syl13anc	|- ( ( ( R e. RingOps /\ A e. X ) /\ x e. X ) -> ( ( x G x ) H A ) = ( ( x H A ) G ( x H A ) ) )
13	12	eqeq2d	|- ( ( ( R e. RingOps /\ A e. X ) /\ x e. X ) -> ( ( A G A ) = ( ( x G x ) H A ) <-> ( A G A ) = ( ( x H A ) G ( x H A ) ) ) )
14	7 13	imbitrrid	|- ( ( ( R e. RingOps /\ A e. X ) /\ x e. X ) -> ( ( x H A ) = A -> ( A G A ) = ( ( x G x ) H A ) ) )
15	14	adantrd	|- ( ( ( R e. RingOps /\ A e. X ) /\ x e. X ) -> ( ( ( x H A ) = A /\ ( A H x ) = A ) -> ( A G A ) = ( ( x G x ) H A ) ) )
16	15	reximdva	|- ( ( R e. RingOps /\ A e. X ) -> ( E. x e. X ( ( x H A ) = A /\ ( A H x ) = A ) -> E. x e. X ( A G A ) = ( ( x G x ) H A ) ) )
17	4 16	mpd	|- ( ( R e. RingOps /\ A e. X ) -> E. x e. X ( A G A ) = ( ( x G x ) H A ) )