unitsubm

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

Step	Hyp	Ref	Expression
1		unitsubm.1	$⊢ U = Unit (R)$
2		unitsubm.2	$⊢ M = {mulGrp}_{R}$
3		eqid	$⊢ {Base}_{R} = {Base}_{R}$
4	3 1	unitss	$⊢ U \subseteq {Base}_{R}$
5	4	a1i	$⊢ R \in Ring \to U \subseteq {Base}_{R}$
6		eqid	$⊢ 1_{R} = 1_{R}$
7	1 6	1unit	$⊢ R \in Ring \to 1_{R} \in U$
8	2	oveq1i	$⊢ M ↾_{𝑠} U = {mulGrp}_{R} ↾_{𝑠} U$
9	1 8	unitgrp	$⊢ R \in Ring \to M ↾_{𝑠} U \in Grp$
10		grpmnd	$⊢ M ↾_{𝑠} U \in Grp \to M ↾_{𝑠} U \in Mnd$
11	9 10	syl	$⊢ R \in Ring \to M ↾_{𝑠} U \in Mnd$
12	2	ringmgp	$⊢ R \in Ring \to M \in Mnd$
13	2 3	mgpbas	$⊢ {Base}_{R} = {Base}_{M}$
14	2 6	ringidval	$⊢ 1_{R} = 0_{M}$
15		eqid	$⊢ M ↾_{𝑠} U = M ↾_{𝑠} U$
16	13 14 15	issubm2	$⊢ M \in Mnd \to (U \in SubMnd (M) \leftrightarrow (U \subseteq {Base}_{R} \land 1_{R} \in U \land M ↾_{𝑠} U \in Mnd))$
17	12 16	syl	$⊢ R \in Ring \to (U \in SubMnd (M) \leftrightarrow (U \subseteq {Base}_{R} \land 1_{R} \in U \land M ↾_{𝑠} U \in Mnd))$
18	5 7 11 17	mpbir3and	$⊢ R \in Ring \to U \in SubMnd (M)$

Metamath Proof Explorer