Theorem llnn0

Description: A lattice line is nonzero. (Contributed by NM, 15-Jul-2012)

	Ref	Expression
Hypotheses	llnn0.z	⊢ 0 = ( 0. ‘ 𝐾 )
	llnn0.n	⊢ 𝑁 = ( LLines ‘ 𝐾 )
Assertion	llnn0	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ) → 𝑋 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		llnn0.z	⊢ 0 = ( 0. ‘ 𝐾 )
2		llnn0.n	⊢ 𝑁 = ( LLines ‘ 𝐾 )
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	llnnleat	⊢ ( ( 𝐾 ∈ 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 )