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	9	grpmndd	$⊢ R \in Ring \to M ↾_{𝑠} U \in Mnd$
11	2	ringmgp	$⊢ R \in Ring \to M \in Mnd$
12	2 3	mgpbas	$⊢ {Base}_{R} = {Base}_{M}$
13	2 6	ringidval	$⊢ 1_{R} = 0_{M}$
14		eqid	$⊢ M ↾_{𝑠} U = M ↾_{𝑠} U$
15	12 13 14	issubm2	$⊢ M \in Mnd \to (U \in SubMnd (M) \leftrightarrow (U \subseteq {Base}_{R} \land 1_{R} \in U \land M ↾_{𝑠} U \in Mnd))$
16	11 15	syl	$⊢ R \in Ring \to (U \in SubMnd (M) \leftrightarrow (U \subseteq {Base}_{R} \land 1_{R} \in U \land M ↾_{𝑠} U \in Mnd))$
17	5 7 10 16	mpbir3and	$⊢ R \in Ring \to U \in SubMnd (M)$

Metamath Proof Explorer