Metamath Proof Explorer

Theorem lidlmsgrp

Description: The multiplicative group of a (left) ideal of a ring is a semigroup. (Contributed by AV, 17-Feb-2020)

Ref Expression
Hypotheses lidlabl.l 
|- L = ( LIdeal ` R )
lidlabl.i 
|- I = ( R |`s U )
Assertion lidlmsgrp 
|- ( ( R e. Ring /\ U e. L ) -> ( mulGrp ` I ) e. Smgrp )

Proof

Step Hyp Ref Expression
1 lidlabl.l 
 |-  L = ( LIdeal ` R )
2 lidlabl.i 
 |-  I = ( R |`s U )
3 1 2 lidlmmgm 
 |-  ( ( R e. Ring /\ U e. L ) -> ( mulGrp ` I ) e. Mgm )
4 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
5 4 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
6 5 ad2antrr 
 |-  ( ( ( R e. Ring /\ U e. L ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) /\ c e. ( Base ` I ) ) ) -> ( mulGrp ` R ) e. Mnd )
7 1 2 lidlssbas 
 |-  ( U e. L -> ( Base ` I ) C_ ( Base ` R ) )
8 7 sseld 
 |-  ( U e. L -> ( a e. ( Base ` I ) -> a e. ( Base ` R ) ) )
9 7 sseld 
 |-  ( U e. L -> ( b e. ( Base ` I ) -> b e. ( Base ` R ) ) )
10 7 sseld 
 |-  ( U e. L -> ( c e. ( Base ` I ) -> c e. ( Base ` R ) ) )
11 8 9 10 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 ) ) ) )
12 11 adantl 
 |-  ( ( R e. Ring /\ 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 imp 
 |-  ( ( ( R e. Ring /\ 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 ) ) )
14 eqid 
 |-  ( Base ` R ) = ( Base ` R )
15 4 14 mgpbas 
 |-  ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
16 eqid 
 |-  ( .r ` R ) = ( .r ` R )
17 4 16 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
18 15 17 mndass 
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ ( 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 ) ) )
19 6 13 18 syl2anc 
 |-  ( ( ( R e. Ring /\ U e. L ) /\ ( 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 ) ) )
20 19 ralrimivvva 
 |-  ( ( R e. Ring /\ U e. L ) -> A. a e. ( Base ` I ) A. b e. ( Base ` I ) A. c e. ( Base ` I ) ( ( a ( .r ` R ) b ) ( .r ` R ) c ) = ( a ( .r ` R ) ( b ( .r ` R ) c ) ) )
21 2 16 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 adantl 
 |-  ( ( R e. Ring /\ 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 ) ) ) )
31 30 ralbidv 
 |-  ( ( R e. Ring /\ U e. L ) -> ( A. c e. ( Base ` I ) ( ( a ( .r ` I ) b ) ( .r ` I ) c ) = ( a ( .r ` I ) ( b ( .r ` I ) c ) ) <-> A. c e. ( Base ` I ) ( ( a ( .r ` R ) b ) ( .r ` R ) c ) = ( a ( .r ` R ) ( b ( .r ` R ) c ) ) ) )
32 31 2ralbidv 
 |-  ( ( R e. Ring /\ U e. L ) -> ( 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 ) ) <-> A. a e. ( Base ` I ) A. b e. ( Base ` I ) A. c e. ( Base ` I ) ( ( a ( .r ` R ) b ) ( .r ` R ) c ) = ( a ( .r ` R ) ( b ( .r ` R ) c ) ) ) )
33 20 32 mpbird 
 |-  ( ( R e. Ring /\ U e. L ) -> 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 3 33 39 sylanbrc 
 |-  ( ( R e. Ring /\ U e. L ) -> ( mulGrp ` I ) e. Smgrp )