Description: A field is a division ring. (Contributed by SN, 17-Jan-2025)
Ref | Expression | ||
---|---|---|---|
Hypothesis | flddrngd.1 | ⊢ ( 𝜑 → 𝑅 ∈ Field ) | |
Assertion | flddrngd | ⊢ ( 𝜑 → 𝑅 ∈ DivRing ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | flddrngd.1 | ⊢ ( 𝜑 → 𝑅 ∈ Field ) | |
2 | isfld | ⊢ ( 𝑅 ∈ Field ↔ ( 𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing ) ) | |
3 | 2 | simplbi | ⊢ ( 𝑅 ∈ Field → 𝑅 ∈ DivRing ) |
4 | 1 3 | syl | ⊢ ( 𝜑 → 𝑅 ∈ DivRing ) |