This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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