drngid

Description: A division ring's unity is the identity element of its multiplicative group. (Contributed by NM, 7-Sep-2011)

Step	Hyp	Ref	Expression
1		drngid.b	$⊢ B = {Base}_{R}$
2		drngid.z	$⊢ \underset{˙}{0} = 0_{R}$
3		drngid.u	$⊢ \underset{˙}{1} = 1_{R}$
4		drngid.g	$⊢ G = {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\})$
5		drngring	$⊢ R \in DivRing \to R \in Ring$
6		eqid	$⊢ Unit (R) = Unit (R)$
7		eqid	$⊢ {mulGrp}_{R} ↾_{𝑠} Unit (R) = {mulGrp}_{R} ↾_{𝑠} Unit (R)$
8	6 7 3	unitgrpid	$⊢ R \in Ring \to \underset{˙}{1} = 0_{({mulGrp}_{R} ↾_{𝑠} Unit (R))}$
9	5 8	syl	$⊢ R \in DivRing \to \underset{˙}{1} = 0_{({mulGrp}_{R} ↾_{𝑠} Unit (R))}$
10	1 6 2	isdrng	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land Unit (R) = B ∖ \{\underset{˙}{0}\})$
11	10	simprbi	$⊢ R \in DivRing \to Unit (R) = B ∖ \{\underset{˙}{0}\}$
12	11	oveq2d	$⊢ R \in DivRing \to {mulGrp}_{R} ↾_{𝑠} Unit (R) = {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\})$
13	12 4	eqtr4di	$⊢ R \in DivRing \to {mulGrp}_{R} ↾_{𝑠} Unit (R) = G$
14	13	fveq2d	$⊢ R \in DivRing \to 0_{({mulGrp}_{R} ↾_{𝑠} Unit (R))} = 0_{G}$
15	9 14	eqtrd	$⊢ R \in DivRing \to \underset{˙}{1} = 0_{G}$

Metamath Proof Explorer