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

Metamath Proof Explorer

Theorem 1unit

Description: The multiplicative identity is a unit. (Contributed by Mario Carneiro, 1-Dec-2014)

Ref Expression
Hypotheses unit.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
unit.2 ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion 1unit ( 𝑅 ∈ Ring → 1 ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 unit.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
2 unit.2 ⊢ 1 = ( 1r ‘ 𝑅 )
3 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4 3 2 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
5 eqid ⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
6 3 5 dvdsrid ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ∈ ( Base ‘ 𝑅 ) ) → 1 ( ∥r ‘ 𝑅 ) 1 )
7 4 6 mpdan ⊢ ( 𝑅 ∈ Ring → 1 ( ∥r ‘ 𝑅 ) 1 )
8 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
9 8 opprring ⊢ ( 𝑅 ∈ Ring → ( oppr ‘ 𝑅 ) ∈ Ring )
10 8 3 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr ‘ 𝑅 ) )
11 eqid ⊢ ( ∥r ‘ ( oppr ‘ 𝑅 ) ) = ( ∥r ‘ ( oppr ‘ 𝑅 ) )
12 10 11 dvdsrid ⊢ ( ( ( oppr ‘ 𝑅 ) ∈ Ring ∧ 1 ∈ ( Base ‘ 𝑅 ) ) → 1 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 )
13 9 4 12 syl2anc ⊢ ( 𝑅 ∈ Ring → 1 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 )
14 1 2 5 8 11 isunit ⊢ ( 1 ∈ 𝑈 ↔ ( 1 ( ∥r ‘ 𝑅 ) 1 ∧ 1 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 ) )
15 7 13 14 sylanbrc ⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝑈 )