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

Metamath Proof Explorer

Theorem rng1nnzr

Description: The (smallest) structure representing a zero ring is not a nonzero ring. (Contributed by AV, 29-Apr-2019)

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

Proof

Step Hyp Ref Expression
1 rng1nnzr.m ⊢ M = Base ndx Z + ndx Z Z Z ⋅ ndx Z Z Z
2 snex ⊢ Z ∈ V
3 1 rngbase ⊢ Z ∈ V → Z = Base M
4 2 3 mp1i ⊢ Z ∈ V → Z = Base M
5 4 eqcomd ⊢ Z ∈ V → Base M = Z
6 5 fveq2d ⊢ Z ∈ V → Base M = Z
7 hashsng ⊢ Z ∈ V → Z = 1
8 6 7 eqtrd ⊢ Z ∈ V → Base M = 1
9 1 ring1 ⊢ Z ∈ V → M ∈ Ring
10 0ringnnzr ⊢ M ∈ Ring → Base M = 1 ↔ ¬ M ∈ NzRing
11 9 10 syl ⊢ Z ∈ V → Base M = 1 ↔ ¬ M ∈ NzRing
12 8 11 mpbid ⊢ Z ∈ V → ¬ M ∈ NzRing
13 df-nel ⊢ M ∉ NzRing ↔ ¬ M ∈ NzRing
14 12 13 sylibr ⊢ Z ∈ V → M ∉ NzRing