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