Theorem unitsubm

Description: The group of units is a submonoid of the multiplicative monoid of the ring. (Contributed by Mario Carneiro, 18-Jun-2015)

	Ref	Expression
Hypotheses	unitsubm.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	unitsubm.2	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
Assertion	unitsubm	⊢ ( 𝑅 ∈ Ring → 𝑈 ∈ ( SubMnd ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		unitsubm.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
2		unitsubm.2	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
3		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4	3 1	unitss	⊢ 𝑈 ⊆ ( Base ‘ 𝑅 )
5	4	a1i	⊢ ( 𝑅 ∈ Ring → 𝑈 ⊆ ( Base ‘ 𝑅 ) )
6		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
7	1 6	1unit	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝑈 )
8	2	oveq1i	⊢ ( 𝑀 ↾s 𝑈 ) = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 )
9	1 8	unitgrp	⊢ ( 𝑅 ∈ Ring → ( 𝑀 ↾s 𝑈 ) ∈ Grp )
10	9	grpmndd	⊢ ( 𝑅 ∈ Ring → ( 𝑀 ↾s 𝑈 ) ∈ Mnd )
11	2	ringmgp	⊢ ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
12	2 3	mgpbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑀 )
13	2 6	ringidval	⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑀 )
14		eqid	⊢ ( 𝑀 ↾s 𝑈 ) = ( 𝑀 ↾s 𝑈 )
15	12 13 14	issubm2	⊢ ( 𝑀 ∈ Mnd → ( 𝑈 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( 𝑈 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝑈 ∧ ( 𝑀 ↾s 𝑈 ) ∈ Mnd ) ) )
16	11 15	syl	⊢ ( 𝑅 ∈ Ring → ( 𝑈 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( 𝑈 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝑈 ∧ ( 𝑀 ↾s 𝑈 ) ∈ Mnd ) ) )
17	5 7 10 16	mpbir3and	⊢ ( 𝑅 ∈ Ring → 𝑈 ∈ ( SubMnd ‘ 𝑀 ) )