Metamath Proof Explorer

Theorem llnle

Description: Any element greater than 0 and not an atom majorizes a lattice line. (Contributed by NM, 28-Jun-2012)

Ref Expression
Hypotheses llnle.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
llnle.l ⊢ ≤ = ( le ‘ 𝐾 )
llnle.z ⊢ 0 = ( 0. ‘ 𝐾 )
llnle.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
llnle.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
Assertion llnle ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) → ∃ 𝑦 ∈ 𝑁 𝑦 ≤ 𝑋 )

Proof

Step Hyp Ref Expression
1 llnle.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 llnle.l ⊢ ≤ = ( le ‘ 𝐾 )
3 llnle.z ⊢ 0 = ( 0. ‘ 𝐾 )
4 llnle.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 llnle.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
6 simpll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) → 𝐾 ∈ HL )
7 simplr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) → 𝑋 ∈ 𝐵 )
8 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) → 𝑋 ≠ 0 )
9 1 2 3 4 atle ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∃ 𝑝 ∈ 𝐴 𝑝 ≤ 𝑋 )
10 6 7 8 9 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) → ∃ 𝑝 ∈ 𝐴 𝑝 ≤ 𝑋 )
11 simp1ll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ) → 𝐾 ∈ HL )
12 1 4 atbase ⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵 )
13 12 3ad2ant2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ) → 𝑝 ∈ 𝐵 )
14 simp1lr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ) → 𝑋 ∈ 𝐵 )
15 simp3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ) → 𝑝 ≤ 𝑋 )
16 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ) → 𝑝 ∈ 𝐴 )
17 simp1rr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ) → ¬ 𝑋 ∈ 𝐴 )
18 nelne2 ⊢ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴 ) → 𝑝 ≠ 𝑋 )
19 16 17 18 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ) → 𝑝 ≠ 𝑋 )
20 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
21 2 20 pltval ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑝 ( lt ‘ 𝐾 ) 𝑋 ↔ ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≠ 𝑋 ) ) )
22 11 16 14 21 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ) → ( 𝑝 ( lt ‘ 𝐾 ) 𝑋 ↔ ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≠ 𝑋 ) ) )
23 15 19 22 mpbir2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ) → 𝑝 ( lt ‘ 𝐾 ) 𝑋 )
24 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
25 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
26 1 2 20 24 25 4 hlrelat3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑋 ) → ∃ 𝑞 ∈ 𝐴 ( 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ≤ 𝑋 ) )
27 11 13 14 23 26 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ) → ∃ 𝑞 ∈ 𝐴 ( 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ≤ 𝑋 ) )
28 simp1ll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ≤ 𝑋 ) ) → 𝐾 ∈ HL )
29 simp21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ≤ 𝑋 ) ) → 𝑝 ∈ 𝐴 )
30 simp23 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ≤ 𝑋 ) ) → 𝑞 ∈ 𝐴 )
31 1 24 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ 𝐵 )
32 28 29 30 31 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ≤ 𝑋 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ 𝐵 )
33 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ≤ 𝑋 ) ) → 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) )
34 1 25 4 5 llni ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ 𝐵 ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ 𝑁 )
35 28 32 29 33 34 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ≤ 𝑋 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ 𝑁 )
36 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ≤ 𝑋 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ≤ 𝑋 )
37 breq1 ⊢ ( 𝑦 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → ( 𝑦 ≤ 𝑋 ↔ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ≤ 𝑋 ) )
38 37 rspcev ⊢ ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ 𝑁 ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ≤ 𝑋 ) → ∃ 𝑦 ∈ 𝑁 𝑦 ≤ 𝑋 )
39 35 36 38 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ≤ 𝑋 ) ) → ∃ 𝑦 ∈ 𝑁 𝑦 ≤ 𝑋 )
40 39 3exp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ∧ 𝑞 ∈ 𝐴 ) → ( ( 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ≤ 𝑋 ) → ∃ 𝑦 ∈ 𝑁 𝑦 ≤ 𝑋 ) ) )
41 40 3expd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) → ( 𝑝 ∈ 𝐴 → ( 𝑝 ≤ 𝑋 → ( 𝑞 ∈ 𝐴 → ( ( 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ≤ 𝑋 ) → ∃ 𝑦 ∈ 𝑁 𝑦 ≤ 𝑋 ) ) ) ) )
42 41 3imp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ) → ( 𝑞 ∈ 𝐴 → ( ( 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ≤ 𝑋 ) → ∃ 𝑦 ∈ 𝑁 𝑦 ≤ 𝑋 ) ) )
43 42 rexlimdv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ) → ( ∃ 𝑞 ∈ 𝐴 ( 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ≤ 𝑋 ) → ∃ 𝑦 ∈ 𝑁 𝑦 ≤ 𝑋 ) )
44 27 43 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑋 ) → ∃ 𝑦 ∈ 𝑁 𝑦 ≤ 𝑋 )
45 44 3exp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) → ( 𝑝 ∈ 𝐴 → ( 𝑝 ≤ 𝑋 → ∃ 𝑦 ∈ 𝑁 𝑦 ≤ 𝑋 ) ) )
46 45 rexlimdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) → ( ∃ 𝑝 ∈ 𝐴 𝑝 ≤ 𝑋 → ∃ 𝑦 ∈ 𝑁 𝑦 ≤ 𝑋 ) )
47 10 46 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) → ∃ 𝑦 ∈ 𝑁 𝑦 ≤ 𝑋 )