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 )