This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subrgsubm

Description: A subring is a submonoid of the multiplicative monoid. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypothesis subrgsubm.1 ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
Assertion subrgsubm ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ∈ ( SubMnd ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 subrgsubm.1 ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
2 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3 2 subrgss ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
4 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
5 4 subrg1cl ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) ∈ 𝐴 )
6 subrgrcl ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )
7 eqid ⊢ ( 𝑅 ↾s 𝐴 ) = ( 𝑅 ↾s 𝐴 )
8 7 1 mgpress ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) → ( 𝑀 ↾s 𝐴 ) = ( mulGrp ‘ ( 𝑅 ↾s 𝐴 ) ) )
9 6 8 mpancom ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑀 ↾s 𝐴 ) = ( mulGrp ‘ ( 𝑅 ↾s 𝐴 ) ) )
10 7 subrgring ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑅 ↾s 𝐴 ) ∈ Ring )
11 eqid ⊢ ( mulGrp ‘ ( 𝑅 ↾s 𝐴 ) ) = ( mulGrp ‘ ( 𝑅 ↾s 𝐴 ) )
12 11 ringmgp ⊢ ( ( 𝑅 ↾s 𝐴 ) ∈ Ring → ( mulGrp ‘ ( 𝑅 ↾s 𝐴 ) ) ∈ Mnd )
13 10 12 syl ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( mulGrp ‘ ( 𝑅 ↾s 𝐴 ) ) ∈ Mnd )
14 9 13 eqeltrd ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑀 ↾s 𝐴 ) ∈ Mnd )
15 1 ringmgp ⊢ ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
16 1 2 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑀 )
17 1 4 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑀 )
18 eqid ⊢ ( 𝑀 ↾s 𝐴 ) = ( 𝑀 ↾s 𝐴 )
19 16 17 18 issubm2 ⊢ ( 𝑀 ∈ Mnd → ( 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( 𝐴 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐴 ∧ ( 𝑀 ↾s 𝐴 ) ∈ Mnd ) ) )
20 6 15 19 3syl ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( 𝐴 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐴 ∧ ( 𝑀 ↾s 𝐴 ) ∈ Mnd ) ) )
21 3 5 14 20 mpbir3and ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ∈ ( SubMnd ‘ 𝑀 ) )