Metamath Proof Explorer


Theorem llncvrlpln2

Description: A lattice line under a lattice plane is covered by it. (Contributed by NM, 24-Jun-2012)

Ref Expression
Hypotheses llncvrlpln2.l = ( le ‘ 𝐾 )
llncvrlpln2.c 𝐶 = ( ⋖ ‘ 𝐾 )
llncvrlpln2.n 𝑁 = ( LLines ‘ 𝐾 )
llncvrlpln2.p 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion llncvrlpln2 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ 𝑋 𝑌 ) → 𝑋 𝐶 𝑌 )

Proof

Step Hyp Ref Expression
1 llncvrlpln2.l = ( le ‘ 𝐾 )
2 llncvrlpln2.c 𝐶 = ( ⋖ ‘ 𝐾 )
3 llncvrlpln2.n 𝑁 = ( LLines ‘ 𝐾 )
4 llncvrlpln2.p 𝑃 = ( LPlanes ‘ 𝐾 )
5 simpr ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ 𝑋 𝑌 ) → 𝑋 𝑌 )
6 simpl1 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ 𝑋 𝑌 ) → 𝐾 ∈ HL )
7 simpl3 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ 𝑋 𝑌 ) → 𝑌𝑃 )
8 3 4 lplnnelln ( ( 𝐾 ∈ HL ∧ 𝑌𝑃 ) → ¬ 𝑌𝑁 )
9 6 7 8 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ 𝑋 𝑌 ) → ¬ 𝑌𝑁 )
10 simpl2 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ 𝑋 𝑌 ) → 𝑋𝑁 )
11 eleq1 ( 𝑋 = 𝑌 → ( 𝑋𝑁𝑌𝑁 ) )
12 10 11 syl5ibcom ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ 𝑋 𝑌 ) → ( 𝑋 = 𝑌𝑌𝑁 ) )
13 12 necon3bd ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ 𝑋 𝑌 ) → ( ¬ 𝑌𝑁𝑋𝑌 ) )
14 9 13 mpd ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ 𝑋 𝑌 ) → 𝑋𝑌 )
15 eqid ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
16 1 15 pltval ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝑋 𝑌𝑋𝑌 ) ) )
17 16 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ 𝑋 𝑌 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝑋 𝑌𝑋𝑌 ) ) )
18 5 14 17 mpbir2and ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ 𝑋 𝑌 ) → 𝑋 ( lt ‘ 𝐾 ) 𝑌 )
19 simpl1 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝐾 ∈ HL )
20 simpl2 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑋𝑁 )
21 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
22 21 3 llnbase ( 𝑋𝑁𝑋 ∈ ( Base ‘ 𝐾 ) )
23 20 22 syl ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
24 simpl3 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑌𝑃 )
25 21 4 lplnbase ( 𝑌𝑃𝑌 ∈ ( Base ‘ 𝐾 ) )
26 24 25 syl ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
27 simpr ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑋 ( lt ‘ 𝐾 ) 𝑌 )
28 eqid ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
29 eqid ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
30 21 1 15 28 2 29 hlrelat3 ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) )
31 19 23 26 27 30 syl31anc ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) )
32 21 1 28 29 4 islpln2 ( 𝐾 ∈ HL → ( 𝑌𝑃 ↔ ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠𝑡 ∧ ¬ 𝑢 ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) ) ) )
33 32 adantr ( ( 𝐾 ∈ HL ∧ 𝑋𝑁 ) → ( 𝑌𝑃 ↔ ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠𝑡 ∧ ¬ 𝑢 ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) ) ) )
34 simp3 ( ( 𝑠𝑡 ∧ ¬ 𝑢 ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) → 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) )
35 21 28 29 3 islln2 ( 𝐾 ∈ HL → ( 𝑋𝑁 ↔ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) )
36 simp3l ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) )
37 simp3r ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 )
38 simp12r ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) )
39 38 oveq1d ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) )
40 simp22 ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) )
41 37 39 40 3brtr3d ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) )
42 simp111 ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → 𝐾 ∈ HL )
43 simp112 ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
44 simp113 ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → 𝑞 ∈ ( Atoms ‘ 𝐾 ) )
45 simp23 ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → 𝑟 ∈ ( Atoms ‘ 𝐾 ) )
46 43 44 45 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) )
47 simp13l ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → 𝑠 ∈ ( Atoms ‘ 𝐾 ) )
48 simp13r ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → 𝑡 ∈ ( Atoms ‘ 𝐾 ) )
49 simp21 ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → 𝑢 ∈ ( Atoms ‘ 𝐾 ) )
50 47 48 49 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) )
51 36 38 39 3brtr3d ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) )
52 21 28 29 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
53 42 43 44 52 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
54 21 1 28 2 29 cvr1 ( ( 𝐾 ∈ HL ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ¬ 𝑟 ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ↔ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) )
55 42 53 45 54 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → ( ¬ 𝑟 ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ↔ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) )
56 51 55 mpbird ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → ¬ 𝑟 ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) )
57 simp12l ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → 𝑝𝑞 )
58 1 28 29 3at ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( ¬ 𝑟 ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑝𝑞 ) ) → ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ↔ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) )
59 42 46 50 56 57 58 syl32anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ↔ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) )
60 41 59 mpbid ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) )
61 60 39 40 3eqtr4d ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) = 𝑌 )
62 36 61 breqtrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → 𝑋 𝐶 𝑌 )
63 62 3exp ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) → 𝑋 𝐶 𝑌 ) ) )
64 63 3expd ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) )
65 64 3exp ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) )
66 65 3expib ( 𝐾 ∈ HL → ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) ) )
67 66 rexlimdvv ( 𝐾 ∈ HL → ( ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) )
68 67 adantld ( 𝐾 ∈ HL → ( ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝𝑞𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) )
69 35 68 sylbid ( 𝐾 ∈ HL → ( 𝑋𝑁 → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) )
70 69 imp31 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁 ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) )
71 34 70 syl7 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁 ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑠𝑡 ∧ ¬ 𝑢 ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) )
72 71 rexlimdv ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁 ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠𝑡 ∧ ¬ 𝑢 ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) )
73 72 rexlimdvva ( ( 𝐾 ∈ HL ∧ 𝑋𝑁 ) → ( ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠𝑡 ∧ ¬ 𝑢 ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) )
74 73 adantld ( ( 𝐾 ∈ HL ∧ 𝑋𝑁 ) → ( ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠𝑡 ∧ ¬ 𝑢 ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) )
75 33 74 sylbid ( ( 𝐾 ∈ HL ∧ 𝑋𝑁 ) → ( 𝑌𝑃 → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) )
76 75 3impia ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) → 𝑋 𝐶 𝑌 ) ) )
77 76 rexlimdv ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) → ( ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) → 𝑋 𝐶 𝑌 ) )
78 77 imp ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) 𝑌 ) ) → 𝑋 𝐶 𝑌 )
79 31 78 syldan ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑋 𝐶 𝑌 )
80 18 79 syldan ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑃 ) ∧ 𝑋 𝑌 ) → 𝑋 𝐶 𝑌 )