drngunz

Description: A division ring's unity is different from its zero. (Contributed by NM, 8-Sep-2011)

	Ref	Expression
Hypotheses	drngunz.z	$⊢ \underset{˙}{0} = 0_{R}$
	drngunz.u	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	drngunz	$⊢ R \in DivRing \to \underset{˙}{1} \neq \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		drngunz.z	$⊢ \underset{˙}{0} = 0_{R}$
2		drngunz.u	$⊢ \underset{˙}{1} = 1_{R}$
3		drngring	$⊢ R \in DivRing \to R \in Ring$
4		eqid	$⊢ Unit (R) = Unit (R)$
5	4 2	1unit	$⊢ R \in Ring \to \underset{˙}{1} \in Unit (R)$
6	3 5	syl	$⊢ R \in DivRing \to \underset{˙}{1} \in Unit (R)$
7		eqid	$⊢ {Base}_{R} = {Base}_{R}$
8	7 4 1	drngunit	$⊢ R \in DivRing \to (\underset{˙}{1} \in Unit (R) \leftrightarrow (\underset{˙}{1} \in {Base}_{R} \land \underset{˙}{1} \neq \underset{˙}{0}))$
9	6 8	mpbid	$⊢ R \in DivRing \to (\underset{˙}{1} \in {Base}_{R} \land \underset{˙}{1} \neq \underset{˙}{0})$
10	9	simprd	$⊢ R \in DivRing \to \underset{˙}{1} \neq \underset{˙}{0}$

Metamath Proof Explorer