Theorem drngunz

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

	Ref	Expression
Hypotheses	drngunz.z	⊢ 0 = ( 0g ‘ 𝑅 )
	drngunz.u	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	drngunz	⊢ ( 𝑅 ∈ DivRing → 1 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		drngunz.z	⊢ 0 = ( 0g ‘ 𝑅 )
2		drngunz.u	⊢ 1 = ( 1r ‘ 𝑅 )
3		drngring	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
4		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
5	4 2	1unit	⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Unit ‘ 𝑅 ) )
6	3 5	syl	⊢ ( 𝑅 ∈ DivRing → 1 ∈ ( Unit ‘ 𝑅 ) )
7		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8	7 4 1	drngunit	⊢ ( 𝑅 ∈ DivRing → ( 1 ∈ ( Unit ‘ 𝑅 ) ↔ ( 1 ∈ ( Base ‘ 𝑅 ) ∧ 1 ≠ 0 ) ) )
9	6 8	mpbid	⊢ ( 𝑅 ∈ DivRing → ( 1 ∈ ( Base ‘ 𝑅 ) ∧ 1 ≠ 0 ) )
10	9	simprd	⊢ ( 𝑅 ∈ DivRing → 1 ≠ 0 )