Metamath Proof Explorer

Theorem rng1nfld

Description: The zero ring is not a field. (Contributed by AV, 29-Apr-2019)

Ref Expression
Hypothesis rng1nfld.m ⊢ M = Base ndx Z + ndx Z Z Z ⋅ ndx Z Z Z
Assertion rng1nfld ⊢ Z ∈ V → M ∉ Field

Proof

Step Hyp Ref Expression
1 rng1nfld.m ⊢ M = Base ndx Z + ndx Z Z Z ⋅ ndx Z Z Z
2 1 rng1nnzr ⊢ Z ∈ V → M ∉ NzRing
3 df-nel ⊢ M ∉ NzRing ↔ ¬ M ∈ NzRing
4 2 3 sylib ⊢ Z ∈ V → ¬ M ∈ NzRing
5 drngnzr ⊢ M ∈ DivRing → M ∈ NzRing
6 4 5 nsyl ⊢ Z ∈ V → ¬ M ∈ DivRing
7 isfld ⊢ M ∈ Field ↔ M ∈ DivRing ∧ M ∈ CRing
8 simpl ⊢ M ∈ DivRing ∧ M ∈ CRing → M ∈ DivRing
9 8 a1i ⊢ Z ∈ V → M ∈ DivRing ∧ M ∈ CRing → M ∈ DivRing
10 7 9 syl5bi ⊢ Z ∈ V → M ∈ Field → M ∈ DivRing
11 6 10 mtod ⊢ Z ∈ V → ¬ M ∈ Field
12 df-nel ⊢ M ∉ Field ↔ ¬ M ∈ Field
13 11 12 sylibr ⊢ Z ∈ V → M ∉ Field