This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) → ¬ 𝑋 ≤ 𝑃 )