Metamath Proof Explorer


Theorem lplnexllnN

Description: Given an atom on a lattice plane, there is a lattice line whose join with the atom equals the plane. (Contributed by NM, 26-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lplnexat.l = ( le ‘ 𝐾 )
lplnexat.j = ( join ‘ 𝐾 )
lplnexat.a 𝐴 = ( Atoms ‘ 𝐾 )
lplnexat.n 𝑁 = ( LLines ‘ 𝐾 )
lplnexat.p 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion lplnexllnN ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) → ∃ 𝑦𝑁 ( ¬ 𝑄 𝑦𝑋 = ( 𝑦 𝑄 ) ) )

Proof

Step Hyp Ref Expression
1 lplnexat.l = ( le ‘ 𝐾 )
2 lplnexat.j = ( join ‘ 𝐾 )
3 lplnexat.a 𝐴 = ( Atoms ‘ 𝐾 )
4 lplnexat.n 𝑁 = ( LLines ‘ 𝐾 )
5 lplnexat.p 𝑃 = ( LPlanes ‘ 𝐾 )
6 simpl2 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) → 𝑋𝑃 )
7 simpl1 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) → 𝐾 ∈ HL )
8 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9 8 5 lplnbase ( 𝑋𝑃𝑋 ∈ ( Base ‘ 𝐾 ) )
10 6 9 syl ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
11 8 1 2 3 4 5 islpln3 ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋𝑃 ↔ ∃ 𝑧𝑁𝑟𝐴 ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) )
12 7 10 11 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) → ( 𝑋𝑃 ↔ ∃ 𝑧𝑁𝑟𝐴 ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) )
13 6 12 mpbid ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) → ∃ 𝑧𝑁𝑟𝐴 ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) )
14 simpll1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → 𝐾 ∈ HL )
15 simpr2l ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → 𝑧𝑁 )
16 simpll3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → 𝑄𝐴 )
17 simpr1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → 𝑄 𝑧 )
18 1 2 3 4 llnexatN ( ( ( 𝐾 ∈ HL ∧ 𝑧𝑁𝑄𝐴 ) ∧ 𝑄 𝑧 ) → ∃ 𝑠𝐴 ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) )
19 14 15 16 17 18 syl31anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → ∃ 𝑠𝐴 ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) )
20 simp1l1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → 𝐾 ∈ HL )
21 simp22r ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → 𝑟𝐴 )
22 simp3l ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → 𝑠𝐴 )
23 simp1l3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → 𝑄𝐴 )
24 simp23l ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → ¬ 𝑟 𝑧 )
25 simp3rr ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → 𝑧 = ( 𝑄 𝑠 ) )
26 25 breq2d ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → ( 𝑟 𝑧𝑟 ( 𝑄 𝑠 ) ) )
27 24 26 mtbid ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → ¬ 𝑟 ( 𝑄 𝑠 ) )
28 1 2 3 atnlej2 ( ( 𝐾 ∈ HL ∧ ( 𝑟𝐴𝑄𝐴𝑠𝐴 ) ∧ ¬ 𝑟 ( 𝑄 𝑠 ) ) → 𝑟𝑠 )
29 20 21 23 22 27 28 syl131anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → 𝑟𝑠 )
30 2 3 4 llni2 ( ( ( 𝐾 ∈ HL ∧ 𝑟𝐴𝑠𝐴 ) ∧ 𝑟𝑠 ) → ( 𝑟 𝑠 ) ∈ 𝑁 )
31 20 21 22 29 30 syl31anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → ( 𝑟 𝑠 ) ∈ 𝑁 )
32 simp3rl ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → 𝑄𝑠 )
33 1 2 3 hlatcon2 ( ( 𝐾 ∈ HL ∧ ( 𝑄𝐴𝑠𝐴𝑟𝐴 ) ∧ ( 𝑄𝑠 ∧ ¬ 𝑟 ( 𝑄 𝑠 ) ) ) → ¬ 𝑄 ( 𝑟 𝑠 ) )
34 20 23 22 21 32 27 33 syl132anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → ¬ 𝑄 ( 𝑟 𝑠 ) )
35 simp23r ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → 𝑋 = ( 𝑧 𝑟 ) )
36 25 oveq1d ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → ( 𝑧 𝑟 ) = ( ( 𝑄 𝑠 ) 𝑟 ) )
37 20 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → 𝐾 ∈ Lat )
38 8 3 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
39 23 38 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
40 8 3 atbase ( 𝑠𝐴𝑠 ∈ ( Base ‘ 𝐾 ) )
41 22 40 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → 𝑠 ∈ ( Base ‘ 𝐾 ) )
42 8 3 atbase ( 𝑟𝐴𝑟 ∈ ( Base ‘ 𝐾 ) )
43 21 42 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → 𝑟 ∈ ( Base ‘ 𝐾 ) )
44 8 2 latj31 ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑠 ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑄 𝑠 ) 𝑟 ) = ( ( 𝑟 𝑠 ) 𝑄 ) )
45 37 39 41 43 44 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → ( ( 𝑄 𝑠 ) 𝑟 ) = ( ( 𝑟 𝑠 ) 𝑄 ) )
46 35 36 45 3eqtrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → 𝑋 = ( ( 𝑟 𝑠 ) 𝑄 ) )
47 breq2 ( 𝑦 = ( 𝑟 𝑠 ) → ( 𝑄 𝑦𝑄 ( 𝑟 𝑠 ) ) )
48 47 notbid ( 𝑦 = ( 𝑟 𝑠 ) → ( ¬ 𝑄 𝑦 ↔ ¬ 𝑄 ( 𝑟 𝑠 ) ) )
49 oveq1 ( 𝑦 = ( 𝑟 𝑠 ) → ( 𝑦 𝑄 ) = ( ( 𝑟 𝑠 ) 𝑄 ) )
50 49 eqeq2d ( 𝑦 = ( 𝑟 𝑠 ) → ( 𝑋 = ( 𝑦 𝑄 ) ↔ 𝑋 = ( ( 𝑟 𝑠 ) 𝑄 ) ) )
51 48 50 anbi12d ( 𝑦 = ( 𝑟 𝑠 ) → ( ( ¬ 𝑄 𝑦𝑋 = ( 𝑦 𝑄 ) ) ↔ ( ¬ 𝑄 ( 𝑟 𝑠 ) ∧ 𝑋 = ( ( 𝑟 𝑠 ) 𝑄 ) ) ) )
52 51 rspcev ( ( ( 𝑟 𝑠 ) ∈ 𝑁 ∧ ( ¬ 𝑄 ( 𝑟 𝑠 ) ∧ 𝑋 = ( ( 𝑟 𝑠 ) 𝑄 ) ) ) → ∃ 𝑦𝑁 ( ¬ 𝑄 𝑦𝑋 = ( 𝑦 𝑄 ) ) )
53 31 34 46 52 syl12anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ∧ ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) ) → ∃ 𝑦𝑁 ( ¬ 𝑄 𝑦𝑋 = ( 𝑦 𝑄 ) ) )
54 53 3expia ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → ( ( 𝑠𝐴 ∧ ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) ) → ∃ 𝑦𝑁 ( ¬ 𝑄 𝑦𝑋 = ( 𝑦 𝑄 ) ) ) )
55 54 expd ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → ( 𝑠𝐴 → ( ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) → ∃ 𝑦𝑁 ( ¬ 𝑄 𝑦𝑋 = ( 𝑦 𝑄 ) ) ) ) )
56 55 rexlimdv ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → ( ∃ 𝑠𝐴 ( 𝑄𝑠𝑧 = ( 𝑄 𝑠 ) ) → ∃ 𝑦𝑁 ( ¬ 𝑄 𝑦𝑋 = ( 𝑦 𝑄 ) ) ) )
57 19 56 mpd ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → ∃ 𝑦𝑁 ( ¬ 𝑄 𝑦𝑋 = ( 𝑦 𝑄 ) ) )
58 57 3exp2 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) → ( 𝑄 𝑧 → ( ( 𝑧𝑁𝑟𝐴 ) → ( ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) → ∃ 𝑦𝑁 ( ¬ 𝑄 𝑦𝑋 = ( 𝑦 𝑄 ) ) ) ) ) )
59 simpr2l ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → 𝑧𝑁 )
60 simpr1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → ¬ 𝑄 𝑧 )
61 simpll1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → 𝐾 ∈ HL )
62 61 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → 𝐾 ∈ Lat )
63 8 4 llnbase ( 𝑧𝑁𝑧 ∈ ( Base ‘ 𝐾 ) )
64 59 63 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → 𝑧 ∈ ( Base ‘ 𝐾 ) )
65 simpr2r ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → 𝑟𝐴 )
66 65 42 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → 𝑟 ∈ ( Base ‘ 𝐾 ) )
67 8 1 2 latlej1 ( ( 𝐾 ∈ Lat ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) → 𝑧 ( 𝑧 𝑟 ) )
68 62 64 66 67 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → 𝑧 ( 𝑧 𝑟 ) )
69 simpr3r ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → 𝑋 = ( 𝑧 𝑟 ) )
70 68 69 breqtrrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → 𝑧 𝑋 )
71 simplr ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → 𝑄 𝑋 )
72 simpll3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → 𝑄𝐴 )
73 72 38 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
74 simpll2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → 𝑋𝑃 )
75 74 9 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
76 8 1 2 latjle12 ( ( 𝐾 ∈ Lat ∧ ( 𝑧 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑧 𝑋𝑄 𝑋 ) ↔ ( 𝑧 𝑄 ) 𝑋 ) )
77 62 64 73 75 76 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → ( ( 𝑧 𝑋𝑄 𝑋 ) ↔ ( 𝑧 𝑄 ) 𝑋 ) )
78 70 71 77 mpbi2and ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → ( 𝑧 𝑄 ) 𝑋 )
79 8 2 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑧 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
80 62 64 73 79 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → ( 𝑧 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
81 eqid ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
82 8 1 2 81 3 cvr1 ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄𝐴 ) → ( ¬ 𝑄 𝑧𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 𝑄 ) ) )
83 61 64 72 82 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → ( ¬ 𝑄 𝑧𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 𝑄 ) ) )
84 60 83 mpbid ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 𝑄 ) )
85 8 81 4 5 lplni ( ( ( 𝐾 ∈ HL ∧ ( 𝑧 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑧𝑁 ) ∧ 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 𝑄 ) ) → ( 𝑧 𝑄 ) ∈ 𝑃 )
86 61 80 59 84 85 syl31anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → ( 𝑧 𝑄 ) ∈ 𝑃 )
87 1 5 lplncmp ( ( 𝐾 ∈ HL ∧ ( 𝑧 𝑄 ) ∈ 𝑃𝑋𝑃 ) → ( ( 𝑧 𝑄 ) 𝑋 ↔ ( 𝑧 𝑄 ) = 𝑋 ) )
88 61 86 74 87 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → ( ( 𝑧 𝑄 ) 𝑋 ↔ ( 𝑧 𝑄 ) = 𝑋 ) )
89 78 88 mpbid ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → ( 𝑧 𝑄 ) = 𝑋 )
90 89 eqcomd ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → 𝑋 = ( 𝑧 𝑄 ) )
91 breq2 ( 𝑦 = 𝑧 → ( 𝑄 𝑦𝑄 𝑧 ) )
92 91 notbid ( 𝑦 = 𝑧 → ( ¬ 𝑄 𝑦 ↔ ¬ 𝑄 𝑧 ) )
93 oveq1 ( 𝑦 = 𝑧 → ( 𝑦 𝑄 ) = ( 𝑧 𝑄 ) )
94 93 eqeq2d ( 𝑦 = 𝑧 → ( 𝑋 = ( 𝑦 𝑄 ) ↔ 𝑋 = ( 𝑧 𝑄 ) ) )
95 92 94 anbi12d ( 𝑦 = 𝑧 → ( ( ¬ 𝑄 𝑦𝑋 = ( 𝑦 𝑄 ) ) ↔ ( ¬ 𝑄 𝑧𝑋 = ( 𝑧 𝑄 ) ) ) )
96 95 rspcev ( ( 𝑧𝑁 ∧ ( ¬ 𝑄 𝑧𝑋 = ( 𝑧 𝑄 ) ) ) → ∃ 𝑦𝑁 ( ¬ 𝑄 𝑦𝑋 = ( 𝑦 𝑄 ) ) )
97 59 60 90 96 syl12anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) ∧ ( ¬ 𝑄 𝑧 ∧ ( 𝑧𝑁𝑟𝐴 ) ∧ ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) ) ) → ∃ 𝑦𝑁 ( ¬ 𝑄 𝑦𝑋 = ( 𝑦 𝑄 ) ) )
98 97 3exp2 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) → ( ¬ 𝑄 𝑧 → ( ( 𝑧𝑁𝑟𝐴 ) → ( ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) → ∃ 𝑦𝑁 ( ¬ 𝑄 𝑦𝑋 = ( 𝑦 𝑄 ) ) ) ) ) )
99 58 98 pm2.61d ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) → ( ( 𝑧𝑁𝑟𝐴 ) → ( ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) → ∃ 𝑦𝑁 ( ¬ 𝑄 𝑦𝑋 = ( 𝑦 𝑄 ) ) ) ) )
100 99 rexlimdvv ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) → ( ∃ 𝑧𝑁𝑟𝐴 ( ¬ 𝑟 𝑧𝑋 = ( 𝑧 𝑟 ) ) → ∃ 𝑦𝑁 ( ¬ 𝑄 𝑦𝑋 = ( 𝑦 𝑄 ) ) ) )
101 13 100 mpd ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴 ) ∧ 𝑄 𝑋 ) → ∃ 𝑦𝑁 ( ¬ 𝑄 𝑦𝑋 = ( 𝑦 𝑄 ) ) )