1unit

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

Step	Hyp	Ref	Expression
1		unit.1	$⊢ U = Unit (R)$
2		unit.2	$⊢ \underset{˙}{1} = 1_{R}$
3		eqid	$⊢ {Base}_{R} = {Base}_{R}$
4	3 2	ringidcl	$⊢ R \in Ring \to \underset{˙}{1} \in {Base}_{R}$
5		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
6	3 5	dvdsrid	$⊢ (R \in Ring \land \underset{˙}{1} \in {Base}_{R}) \to \underset{˙}{1} ∥_{r} (R) \underset{˙}{1}$
7	4 6	mpdan	$⊢ R \in Ring \to \underset{˙}{1} ∥_{r} (R) \underset{˙}{1}$
8		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
9	8	opprring	$⊢ R \in Ring \to {opp}_{r} (R) \in Ring$
10	8 3	opprbas	$⊢ {Base}_{R} = {Base}_{{opp}_{r} (R)}$
11		eqid	$⊢ ∥_{r} ({opp}_{r} (R)) = ∥_{r} ({opp}_{r} (R))$
12	10 11	dvdsrid	$⊢ ({opp}_{r} (R) \in Ring \land \underset{˙}{1} \in {Base}_{R}) \to \underset{˙}{1} ∥_{r} ({opp}_{r} (R)) \underset{˙}{1}$
13	9 4 12	syl2anc	$⊢ R \in Ring \to \underset{˙}{1} ∥_{r} ({opp}_{r} (R)) \underset{˙}{1}$
14	1 2 5 8 11	isunit	$⊢ \underset{˙}{1} \in U \leftrightarrow (\underset{˙}{1} ∥_{r} (R) \underset{˙}{1} \land \underset{˙}{1} ∥_{r} ({opp}_{r} (R)) \underset{˙}{1})$
15	7 13 14	sylanbrc	$⊢ R \in Ring \to \underset{˙}{1} \in U$

Metamath Proof Explorer