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 ⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
lidlabl.i ⊢ 𝐼 = ( 𝑅 ↾s 𝑈 )
Assertion lidlmsgrp ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( mulGrp ‘ 𝐼 ) ∈ Smgrp )

Proof

Step Hyp Ref Expression
1 lidlabl.l ⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
2 lidlabl.i ⊢ 𝐼 = ( 𝑅 ↾s 𝑈 )
3 1 2 lidlmmgm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( mulGrp ‘ 𝐼 ) ∈ Mgm )
4 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
5 4 ringmgp ⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
6 5 ad2antrr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
7 1 2 lidlssbas ⊢ ( 𝑈 ∈ 𝐿 → ( Base ‘ 𝐼 ) ⊆ ( Base ‘ 𝑅 ) )
8 7 sseld ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑎 ∈ ( Base ‘ 𝐼 ) → 𝑎 ∈ ( Base ‘ 𝑅 ) ) )
9 7 sseld ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑏 ∈ ( Base ‘ 𝐼 ) → 𝑏 ∈ ( Base ‘ 𝑅 ) ) )
10 7 sseld ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑐 ∈ ( Base ‘ 𝐼 ) → 𝑐 ∈ ( Base ‘ 𝑅 ) ) )
11 8 9 10 3anim123d ⊢ ( 𝑈 ∈ 𝐿 → ( ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ) )
12 11 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ) )
13 12 imp ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) )
14 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
15 4 14 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
16 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
17 4 16 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
18 15 17 mndass ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) )
19 6 13 18 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) ) → ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) )
20 19 ralrimivvva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ∀ 𝑐 ∈ ( Base ‘ 𝐼 ) ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) )
21 2 16 ressmulr ⊢ ( 𝑈 ∈ 𝐿 → ( .r ‘ 𝑅 ) = ( .r ‘ 𝐼 ) )
22 21 eqcomd ⊢ ( 𝑈 ∈ 𝐿 → ( .r ‘ 𝐼 ) = ( .r ‘ 𝑅 ) )
23 22 oveqd ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) = ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) )
24 eqidd ⊢ ( 𝑈 ∈ 𝐿 → 𝑐 = 𝑐 )
25 22 23 24 oveq123d ⊢ ( 𝑈 ∈ 𝐿 → ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) )
26 eqidd ⊢ ( 𝑈 ∈ 𝐿 → 𝑎 = 𝑎 )
27 22 oveqd ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) = ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) )
28 22 26 27 oveq123d ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) = ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) )
29 25 28 eqeq12d ⊢ ( 𝑈 ∈ 𝐿 → ( ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ↔ ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) ) )
30 29 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ↔ ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) ) )
31 30 ralbidv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( ∀ 𝑐 ∈ ( Base ‘ 𝐼 ) ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ↔ ∀ 𝑐 ∈ ( Base ‘ 𝐼 ) ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) ) )
32 31 2ralbidv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ∀ 𝑐 ∈ ( Base ‘ 𝐼 ) ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ↔ ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ∀ 𝑐 ∈ ( Base ‘ 𝐼 ) ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) ) )
33 20 32 mpbird ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ∀ 𝑐 ∈ ( Base ‘ 𝐼 ) ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) )
34 eqid ⊢ ( mulGrp ‘ 𝐼 ) = ( mulGrp ‘ 𝐼 )
35 eqid ⊢ ( Base ‘ 𝐼 ) = ( Base ‘ 𝐼 )
36 34 35 mgpbas ⊢ ( Base ‘ 𝐼 ) = ( Base ‘ ( mulGrp ‘ 𝐼 ) )
37 eqid ⊢ ( .r ‘ 𝐼 ) = ( .r ‘ 𝐼 )
38 34 37 mgpplusg ⊢ ( .r ‘ 𝐼 ) = ( +g ‘ ( mulGrp ‘ 𝐼 ) )
39 36 38 issgrp ⊢ ( ( mulGrp ‘ 𝐼 ) ∈ Smgrp ↔ ( ( mulGrp ‘ 𝐼 ) ∈ Mgm ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ∀ 𝑐 ∈ ( Base ‘ 𝐼 ) ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ) )
40 3 33 39 sylanbrc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( mulGrp ‘ 𝐼 ) ∈ Smgrp )