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 )