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	|- U = ( Unit ` R )
	unitsubm.2	|- M = ( mulGrp ` R )
Assertion	unitsubm	|- ( R e. Ring -> U e. ( SubMnd ` M ) )

Proof

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 C_ ( Base ` R )
5	4	a1i	|- ( R e. Ring -> U C_ ( Base ` R ) )
6		eqid	|- ( 1r ` R ) = ( 1r ` R )
7	1 6	1unit	|- ( R e. Ring -> ( 1r ` R ) e. U )
8	2	oveq1i	|- ( M |`s U ) = ( ( mulGrp ` R ) |`s U )
9	1 8	unitgrp	|- ( R e. Ring -> ( M |`s U ) e. Grp )
10	9	grpmndd	|- ( R e. Ring -> ( M |`s U ) e. Mnd )
11	2	ringmgp	|- ( R e. Ring -> M e. Mnd )
12	2 3	mgpbas	|- ( Base ` R ) = ( Base ` M )
13	2 6	ringidval	|- ( 1r ` R ) = ( 0g ` M )
14		eqid	|- ( M |`s U ) = ( M |`s U )
15	12 13 14	issubm2	|- ( M e. Mnd -> ( U e. ( SubMnd ` M ) <-> ( U C_ ( Base ` R ) /\ ( 1r ` R ) e. U /\ ( M |`s U ) e. Mnd ) ) )
16	11 15	syl	|- ( R e. Ring -> ( U e. ( SubMnd ` M ) <-> ( U C_ ( Base ` R ) /\ ( 1r ` R ) e. U /\ ( M |`s U ) e. Mnd ) ) )
17	5 7 10 16	mpbir3and	|- ( R e. Ring -> U e. ( SubMnd ` M ) )