Metamath Proof Explorer

Theorem rngomndo

Description: In a unital ring the multiplication is a monoid. (Contributed by FL, 24-Jan-2010) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis unmnd.1 
|- H = ( 2nd ` R )
Assertion rngomndo 
|- ( R e. RingOps -> H e. MndOp )

Proof

Step Hyp Ref Expression
1 unmnd.1 
 |-  H = ( 2nd ` R )
2 eqid 
 |-  ( 1st ` R ) = ( 1st ` R )
3 eqid 
 |-  ran ( 1st ` R ) = ran ( 1st ` R )
4 2 1 3 rngosm 
 |-  ( R e. RingOps -> H : ( ran ( 1st ` R ) X. ran ( 1st ` R ) ) --> ran ( 1st ` R ) )
5 2 1 3 rngoass 
 |-  ( ( R e. RingOps /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) /\ z e. ran ( 1st ` R ) ) ) -> ( ( x H y ) H z ) = ( x H ( y H z ) ) )
6 5 ralrimivvva 
 |-  ( R e. RingOps -> A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) A. z e. ran ( 1st ` R ) ( ( x H y ) H z ) = ( x H ( y H z ) ) )
7 2 1 3 rngoi 
 |-  ( R e. RingOps -> ( ( ( 1st ` R ) e. AbelOp /\ H : ( ran ( 1st ` R ) X. ran ( 1st ` R ) ) --> ran ( 1st ` R ) ) /\ ( A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) A. z e. ran ( 1st ` R ) ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y ( 1st ` R ) z ) ) = ( ( x H y ) ( 1st ` R ) ( x H z ) ) /\ ( ( x ( 1st ` R ) y ) H z ) = ( ( x H z ) ( 1st ` R ) ( y H z ) ) ) /\ E. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( x H y ) = y /\ ( y H x ) = y ) ) ) )
8 7 simprrd 
 |-  ( R e. RingOps -> E. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( x H y ) = y /\ ( y H x ) = y ) )
9 1 2 rngorn1 
 |-  ( R e. RingOps -> ran ( 1st ` R ) = dom dom H )
10 xpid11 
 |-  ( ( dom dom H X. dom dom H ) = ( ran ( 1st ` R ) X. ran ( 1st ` R ) ) <-> dom dom H = ran ( 1st ` R ) )
11 10 biimpri 
 |-  ( dom dom H = ran ( 1st ` R ) -> ( dom dom H X. dom dom H ) = ( ran ( 1st ` R ) X. ran ( 1st ` R ) ) )
12 feq23 
 |-  ( ( ( dom dom H X. dom dom H ) = ( ran ( 1st ` R ) X. ran ( 1st ` R ) ) /\ dom dom H = ran ( 1st ` R ) ) -> ( H : ( dom dom H X. dom dom H ) --> dom dom H <-> H : ( ran ( 1st ` R ) X. ran ( 1st ` R ) ) --> ran ( 1st ` R ) ) )
13 11 12 mpancom 
 |-  ( dom dom H = ran ( 1st ` R ) -> ( H : ( dom dom H X. dom dom H ) --> dom dom H <-> H : ( ran ( 1st ` R ) X. ran ( 1st ` R ) ) --> ran ( 1st ` R ) ) )
14 raleq 
 |-  ( dom dom H = ran ( 1st ` R ) -> ( A. z e. dom dom H ( ( x H y ) H z ) = ( x H ( y H z ) ) <-> A. z e. ran ( 1st ` R ) ( ( x H y ) H z ) = ( x H ( y H z ) ) ) )
15 14 raleqbi1dv 
 |-  ( dom dom H = ran ( 1st ` R ) -> ( A. y e. dom dom H A. z e. dom dom H ( ( x H y ) H z ) = ( x H ( y H z ) ) <-> A. y e. ran ( 1st ` R ) A. z e. ran ( 1st ` R ) ( ( x H y ) H z ) = ( x H ( y H z ) ) ) )
16 15 raleqbi1dv 
 |-  ( dom dom H = ran ( 1st ` R ) -> ( A. x e. dom dom H A. y e. dom dom H A. z e. dom dom H ( ( x H y ) H z ) = ( x H ( y H z ) ) <-> A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) A. z e. ran ( 1st ` R ) ( ( x H y ) H z ) = ( x H ( y H z ) ) ) )
17 raleq 
 |-  ( dom dom H = ran ( 1st ` R ) -> ( A. y e. dom dom H ( ( x H y ) = y /\ ( y H x ) = y ) <-> A. y e. ran ( 1st ` R ) ( ( x H y ) = y /\ ( y H x ) = y ) ) )
18 17 rexeqbi1dv 
 |-  ( dom dom H = ran ( 1st ` R ) -> ( E. x e. dom dom H A. y e. dom dom H ( ( x H y ) = y /\ ( y H x ) = y ) <-> E. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( x H y ) = y /\ ( y H x ) = y ) ) )
19 13 16 18 3anbi123d 
 |-  ( dom dom H = ran ( 1st ` R ) -> ( ( H : ( dom dom H X. dom dom H ) --> dom dom H /\ A. x e. dom dom H A. y e. dom dom H A. z e. dom dom H ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ E. x e. dom dom H A. y e. dom dom H ( ( x H y ) = y /\ ( y H x ) = y ) ) <-> ( H : ( ran ( 1st ` R ) X. ran ( 1st ` R ) ) --> ran ( 1st ` R ) /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) A. z e. ran ( 1st ` R ) ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ E. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( x H y ) = y /\ ( y H x ) = y ) ) ) )
20 19 eqcoms 
 |-  ( ran ( 1st ` R ) = dom dom H -> ( ( H : ( dom dom H X. dom dom H ) --> dom dom H /\ A. x e. dom dom H A. y e. dom dom H A. z e. dom dom H ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ E. x e. dom dom H A. y e. dom dom H ( ( x H y ) = y /\ ( y H x ) = y ) ) <-> ( H : ( ran ( 1st ` R ) X. ran ( 1st ` R ) ) --> ran ( 1st ` R ) /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) A. z e. ran ( 1st ` R ) ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ E. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( x H y ) = y /\ ( y H x ) = y ) ) ) )
21 9 20 syl 
 |-  ( R e. RingOps -> ( ( H : ( dom dom H X. dom dom H ) --> dom dom H /\ A. x e. dom dom H A. y e. dom dom H A. z e. dom dom H ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ E. x e. dom dom H A. y e. dom dom H ( ( x H y ) = y /\ ( y H x ) = y ) ) <-> ( H : ( ran ( 1st ` R ) X. ran ( 1st ` R ) ) --> ran ( 1st ` R ) /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) A. z e. ran ( 1st ` R ) ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ E. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( x H y ) = y /\ ( y H x ) = y ) ) ) )
22 4 6 8 21 mpbir3and 
 |-  ( R e. RingOps -> ( H : ( dom dom H X. dom dom H ) --> dom dom H /\ A. x e. dom dom H A. y e. dom dom H A. z e. dom dom H ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ E. x e. dom dom H A. y e. dom dom H ( ( x H y ) = y /\ ( y H x ) = y ) ) )
23 fvex 
 |-  ( 2nd ` R ) e. _V
24 eleq1 
 |-  ( H = ( 2nd ` R ) -> ( H e. _V <-> ( 2nd ` R ) e. _V ) )
25 23 24 mpbiri 
 |-  ( H = ( 2nd ` R ) -> H e. _V )
26 eqid 
 |-  dom dom H = dom dom H
27 26 ismndo1 
 |-  ( H e. _V -> ( H e. MndOp <-> ( H : ( dom dom H X. dom dom H ) --> dom dom H /\ A. x e. dom dom H A. y e. dom dom H A. z e. dom dom H ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ E. x e. dom dom H A. y e. dom dom H ( ( x H y ) = y /\ ( y H x ) = y ) ) ) )
28 1 25 27 mp2b 
 |-  ( H e. MndOp <-> ( H : ( dom dom H X. dom dom H ) --> dom dom H /\ A. x e. dom dom H A. y e. dom dom H A. z e. dom dom H ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ E. x e. dom dom H A. y e. dom dom H ( ( x H y ) = y /\ ( y H x ) = y ) ) )
29 22 28 sylibr 
 |-  ( R e. RingOps -> H e. MndOp )