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

Metamath Proof Explorer

Theorem rrgsubm

Description: The left regular elements of a ring form a submonoid of the multiplicative group. (Contributed by Thierry Arnoux, 10-May-2025)

Ref Expression
Hypotheses rrgsubm.1 
|- E = ( RLReg ` R )
rrgsubm.2 
|- M = ( mulGrp ` R )
rrgsubm.3 
|- ( ph -> R e. Ring )
Assertion rrgsubm 
|- ( ph -> E e. ( SubMnd ` M ) )

Proof

Step Hyp Ref Expression
1 rrgsubm.1 
 |-  E = ( RLReg ` R )
2 rrgsubm.2 
 |-  M = ( mulGrp ` R )
3 rrgsubm.3 
 |-  ( ph -> R e. Ring )
4 2 ringmgp 
 |-  ( R e. Ring -> M e. Mnd )
5 3 4 syl 
 |-  ( ph -> M e. Mnd )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 1 6 rrgss 
 |-  E C_ ( Base ` R )
8 7 a1i 
 |-  ( ph -> E C_ ( Base ` R ) )
9 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
10 9 1 3 1rrg 
 |-  ( ph -> ( 1r ` R ) e. E )
11 eqid 
 |-  ( .r ` R ) = ( .r ` R )
12 3 ad2antrr 
 |-  ( ( ( ph /\ x e. E ) /\ y e. E ) -> R e. Ring )
13 simplr 
 |-  ( ( ( ph /\ x e. E ) /\ y e. E ) -> x e. E )
14 7 13 sselid 
 |-  ( ( ( ph /\ x e. E ) /\ y e. E ) -> x e. ( Base ` R ) )
15 simpr 
 |-  ( ( ( ph /\ x e. E ) /\ y e. E ) -> y e. E )
16 7 15 sselid 
 |-  ( ( ( ph /\ x e. E ) /\ y e. E ) -> y e. ( Base ` R ) )
17 6 11 12 14 16 ringcld 
 |-  ( ( ( ph /\ x e. E ) /\ y e. E ) -> ( x ( .r ` R ) y ) e. ( Base ` R ) )
18 15 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. E ) /\ y e. E ) /\ z e. ( Base ` R ) ) /\ ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( 0g ` R ) ) -> y e. E )
19 simplr 
 |-  ( ( ( ( ( ph /\ x e. E ) /\ y e. E ) /\ z e. ( Base ` R ) ) /\ ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( 0g ` R ) ) -> z e. ( Base ` R ) )
20 13 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. E ) /\ y e. E ) /\ z e. ( Base ` R ) ) /\ ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( 0g ` R ) ) -> x e. E )
21 12 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. E ) /\ y e. E ) /\ z e. ( Base ` R ) ) /\ ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( 0g ` R ) ) -> R e. Ring )
22 16 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. E ) /\ y e. E ) /\ z e. ( Base ` R ) ) /\ ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( 0g ` R ) ) -> y e. ( Base ` R ) )
23 6 11 21 22 19 ringcld 
 |-  ( ( ( ( ( ph /\ x e. E ) /\ y e. E ) /\ z e. ( Base ` R ) ) /\ ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( 0g ` R ) ) -> ( y ( .r ` R ) z ) e. ( Base ` R ) )
24 14 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. E ) /\ y e. E ) /\ z e. ( Base ` R ) ) /\ ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( 0g ` R ) ) -> x e. ( Base ` R ) )
25 6 11 21 24 22 19 ringassd 
 |-  ( ( ( ( ( ph /\ x e. E ) /\ y e. E ) /\ z e. ( Base ` R ) ) /\ ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( 0g ` R ) ) -> ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( x ( .r ` R ) ( y ( .r ` R ) z ) ) )
26 simpr 
 |-  ( ( ( ( ( ph /\ x e. E ) /\ y e. E ) /\ z e. ( Base ` R ) ) /\ ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( 0g ` R ) ) -> ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( 0g ` R ) )
27 25 26 eqtr3d 
 |-  ( ( ( ( ( ph /\ x e. E ) /\ y e. E ) /\ z e. ( Base ` R ) ) /\ ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( 0g ` R ) ) -> ( x ( .r ` R ) ( y ( .r ` R ) z ) ) = ( 0g ` R ) )
28 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
29 1 6 11 28 rrgeq0i 
 |-  ( ( x e. E /\ ( y ( .r ` R ) z ) e. ( Base ` R ) ) -> ( ( x ( .r ` R ) ( y ( .r ` R ) z ) ) = ( 0g ` R ) -> ( y ( .r ` R ) z ) = ( 0g ` R ) ) )
30 29 imp 
 |-  ( ( ( x e. E /\ ( y ( .r ` R ) z ) e. ( Base ` R ) ) /\ ( x ( .r ` R ) ( y ( .r ` R ) z ) ) = ( 0g ` R ) ) -> ( y ( .r ` R ) z ) = ( 0g ` R ) )
31 20 23 27 30 syl21anc 
 |-  ( ( ( ( ( ph /\ x e. E ) /\ y e. E ) /\ z e. ( Base ` R ) ) /\ ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( 0g ` R ) ) -> ( y ( .r ` R ) z ) = ( 0g ` R ) )
32 1 6 11 28 rrgeq0i 
 |-  ( ( y e. E /\ z e. ( Base ` R ) ) -> ( ( y ( .r ` R ) z ) = ( 0g ` R ) -> z = ( 0g ` R ) ) )
33 32 imp 
 |-  ( ( ( y e. E /\ z e. ( Base ` R ) ) /\ ( y ( .r ` R ) z ) = ( 0g ` R ) ) -> z = ( 0g ` R ) )
34 18 19 31 33 syl21anc 
 |-  ( ( ( ( ( ph /\ x e. E ) /\ y e. E ) /\ z e. ( Base ` R ) ) /\ ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( 0g ` R ) ) -> z = ( 0g ` R ) )
35 34 ex 
 |-  ( ( ( ( ph /\ x e. E ) /\ y e. E ) /\ z e. ( Base ` R ) ) -> ( ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( 0g ` R ) -> z = ( 0g ` R ) ) )
36 35 ralrimiva 
 |-  ( ( ( ph /\ x e. E ) /\ y e. E ) -> A. z e. ( Base ` R ) ( ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( 0g ` R ) -> z = ( 0g ` R ) ) )
37 1 6 11 28 isrrg 
 |-  ( ( x ( .r ` R ) y ) e. E <-> ( ( x ( .r ` R ) y ) e. ( Base ` R ) /\ A. z e. ( Base ` R ) ( ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( 0g ` R ) -> z = ( 0g ` R ) ) ) )
38 17 36 37 sylanbrc 
 |-  ( ( ( ph /\ x e. E ) /\ y e. E ) -> ( x ( .r ` R ) y ) e. E )
39 38 anasss 
 |-  ( ( ph /\ ( x e. E /\ y e. E ) ) -> ( x ( .r ` R ) y ) e. E )
40 39 ralrimivva 
 |-  ( ph -> A. x e. E A. y e. E ( x ( .r ` R ) y ) e. E )
41 2 6 mgpbas 
 |-  ( Base ` R ) = ( Base ` M )
42 2 9 ringidval 
 |-  ( 1r ` R ) = ( 0g ` M )
43 2 11 mgpplusg 
 |-  ( .r ` R ) = ( +g ` M )
44 41 42 43 issubm 
 |-  ( M e. Mnd -> ( E e. ( SubMnd ` M ) <-> ( E C_ ( Base ` R ) /\ ( 1r ` R ) e. E /\ A. x e. E A. y e. E ( x ( .r ` R ) y ) e. E ) ) )
45 44 biimpar 
 |-  ( ( M e. Mnd /\ ( E C_ ( Base ` R ) /\ ( 1r ` R ) e. E /\ A. x e. E A. y e. E ( x ( .r ` R ) y ) e. E ) ) -> E e. ( SubMnd ` M ) )
46 5 8 10 40 45 syl13anc 
 |-  ( ph -> E e. ( SubMnd ` M ) )