Metamath Proof Explorer

Theorem rnglidlmsgrp

Description: The multiplicative group of a (left) ideal of a non-unital ring is a semigroup. (Contributed by AV, 17-Feb-2020) Generalization for non-unital rings. The assumption .0. e. U is required because a left ideal of a non-unital ring does not have to be a subgroup. (Revised by AV, 11-Mar-2025)

Ref Expression
Hypotheses rnglidlabl.l 
|- L = ( LIdeal ` R )
rnglidlabl.i 
|- I = ( R |`s U )
rnglidlabl.z 
|- .0. = ( 0g ` R )
Assertion rnglidlmsgrp 
|- ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> ( mulGrp ` I ) e. Smgrp )

Proof

Step Hyp Ref Expression
1 rnglidlabl.l 
 |-  L = ( LIdeal ` R )
2 rnglidlabl.i 
 |-  I = ( R |`s U )
3 rnglidlabl.z 
 |-  .0. = ( 0g ` R )
4 1 2 3 rnglidlmmgm 
 |-  ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> ( mulGrp ` I ) e. Mgm )
5 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
6 5 rngmgp 
 |-  ( R e. Rng -> ( mulGrp ` R ) e. Smgrp )
7 6 3ad2ant1 
 |-  ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> ( mulGrp ` R ) e. Smgrp )
8 1 2 lidlssbas 
 |-  ( U e. L -> ( Base ` I ) C_ ( Base ` R ) )
9 8 sseld 
 |-  ( U e. L -> ( a e. ( Base ` I ) -> a e. ( Base ` R ) ) )
10 8 sseld 
 |-  ( U e. L -> ( b e. ( Base ` I ) -> b e. ( Base ` R ) ) )
11 8 sseld 
 |-  ( U e. L -> ( c e. ( Base ` I ) -> c e. ( Base ` R ) ) )
12 9 10 11 3anim123d 
 |-  ( U e. L -> ( ( a e. ( Base ` I ) /\ b e. ( Base ` I ) /\ c e. ( Base ` I ) ) -> ( a e. ( Base ` R ) /\ b e. ( Base ` R ) /\ c e. ( Base ` R ) ) ) )
13 12 3ad2ant2 
 |-  ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> ( ( a e. ( Base ` I ) /\ b e. ( Base ` I ) /\ c e. ( Base ` I ) ) -> ( a e. ( Base ` R ) /\ b e. ( Base ` R ) /\ c e. ( Base ` R ) ) ) )
14 13 imp 
 |-  ( ( ( R e. Rng /\ U e. L /\ .0. e. U ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) /\ c e. ( Base ` I ) ) ) -> ( a e. ( Base ` R ) /\ b e. ( Base ` R ) /\ c e. ( Base ` R ) ) )
15 eqid 
 |-  ( Base ` R ) = ( Base ` R )
16 5 15 mgpbas 
 |-  ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
17 eqid 
 |-  ( .r ` R ) = ( .r ` R )
18 5 17 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
19 16 18 sgrpass 
 |-  ( ( ( mulGrp ` R ) e. Smgrp /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) /\ c e. ( Base ` R ) ) ) -> ( ( a ( .r ` R ) b ) ( .r ` R ) c ) = ( a ( .r ` R ) ( b ( .r ` R ) c ) ) )
20 7 14 19 syl2an2r 
 |-  ( ( ( R e. Rng /\ U e. L /\ .0. e. U ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) /\ c e. ( Base ` I ) ) ) -> ( ( a ( .r ` R ) b ) ( .r ` R ) c ) = ( a ( .r ` R ) ( b ( .r ` R ) c ) ) )
21 2 17 ressmulr 
 |-  ( U e. L -> ( .r ` R ) = ( .r ` I ) )
22 21 eqcomd 
 |-  ( U e. L -> ( .r ` I ) = ( .r ` R ) )
23 22 oveqd 
 |-  ( U e. L -> ( a ( .r ` I ) b ) = ( a ( .r ` R ) b ) )
24 eqidd 
 |-  ( U e. L -> c = c )
25 22 23 24 oveq123d 
 |-  ( U e. L -> ( ( a ( .r ` I ) b ) ( .r ` I ) c ) = ( ( a ( .r ` R ) b ) ( .r ` R ) c ) )
26 eqidd 
 |-  ( U e. L -> a = a )
27 22 oveqd 
 |-  ( U e. L -> ( b ( .r ` I ) c ) = ( b ( .r ` R ) c ) )
28 22 26 27 oveq123d 
 |-  ( U e. L -> ( a ( .r ` I ) ( b ( .r ` I ) c ) ) = ( a ( .r ` R ) ( b ( .r ` R ) c ) ) )
29 25 28 eqeq12d 
 |-  ( U e. L -> ( ( ( a ( .r ` I ) b ) ( .r ` I ) c ) = ( a ( .r ` I ) ( b ( .r ` I ) c ) ) <-> ( ( a ( .r ` R ) b ) ( .r ` R ) c ) = ( a ( .r ` R ) ( b ( .r ` R ) c ) ) ) )
30 29 3ad2ant2 
 |-  ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> ( ( ( a ( .r ` I ) b ) ( .r ` I ) c ) = ( a ( .r ` I ) ( b ( .r ` I ) c ) ) <-> ( ( a ( .r ` R ) b ) ( .r ` R ) c ) = ( a ( .r ` R ) ( b ( .r ` R ) c ) ) ) )
31 30 adantr 
 |-  ( ( ( R e. Rng /\ U e. L /\ .0. e. U ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) /\ c e. ( Base ` I ) ) ) -> ( ( ( a ( .r ` I ) b ) ( .r ` I ) c ) = ( a ( .r ` I ) ( b ( .r ` I ) c ) ) <-> ( ( a ( .r ` R ) b ) ( .r ` R ) c ) = ( a ( .r ` R ) ( b ( .r ` R ) c ) ) ) )
32 20 31 mpbird 
 |-  ( ( ( R e. Rng /\ U e. L /\ .0. e. U ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) /\ c e. ( Base ` I ) ) ) -> ( ( a ( .r ` I ) b ) ( .r ` I ) c ) = ( a ( .r ` I ) ( b ( .r ` I ) c ) ) )
33 32 ralrimivvva 
 |-  ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> A. a e. ( Base ` I ) A. b e. ( Base ` I ) A. c e. ( Base ` I ) ( ( a ( .r ` I ) b ) ( .r ` I ) c ) = ( a ( .r ` I ) ( b ( .r ` I ) c ) ) )
34 eqid 
 |-  ( mulGrp ` I ) = ( mulGrp ` I )
35 eqid 
 |-  ( Base ` I ) = ( Base ` I )
36 34 35 mgpbas 
 |-  ( Base ` I ) = ( Base ` ( mulGrp ` I ) )
37 eqid 
 |-  ( .r ` I ) = ( .r ` I )
38 34 37 mgpplusg 
 |-  ( .r ` I ) = ( +g ` ( mulGrp ` I ) )
39 36 38 issgrp 
 |-  ( ( mulGrp ` I ) e. Smgrp <-> ( ( mulGrp ` I ) e. Mgm /\ A. a e. ( Base ` I ) A. b e. ( Base ` I ) A. c e. ( Base ` I ) ( ( a ( .r ` I ) b ) ( .r ` I ) c ) = ( a ( .r ` I ) ( b ( .r ` I ) c ) ) ) )
40 4 33 39 sylanbrc 
 |-  ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> ( mulGrp ` I ) e. Smgrp )