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=BasendxZ+ndxZZZndxZZZ
Assertion rng1nfld ZVMField

Proof

Step Hyp Ref Expression
1 rng1nfld.m M=BasendxZ+ndxZZZndxZZZ
2 1 rng1nnzr ZVMNzRing
3 df-nel MNzRing¬MNzRing
4 2 3 sylib ZV¬MNzRing
5 drngnzr MDivRingMNzRing
6 4 5 nsyl ZV¬MDivRing
7 isfld MFieldMDivRingMCRing
8 7 simplbi MFieldMDivRing
9 6 8 nsyl ZV¬MField
10 df-nel MField¬MField
11 9 10 sylibr ZVMField