Metamath Proof Explorer

Theorem rnglidlmmgm

Description: The multiplicative group of a (left) ideal of a non-unital ring is a magma. (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 rnglidlmmgm 
|- ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> ( mulGrp ` I ) e. Mgm )

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 simp1 
 |-  ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> R e. Rng )
5 1 2 lidlbas 
 |-  ( U e. L -> ( Base ` I ) = U )
6 eleq1a 
 |-  ( U e. L -> ( ( Base ` I ) = U -> ( Base ` I ) e. L ) )
7 5 6 mpd 
 |-  ( U e. L -> ( Base ` I ) e. L )
8 7 3ad2ant2 
 |-  ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> ( Base ` I ) e. L )
9 5 eqcomd 
 |-  ( U e. L -> U = ( Base ` I ) )
10 9 eleq2d 
 |-  ( U e. L -> ( .0. e. U <-> .0. e. ( Base ` I ) ) )
11 10 biimpa 
 |-  ( ( U e. L /\ .0. e. U ) -> .0. e. ( Base ` I ) )
12 11 3adant1 
 |-  ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> .0. e. ( Base ` I ) )
13 4 8 12 3jca 
 |-  ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> ( R e. Rng /\ ( Base ` I ) e. L /\ .0. e. ( Base ` I ) ) )
14 1 2 lidlssbas 
 |-  ( U e. L -> ( Base ` I ) C_ ( Base ` R ) )
15 14 sseld 
 |-  ( U e. L -> ( a e. ( Base ` I ) -> a e. ( Base ` R ) ) )
16 15 3ad2ant2 
 |-  ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> ( a e. ( Base ` I ) -> a e. ( Base ` R ) ) )
17 16 anim1d 
 |-  ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> ( ( a e. ( Base ` I ) /\ b e. ( Base ` I ) ) -> ( a e. ( Base ` R ) /\ b e. ( Base ` I ) ) ) )
18 17 imp 
 |-  ( ( ( R e. Rng /\ U e. L /\ .0. e. U ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) ) ) -> ( a e. ( Base ` R ) /\ b e. ( Base ` I ) ) )
19 eqid 
 |-  ( Base ` R ) = ( Base ` R )
20 eqid 
 |-  ( .r ` R ) = ( .r ` R )
21 3 19 20 1 rnglidlmcl 
 |-  ( ( ( R e. Rng /\ ( Base ` I ) e. L /\ .0. e. ( Base ` I ) ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` I ) ) ) -> ( a ( .r ` R ) b ) e. ( Base ` I ) )
22 13 18 21 syl2an2r 
 |-  ( ( ( R e. Rng /\ U e. L /\ .0. e. U ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) ) ) -> ( a ( .r ` R ) b ) e. ( Base ` I ) )
23 2 20 ressmulr 
 |-  ( U e. L -> ( .r ` R ) = ( .r ` I ) )
24 23 eqcomd 
 |-  ( U e. L -> ( .r ` I ) = ( .r ` R ) )
25 24 oveqd 
 |-  ( U e. L -> ( a ( .r ` I ) b ) = ( a ( .r ` R ) b ) )
26 25 eleq1d 
 |-  ( U e. L -> ( ( a ( .r ` I ) b ) e. ( Base ` I ) <-> ( a ( .r ` R ) b ) e. ( Base ` I ) ) )
27 26 3ad2ant2 
 |-  ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> ( ( a ( .r ` I ) b ) e. ( Base ` I ) <-> ( a ( .r ` R ) b ) e. ( Base ` I ) ) )
28 27 adantr 
 |-  ( ( ( R e. Rng /\ U e. L /\ .0. e. U ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) ) ) -> ( ( a ( .r ` I ) b ) e. ( Base ` I ) <-> ( a ( .r ` R ) b ) e. ( Base ` I ) ) )
29 22 28 mpbird 
 |-  ( ( ( R e. Rng /\ U e. L /\ .0. e. U ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) ) ) -> ( a ( .r ` I ) b ) e. ( Base ` I ) )
30 29 ralrimivva 
 |-  ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> A. a e. ( Base ` I ) A. b e. ( Base ` I ) ( a ( .r ` I ) b ) e. ( Base ` I ) )
31 fvex 
 |-  ( mulGrp ` I ) e. _V
32 eqid 
 |-  ( mulGrp ` I ) = ( mulGrp ` I )
33 eqid 
 |-  ( Base ` I ) = ( Base ` I )
34 32 33 mgpbas 
 |-  ( Base ` I ) = ( Base ` ( mulGrp ` I ) )
35 eqid 
 |-  ( .r ` I ) = ( .r ` I )
36 32 35 mgpplusg 
 |-  ( .r ` I ) = ( +g ` ( mulGrp ` I ) )
37 34 36 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 ) ) )
38 31 37 mp1i 
 |-  ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> ( ( mulGrp ` I ) e. Mgm <-> A. a e. ( Base ` I ) A. b e. ( Base ` I ) ( a ( .r ` I ) b ) e. ( Base ` I ) ) )
39 30 38 mpbird 
 |-  ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> ( mulGrp ` I ) e. Mgm )