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		simpl	⊢ ( ( 𝑀 ∈ DivRing ∧ 𝑀 ∈ CRing ) → 𝑀 ∈ DivRing )
9	8	a1i	⊢ ( 𝑍 ∈ 𝑉 → ( ( 𝑀 ∈ DivRing ∧ 𝑀 ∈ CRing ) → 𝑀 ∈ DivRing ) )
10	7 9	syl5bi	⊢ ( 𝑍 ∈ 𝑉 → ( 𝑀 ∈ Field → 𝑀 ∈ DivRing ) )
11	6 10	mtod	⊢ ( 𝑍 ∈ 𝑉 → ¬ 𝑀 ∈ Field )
12		df-nel	⊢ ( 𝑀 ∉ Field ↔ ¬ 𝑀 ∈ Field )
13	11 12	sylibr	⊢ ( 𝑍 ∈ 𝑉 → 𝑀 ∉ Field )