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 ‘ 𝑀 ) )