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