Metamath Proof Explorer

Theorem lidlmmgm

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

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

Proof

Step Hyp Ref Expression
1 lidlabl.l 
 |-  L = ( LIdeal ` R )
2 lidlabl.i 
 |-  I = ( R |`s U )
3 1 2 lidlbas 
 |-  ( U e. L -> ( Base ` I ) = U )
4 eleq1a 
 |-  ( U e. L -> ( ( Base ` I ) = U -> ( Base ` I ) e. L ) )
5 3 4 mpd 
 |-  ( U e. L -> ( Base ` I ) e. L )
6 5 anim2i 
 |-  ( ( R e. Ring /\ U e. L ) -> ( R e. Ring /\ ( Base ` I ) e. L ) )
7 6 adantr 
 |-  ( ( ( R e. Ring /\ U e. L ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) ) ) -> ( R e. Ring /\ ( Base ` I ) e. L ) )
8 1 2 lidlssbas 
 |-  ( U e. L -> ( Base ` I ) C_ ( Base ` R ) )
9 8 adantl 
 |-  ( ( R e. Ring /\ U e. L ) -> ( Base ` I ) C_ ( Base ` R ) )
10 9 sseld 
 |-  ( ( R e. Ring /\ U e. L ) -> ( a e. ( Base ` I ) -> a e. ( Base ` R ) ) )
11 10 com12 
 |-  ( a e. ( Base ` I ) -> ( ( R e. Ring /\ U e. L ) -> a e. ( Base ` R ) ) )
12 11 adantr 
 |-  ( ( a e. ( Base ` I ) /\ b e. ( Base ` I ) ) -> ( ( R e. Ring /\ U e. L ) -> a e. ( Base ` R ) ) )
13 12 impcom 
 |-  ( ( ( R e. Ring /\ U e. L ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) ) ) -> a e. ( Base ` R ) )
14 simprr 
 |-  ( ( ( R e. Ring /\ U e. L ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) ) ) -> b e. ( Base ` I ) )
15 eqid 
 |-  ( Base ` R ) = ( Base ` R )
16 eqid 
 |-  ( .r ` R ) = ( .r ` R )
17 1 15 16 lidlmcl 
 |-  ( ( ( R e. Ring /\ ( Base ` I ) e. L ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` I ) ) ) -> ( a ( .r ` R ) b ) e. ( Base ` I ) )
18 7 13 14 17 syl12anc 
 |-  ( ( ( R e. Ring /\ U e. L ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) ) ) -> ( a ( .r ` R ) b ) e. ( Base ` I ) )
19 18 ralrimivva 
 |-  ( ( R e. Ring /\ U e. L ) -> A. a e. ( Base ` I ) A. b e. ( Base ` I ) ( a ( .r ` R ) b ) e. ( Base ` I ) )
20 fvex 
 |-  ( mulGrp ` I ) e. _V
21 eqid 
 |-  ( mulGrp ` I ) = ( mulGrp ` I )
22 eqid 
 |-  ( Base ` I ) = ( Base ` I )
23 21 22 mgpbas 
 |-  ( Base ` I ) = ( Base ` ( mulGrp ` I ) )
24 eqid 
 |-  ( .r ` I ) = ( .r ` I )
25 21 24 mgpplusg 
 |-  ( .r ` I ) = ( +g ` ( mulGrp ` I ) )
26 23 25 ismgm 
 |-  ( ( mulGrp ` I ) e. _V -> ( ( mulGrp ` I ) e. Mgm <-> A. a e. ( Base ` I ) A. b e. ( Base ` I ) ( a ( .r ` I ) b ) e. ( Base ` I ) ) )
27 20 26 mp1i 
 |-  ( ( R e. Ring /\ U e. L ) -> ( ( mulGrp ` I ) e. Mgm <-> A. a e. ( Base ` I ) A. b e. ( Base ` I ) ( a ( .r ` I ) b ) e. ( Base ` I ) ) )
28 2 16 ressmulr 
 |-  ( U e. L -> ( .r ` R ) = ( .r ` I ) )
29 28 eqcomd 
 |-  ( U e. L -> ( .r ` I ) = ( .r ` R ) )
30 29 adantl 
 |-  ( ( R e. Ring /\ U e. L ) -> ( .r ` I ) = ( .r ` R ) )
31 30 oveqdr 
 |-  ( ( ( R e. Ring /\ U e. L ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) ) ) -> ( a ( .r ` I ) b ) = ( a ( .r ` R ) b ) )
32 31 eleq1d 
 |-  ( ( ( R e. Ring /\ U e. L ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) ) ) -> ( ( a ( .r ` I ) b ) e. ( Base ` I ) <-> ( a ( .r ` R ) b ) e. ( Base ` I ) ) )
33 32 2ralbidva 
 |-  ( ( R e. Ring /\ U e. L ) -> ( A. a e. ( Base ` I ) A. b e. ( Base ` I ) ( a ( .r ` I ) b ) e. ( Base ` I ) <-> A. a e. ( Base ` I ) A. b e. ( Base ` I ) ( a ( .r ` R ) b ) e. ( Base ` I ) ) )
34 27 33 bitrd 
 |-  ( ( R e. Ring /\ U e. L ) -> ( ( mulGrp ` I ) e. Mgm <-> A. a e. ( Base ` I ) A. b e. ( Base ` I ) ( a ( .r ` R ) b ) e. ( Base ` I ) ) )
35 19 34 mpbird 
 |-  ( ( R e. Ring /\ U e. L ) -> ( mulGrp ` I ) e. Mgm )