Description: Functionality of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9Sep2007) (Revised by Mario Carneiro, 21Dec2013) (New usage is discouraged.)
Ref  Expression  

Hypotheses  ringi.1   G = ( 1st ` R ) 

ringi.2   H = ( 2nd ` R ) 

ringi.3   X = ran G 

Assertion  rngosm   ( R e. RingOps > H : ( X X. X ) > X ) 
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. x e. X A. y e. X A. z e. X ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) /\ E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) ) ) 
5  4  simpld   ( R e. RingOps > ( G e. AbelOp /\ H : ( X X. X ) > X ) ) 
6  5  simprd   ( R e. RingOps > H : ( X X. X ) > X ) 