This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rng1nfld

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

Ref Expression
Hypothesis rng1nfld.m ⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ }
Assertion rng1nfld ( 𝑍 ∈ 𝑉 → 𝑀 ∉ Field )

Proof

Step Hyp Ref Expression
1 rng1nfld.m ⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ }
2 1 rng1nnzr ⊢ ( 𝑍 ∈ 𝑉 → 𝑀 ∉ NzRing )
3 df-nel ⊢ ( 𝑀 ∉ NzRing ↔ ¬ 𝑀 ∈ NzRing )
4 2 3 sylib ⊢ ( 𝑍 ∈ 𝑉 → ¬ 𝑀 ∈ NzRing )
5 drngnzr ⊢ ( 𝑀 ∈ DivRing → 𝑀 ∈ NzRing )
6 4 5 nsyl ⊢ ( 𝑍 ∈ 𝑉 → ¬ 𝑀 ∈ DivRing )
7 isfld ⊢ ( 𝑀 ∈ Field ↔ ( 𝑀 ∈ DivRing ∧ 𝑀 ∈ CRing ) )
8 7 simplbi ⊢ ( 𝑀 ∈ Field → 𝑀 ∈ DivRing )
9 6 8 nsyl ⊢ ( 𝑍 ∈ 𝑉 → ¬ 𝑀 ∈ Field )
10 df-nel ⊢ ( 𝑀 ∉ Field ↔ ¬ 𝑀 ∈ Field )
11 9 10 sylibr ⊢ ( 𝑍 ∈ 𝑉 → 𝑀 ∉ Field )