Theorem rngorn1eq

Description: In a unital ring the range of the addition equals the range of the multiplication. (Contributed by FL, 24-Jan-2010) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rnplrnml0.1	|- H = ( 2nd ` R )
	rnplrnml0.2	|- G = ( 1st ` R )
Assertion	rngorn1eq	|- ( R e. RingOps -> ran G = ran H )

Proof

Step	Hyp	Ref	Expression
1		rnplrnml0.1	|- H = ( 2nd ` R )
2		rnplrnml0.2	|- G = ( 1st ` R )
3		eqid	|- ran G = ran G
4	2 1 3	rngosm	|- ( R e. RingOps -> H : ( ran G X. ran G ) --> ran G )
5	2 1 3	rngoi	|- ( R e. RingOps -> ( ( G e. AbelOp /\ H : ( ran G X. ran G ) --> ran G ) /\ ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( ( 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. ran G A. y e. ran G ( ( x H y ) = y /\ ( y H x ) = y ) ) ) )
6	5	simprrd	|- ( R e. RingOps -> E. x e. ran G A. y e. ran G ( ( x H y ) = y /\ ( y H x ) = y ) )
7		rngmgmbs4	|- ( ( H : ( ran G X. ran G ) --> ran G /\ E. x e. ran G A. y e. ran G ( ( x H y ) = y /\ ( y H x ) = y ) ) -> ran H = ran G )
8	4 6 7	syl2anc	|- ( R e. RingOps -> ran H = ran G )
9	8	eqcomd	|- ( R e. RingOps -> ran G = ran H )