Metamath Proof Explorer


Theorem rngosm

Description: Functionality of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Mario Carneiro, 21-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 rngosm
|- ( R e. RingOps -> H : ( X X. X ) --> X )

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