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 ∧ ¬ 𝑋𝐴 ) ) → ∃ 𝑦𝑁 𝑦 𝑋 )