Theorem atn0

Description: An atom is not zero. ( atne0 analog.) (Contributed by NM, 5-Nov-2012)

	Ref	Expression
Hypotheses	atne0.z	⊢ 0 = ( 0. ‘ 𝐾 )
	atne0.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	atn0	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		atne0.z	⊢ 0 = ( 0. ‘ 𝐾 )
2		atne0.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
4		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5	3 4 1 2	isat3	⊢ ( 𝐾 ∈ AtLat → ( 𝑃 ∈ 𝐴 ↔ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ≠ 0 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑃 → ( 𝑥 = 𝑃 ∨ 𝑥 = 0 ) ) ) ) )
6		simp2	⊢ ( ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ≠ 0 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑃 → ( 𝑥 = 𝑃 ∨ 𝑥 = 0 ) ) ) → 𝑃 ≠ 0 )
7	5 6	biimtrdi	⊢ ( 𝐾 ∈ AtLat → ( 𝑃 ∈ 𝐴 → 𝑃 ≠ 0 ) )
8	7	imp	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ≠ 0 )