Metamath Proof Explorer


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 → 10 )

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 ‘ 𝑅 ) ∧ 10 ) ) )
9 6 8 mpbid ( 𝑅 ∈ DivRing → ( 1 ∈ ( Base ‘ 𝑅 ) ∧ 10 ) )
10 9 simprd ( 𝑅 ∈ DivRing → 10 )