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 ∈ Ring → U ∈ 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 ⊆ Base R
5 4 a1i ⊢ R ∈ Ring → U ⊆ Base R
6 eqid ⊢ 1 R = 1 R
7 1 6 1unit ⊢ R ∈ Ring → 1 R ∈ U
8 2 oveq1i ⊢ M ↾ 𝑠 U = mulGrp R ↾ 𝑠 U
9 1 8 unitgrp ⊢ R ∈ Ring → M ↾ 𝑠 U ∈ Grp
10 9 grpmndd ⊢ R ∈ Ring → M ↾ 𝑠 U ∈ Mnd
11 2 ringmgp ⊢ R ∈ Ring → M ∈ 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 ∈ Mnd → U ∈ SubMnd ⁡ M ↔ U ⊆ Base R ∧ 1 R ∈ U ∧ M ↾ 𝑠 U ∈ Mnd
16 11 15 syl ⊢ R ∈ Ring → U ∈ SubMnd ⁡ M ↔ U ⊆ Base R ∧ 1 R ∈ U ∧ M ↾ 𝑠 U ∈ Mnd
17 5 7 10 16 mpbir3and ⊢ R ∈ Ring → U ∈ SubMnd ⁡ M