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 ⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ }
Assertion rng1nnzr ( 𝑍 ∈ 𝑉 → 𝑀 ∉ NzRing )

Proof

Step Hyp Ref Expression
1 rng1nnzr.m ⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ }
2 snex ⊢ { 𝑍 } ∈ V
3 1 rngbase ⊢ ( { 𝑍 } ∈ V → { 𝑍 } = ( Base ‘ 𝑀 ) )
4 2 3 mp1i ⊢ ( 𝑍 ∈ 𝑉 → { 𝑍 } = ( Base ‘ 𝑀 ) )
5 4 eqcomd ⊢ ( 𝑍 ∈ 𝑉 → ( Base ‘ 𝑀 ) = { 𝑍 } )
6 5 fveq2d ⊢ ( 𝑍 ∈ 𝑉 → ( ♯ ‘ ( Base ‘ 𝑀 ) ) = ( ♯ ‘ { 𝑍 } ) )
7 hashsng ⊢ ( 𝑍 ∈ 𝑉 → ( ♯ ‘ { 𝑍 } ) = 1 )
8 6 7 eqtrd ⊢ ( 𝑍 ∈ 𝑉 → ( ♯ ‘ ( Base ‘ 𝑀 ) ) = 1 )
9 1 ring1 ⊢ ( 𝑍 ∈ 𝑉 → 𝑀 ∈ Ring )
10 0ringnnzr ⊢ ( 𝑀 ∈ Ring → ( ( ♯ ‘ ( Base ‘ 𝑀 ) ) = 1 ↔ ¬ 𝑀 ∈ NzRing ) )
11 9 10 syl ⊢ ( 𝑍 ∈ 𝑉 → ( ( ♯ ‘ ( Base ‘ 𝑀 ) ) = 1 ↔ ¬ 𝑀 ∈ NzRing ) )
12 8 11 mpbid ⊢ ( 𝑍 ∈ 𝑉 → ¬ 𝑀 ∈ NzRing )
13 df-nel ⊢ ( 𝑀 ∉ NzRing ↔ ¬ 𝑀 ∈ NzRing )
14 12 13 sylibr ⊢ ( 𝑍 ∈ 𝑉 → 𝑀 ∉ NzRing )