This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )