Theorem lplnn0N

Description: A lattice plane is nonzero. (Contributed by NM, 15-Jul-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lplnn0.z	⊢ 0 = ( 0. ‘ 𝐾 )
	lplnn0.p	⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion	lplnn0N	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) → 𝑋 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		lplnn0.z	⊢ 0 = ( 0. ‘ 𝐾 )
2		lplnn0.p	⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
3		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
4	3	atex	⊢ ( 𝐾 ∈ HL → ( Atoms ‘ 𝐾 ) ≠ ∅ )
5		n0	⊢ ( ( Atoms ‘ 𝐾 ) ≠ ∅ ↔ ∃ 𝑝 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
6	4 5	sylib	⊢ ( 𝐾 ∈ HL → ∃ 𝑝 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
7	6	adantr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) → ∃ 𝑝 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
8		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
9	8 3 2	lplnnleat	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ¬ 𝑋 ( le ‘ 𝐾 ) 𝑝 )
10	9	3expa	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ¬ 𝑋 ( le ‘ 𝐾 ) 𝑝 )
11		hlop	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
12	11	ad2antrr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝐾 ∈ OP )
13		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14	13 3	atbase	⊢ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
15	14	adantl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
16	13 8 1	op0le	⊢ ( ( 𝐾 ∈ OP ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ) → 0 ( le ‘ 𝐾 ) 𝑝 )
17	12 15 16	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 0 ( le ‘ 𝐾 ) 𝑝 )
18		breq1	⊢ ( 𝑋 = 0 → ( 𝑋 ( le ‘ 𝐾 ) 𝑝 ↔ 0 ( le ‘ 𝐾 ) 𝑝 ) )
19	17 18	syl5ibrcom	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑋 = 0 → 𝑋 ( le ‘ 𝐾 ) 𝑝 ) )
20	19	necon3bd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ¬ 𝑋 ( le ‘ 𝐾 ) 𝑝 → 𝑋 ≠ 0 ) )
21	10 20	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑋 ≠ 0 )
22	7 21	exlimddv	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) → 𝑋 ≠ 0 )