This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )