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

rngoi 
 ( R e. RingOps > ( ( G e. AbelOp /\ H : ( X X. X ) > X ) /\ ( A. u e. X A. x e. X A. y e. X ( ( ( u H x ) H y ) = ( u H ( x H y ) ) /\ ( u H ( x G y ) ) = ( ( u H x ) G ( u H y ) ) /\ ( ( u G x ) H y ) = ( ( u H y ) G ( x H y ) ) ) /\ E. u e. X A. x e. X ( ( u H x ) = x /\ ( x H u ) = x ) ) ) ) 
5 
4

simprrd 
 ( R e. RingOps > E. u e. X A. x e. X ( ( u H x ) = x /\ ( x H u ) = x ) ) 
6 

r19.12 
 ( E. u e. X A. x e. X ( ( u H x ) = x /\ ( x H u ) = x ) > A. x e. X E. u e. X ( ( u H x ) = x /\ ( x H u ) = x ) ) 
7 
5 6

syl 
 ( R e. RingOps > A. x e. X E. u e. X ( ( u H x ) = x /\ ( x H u ) = x ) ) 
8 

oveq2 
 ( x = A > ( u H x ) = ( u H A ) ) 
9 

id 
 ( x = A > x = A ) 
10 
8 9

eqeq12d 
 ( x = A > ( ( u H x ) = x <> ( u H A ) = A ) ) 
11 

oveq1 
 ( x = A > ( x H u ) = ( A H u ) ) 
12 
11 9

eqeq12d 
 ( x = A > ( ( x H u ) = x <> ( A H u ) = A ) ) 
13 
10 12

anbi12d 
 ( x = A > ( ( ( u H x ) = x /\ ( x H u ) = x ) <> ( ( u H A ) = A /\ ( A H u ) = A ) ) ) 
14 
13

rexbidv 
 ( x = A > ( E. u e. X ( ( u H x ) = x /\ ( x H u ) = x ) <> E. u e. X ( ( u H A ) = A /\ ( A H u ) = A ) ) ) 
15 
14

rspccva 
 ( ( A. x e. X E. u e. X ( ( u H x ) = x /\ ( x H u ) = x ) /\ A e. X ) > E. u e. X ( ( u H A ) = A /\ ( A H u ) = A ) ) 
16 
7 15

sylan 
 ( ( R e. RingOps /\ A e. X ) > E. u e. X ( ( u H A ) = A /\ ( A H u ) = A ) ) 