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

Proof

Step Hyp Ref Expression
1 lidlabl.l ⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
2 lidlabl.i ⊢ 𝐼 = ( 𝑅 ↾s 𝑈 )
3 1 2 lidlbas ⊢ ( 𝑈 ∈ 𝐿 → ( Base ‘ 𝐼 ) = 𝑈 )
4 eleq1a ⊢ ( 𝑈 ∈ 𝐿 → ( ( Base ‘ 𝐼 ) = 𝑈 → ( Base ‘ 𝐼 ) ∈ 𝐿 ) )
5 3 4 mpd ⊢ ( 𝑈 ∈ 𝐿 → ( Base ‘ 𝐼 ) ∈ 𝐿 )
6 5 anim2i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( 𝑅 ∈ Ring ∧ ( Base ‘ 𝐼 ) ∈ 𝐿 ) )
7 6 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ) ) → ( 𝑅 ∈ Ring ∧ ( Base ‘ 𝐼 ) ∈ 𝐿 ) )
8 1 2 lidlssbas ⊢ ( 𝑈 ∈ 𝐿 → ( Base ‘ 𝐼 ) ⊆ ( Base ‘ 𝑅 ) )
9 8 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( Base ‘ 𝐼 ) ⊆ ( Base ‘ 𝑅 ) )
10 9 sseld ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( 𝑎 ∈ ( Base ‘ 𝐼 ) → 𝑎 ∈ ( Base ‘ 𝑅 ) ) )
11 10 com12 ⊢ ( 𝑎 ∈ ( Base ‘ 𝐼 ) → ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → 𝑎 ∈ ( Base ‘ 𝑅 ) ) )
12 11 adantr ⊢ ( ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ) → ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → 𝑎 ∈ ( Base ‘ 𝑅 ) ) )
13 12 impcom ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
14 simprr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ) ) → 𝑏 ∈ ( Base ‘ 𝐼 ) )
15 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
17 1 15 16 lidlmcl ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( Base ‘ 𝐼 ) ∈ 𝐿 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) )
18 7 13 14 17 syl12anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) )
19 18 ralrimivva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) )
20 fvex ⊢ ( mulGrp ‘ 𝐼 ) ∈ V
21 eqid ⊢ ( mulGrp ‘ 𝐼 ) = ( mulGrp ‘ 𝐼 )
22 eqid ⊢ ( Base ‘ 𝐼 ) = ( Base ‘ 𝐼 )
23 21 22 mgpbas ⊢ ( Base ‘ 𝐼 ) = ( Base ‘ ( mulGrp ‘ 𝐼 ) )
24 eqid ⊢ ( .r ‘ 𝐼 ) = ( .r ‘ 𝐼 )
25 21 24 mgpplusg ⊢ ( .r ‘ 𝐼 ) = ( +g ‘ ( mulGrp ‘ 𝐼 ) )
26 23 25 ismgm ⊢ ( ( mulGrp ‘ 𝐼 ) ∈ V → ( ( mulGrp ‘ 𝐼 ) ∈ Mgm ↔ ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) ) )
27 20 26 mp1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( ( mulGrp ‘ 𝐼 ) ∈ Mgm ↔ ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) ) )
28 2 16 ressmulr ⊢ ( 𝑈 ∈ 𝐿 → ( .r ‘ 𝑅 ) = ( .r ‘ 𝐼 ) )
29 28 eqcomd ⊢ ( 𝑈 ∈ 𝐿 → ( .r ‘ 𝐼 ) = ( .r ‘ 𝑅 ) )
30 29 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( .r ‘ 𝐼 ) = ( .r ‘ 𝑅 ) )
31 30 oveqdr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ) ) → ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) = ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) )
32 31 eleq1d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ) ) → ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) ↔ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) ) )
33 32 2ralbidva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) ↔ ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) ) )
34 27 33 bitrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( ( mulGrp ‘ 𝐼 ) ∈ Mgm ↔ ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) ) )
35 19 34 mpbird ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( mulGrp ‘ 𝐼 ) ∈ Mgm )