Description: A field is a commutative ring. (Contributed by SN, 23-Nov-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | fldcrngd.1 | ⊢ ( 𝜑 → 𝑅 ∈ Field ) | |
Assertion | fldcrngd | ⊢ ( 𝜑 → 𝑅 ∈ CRing ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fldcrngd.1 | ⊢ ( 𝜑 → 𝑅 ∈ Field ) | |
2 | isfld | ⊢ ( 𝑅 ∈ Field ↔ ( 𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing ) ) | |
3 | 2 | simprbi | ⊢ ( 𝑅 ∈ Field → 𝑅 ∈ CRing ) |
4 | 1 3 | syl | ⊢ ( 𝜑 → 𝑅 ∈ CRing ) |