Metamath Proof Explorer

Theorem rngodm1dm2

Description: In a unital ring the domain of the first variable of the addition equals the domain of the first variable 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 rngodm1dm2 
|- ( R e. RingOps -> dom dom G = dom dom H )

Proof

Step Hyp Ref Expression
1 rnplrnml0.1 
 |-  H = ( 2nd ` R )
2 rnplrnml0.2 
 |-  G = ( 1st ` R )
3 2 rngogrpo 
 |-  ( R e. RingOps -> G e. GrpOp )
4 eqid 
 |-  ran G = ran G
5 4 grpofo 
 |-  ( G e. GrpOp -> G : ( ran G X. ran G ) -onto-> ran G )
6 3 5 syl 
 |-  ( R e. RingOps -> G : ( ran G X. ran G ) -onto-> ran G )
7 2 1 4 rngosm 
 |-  ( R e. RingOps -> H : ( ran G X. ran G ) --> ran G )
8 fof 
 |-  ( G : ( ran G X. ran G ) -onto-> ran G -> G : ( ran G X. ran G ) --> ran G )
9 8 fdmd 
 |-  ( G : ( ran G X. ran G ) -onto-> ran G -> dom G = ( ran G X. ran G ) )
10 fdm 
 |-  ( H : ( ran G X. ran G ) --> ran G -> dom H = ( ran G X. ran G ) )
11 eqtr 
 |-  ( ( dom G = ( ran G X. ran G ) /\ ( ran G X. ran G ) = dom H ) -> dom G = dom H )
12 11 dmeqd 
 |-  ( ( dom G = ( ran G X. ran G ) /\ ( ran G X. ran G ) = dom H ) -> dom dom G = dom dom H )
13 12 expcom 
 |-  ( ( ran G X. ran G ) = dom H -> ( dom G = ( ran G X. ran G ) -> dom dom G = dom dom H ) )
14 13 eqcoms 
 |-  ( dom H = ( ran G X. ran G ) -> ( dom G = ( ran G X. ran G ) -> dom dom G = dom dom H ) )
15 10 14 syl 
 |-  ( H : ( ran G X. ran G ) --> ran G -> ( dom G = ( ran G X. ran G ) -> dom dom G = dom dom H ) )
16 9 15 syl5com 
 |-  ( G : ( ran G X. ran G ) -onto-> ran G -> ( H : ( ran G X. ran G ) --> ran G -> dom dom G = dom dom H ) )
17 6 7 16 sylc 
 |-  ( R e. RingOps -> dom dom G = dom dom H )