Theorem llnnleat

Description: An atom cannot majorize a lattice line. (Contributed by NM, 8-Jul-2012)

	Ref	Expression
Hypotheses	llnnleat.l	⊢ ≤ = ( le ‘ 𝐾 )
	llnnleat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	llnnleat.n	⊢ 𝑁 = ( LLines ‘ 𝐾 )
Assertion	llnnleat	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) → ¬ 𝑋 ≤ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		llnnleat.l	⊢ ≤ = ( le ‘ 𝐾 )
2		llnnleat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		llnnleat.n	⊢ 𝑁 = ( LLines ‘ 𝐾 )
4		simp2	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) → 𝑋 ∈ 𝑁 )
5		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6		eqid	⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
7	5 6 2 3	islln	⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑁 ↔ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ 𝐴 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) )
8	7	3ad2ant1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑋 ∈ 𝑁 ↔ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ 𝐴 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) )
9	4 8	mpbid	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ 𝐴 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 ) )
10	9	simprd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) → ∃ 𝑞 ∈ 𝐴 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 )
11		simp11	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 ) → 𝐾 ∈ HL )
12		hlatl	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
13	11 12	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 ) → 𝐾 ∈ AtLat )
14		simp2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 ) → 𝑞 ∈ 𝐴 )
15		simp13	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 ) → 𝑃 ∈ 𝐴 )
16		eqid	⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
17	16 2	atnlt	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑞 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) → ¬ 𝑞 ( lt ‘ 𝐾 ) 𝑃 )
18	13 14 15 17	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 ) → ¬ 𝑞 ( lt ‘ 𝐾 ) 𝑃 )
19	5 2	atbase	⊢ ( 𝑞 ∈ 𝐴 → 𝑞 ∈ ( Base ‘ 𝐾 ) )
20	19	3ad2ant2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 ) → 𝑞 ∈ ( Base ‘ 𝐾 ) )
21		simp12	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 ) → 𝑋 ∈ 𝑁 )
22	5 3	llnbase	⊢ ( 𝑋 ∈ 𝑁 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
23	21 22	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
24		simp3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 ) → 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 )
25	5 16 6	cvrlt	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 ) → 𝑞 ( lt ‘ 𝐾 ) 𝑋 )
26	11 20 23 24 25	syl31anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 ) → 𝑞 ( lt ‘ 𝐾 ) 𝑋 )
27		hlpos	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
28	11 27	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 ) → 𝐾 ∈ Poset )
29	5 2	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
30	15 29	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
31	5 1 16	pltletr	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑞 ( lt ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑃 ) → 𝑞 ( lt ‘ 𝐾 ) 𝑃 ) )
32	28 20 23 30 31	syl13anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 ) → ( ( 𝑞 ( lt ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑃 ) → 𝑞 ( lt ‘ 𝐾 ) 𝑃 ) )
33	26 32	mpand	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 ) → ( 𝑋 ≤ 𝑃 → 𝑞 ( lt ‘ 𝐾 ) 𝑃 ) )
34	18 33	mtod	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 ) → ¬ 𝑋 ≤ 𝑃 )
35	34	rexlimdv3a	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) → ( ∃ 𝑞 ∈ 𝐴 𝑞 ( ⋖ ‘ 𝐾 ) 𝑋 → ¬ 𝑋 ≤ 𝑃 ) )
36	10 35	mpd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) → ¬ 𝑋 ≤ 𝑃 )