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 ⊢ 𝑈 = ( 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 ‘ 𝑀 ) )