Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lplnexllnN Structured version   Visualization version   GIF version

Theorem lplnexllnN 36580
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.)
Hypotheses
Ref Expression
lplnexat.l = (le‘𝐾)
lplnexat.j = (join‘𝐾)
lplnexat.a 𝐴 = (Atoms‘𝐾)
lplnexat.n 𝑁 = (LLines‘𝐾)
lplnexat.p 𝑃 = (LPlanes‘𝐾)
Assertion
Ref Expression
lplnexllnN (((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) → ∃𝑦𝑁𝑄 𝑦𝑋 = (𝑦 𝑄)))
Distinct variable groups:   𝑦,   𝑦,   𝑦,𝑁   𝑦,𝑄   𝑦,𝑋
Allowed substitution hints:   𝐴(𝑦)   𝑃(𝑦)   𝐾(𝑦)

Proof of Theorem lplnexllnN
Dummy variables 𝑠 𝑟 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl2 1184 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) → 𝑋𝑃)
2 simpl1 1183 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) → 𝐾 ∈ HL)
3 eqid 2818 . . . . . 6 (Base‘𝐾) = (Base‘𝐾)
4 lplnexat.p . . . . . 6 𝑃 = (LPlanes‘𝐾)
53, 4lplnbase 36550 . . . . 5 (𝑋𝑃𝑋 ∈ (Base‘𝐾))
61, 5syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) → 𝑋 ∈ (Base‘𝐾))
7 lplnexat.l . . . . 5 = (le‘𝐾)
8 lplnexat.j . . . . 5 = (join‘𝐾)
9 lplnexat.a . . . . 5 𝐴 = (Atoms‘𝐾)
10 lplnexat.n . . . . 5 𝑁 = (LLines‘𝐾)
113, 7, 8, 9, 10, 4islpln3 36549 . . . 4 ((𝐾 ∈ HL ∧ 𝑋 ∈ (Base‘𝐾)) → (𝑋𝑃 ↔ ∃𝑧𝑁𝑟𝐴𝑟 𝑧𝑋 = (𝑧 𝑟))))
122, 6, 11syl2anc 584 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) → (𝑋𝑃 ↔ ∃𝑧𝑁𝑟𝐴𝑟 𝑧𝑋 = (𝑧 𝑟))))
131, 12mpbid 233 . 2 (((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) → ∃𝑧𝑁𝑟𝐴𝑟 𝑧𝑋 = (𝑧 𝑟)))
14 simpll1 1204 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → 𝐾 ∈ HL)
15 simpr2l 1224 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → 𝑧𝑁)
16 simpll3 1206 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → 𝑄𝐴)
17 simpr1 1186 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → 𝑄 𝑧)
187, 8, 9, 10llnexatN 36537 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑧𝑁𝑄𝐴) ∧ 𝑄 𝑧) → ∃𝑠𝐴 (𝑄𝑠𝑧 = (𝑄 𝑠)))
1914, 15, 16, 17, 18syl31anc 1365 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → ∃𝑠𝐴 (𝑄𝑠𝑧 = (𝑄 𝑠)))
20 simp1l1 1258 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → 𝐾 ∈ HL)
21 simp22r 1285 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → 𝑟𝐴)
22 simp3l 1193 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → 𝑠𝐴)
23 simp1l3 1260 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → 𝑄𝐴)
24 simp23l 1286 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → ¬ 𝑟 𝑧)
25 simp3rr 1239 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → 𝑧 = (𝑄 𝑠))
2625breq2d 5069 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → (𝑟 𝑧𝑟 (𝑄 𝑠)))
2724, 26mtbid 325 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → ¬ 𝑟 (𝑄 𝑠))
287, 8, 9atnlej2 36396 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑟𝐴𝑄𝐴𝑠𝐴) ∧ ¬ 𝑟 (𝑄 𝑠)) → 𝑟𝑠)
2920, 21, 23, 22, 27, 28syl131anc 1375 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → 𝑟𝑠)
308, 9, 10llni2 36528 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑟𝐴𝑠𝐴) ∧ 𝑟𝑠) → (𝑟 𝑠) ∈ 𝑁)
3120, 21, 22, 29, 30syl31anc 1365 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → (𝑟 𝑠) ∈ 𝑁)
32 simp3rl 1238 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → 𝑄𝑠)
337, 8, 9hlatcon2 36468 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑄𝐴𝑠𝐴𝑟𝐴) ∧ (𝑄𝑠 ∧ ¬ 𝑟 (𝑄 𝑠))) → ¬ 𝑄 (𝑟 𝑠))
3420, 23, 22, 21, 32, 27, 33syl132anc 1380 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → ¬ 𝑄 (𝑟 𝑠))
35 simp23r 1287 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → 𝑋 = (𝑧 𝑟))
3625oveq1d 7160 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → (𝑧 𝑟) = ((𝑄 𝑠) 𝑟))
3720hllatd 36380 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → 𝐾 ∈ Lat)
383, 9atbase 36305 . . . . . . . . . . . . 13 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
3923, 38syl 17 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → 𝑄 ∈ (Base‘𝐾))
403, 9atbase 36305 . . . . . . . . . . . . 13 (𝑠𝐴𝑠 ∈ (Base‘𝐾))
4122, 40syl 17 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → 𝑠 ∈ (Base‘𝐾))
423, 9atbase 36305 . . . . . . . . . . . . 13 (𝑟𝐴𝑟 ∈ (Base‘𝐾))
4321, 42syl 17 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → 𝑟 ∈ (Base‘𝐾))
443, 8latj31 17697 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ 𝑠 ∈ (Base‘𝐾) ∧ 𝑟 ∈ (Base‘𝐾))) → ((𝑄 𝑠) 𝑟) = ((𝑟 𝑠) 𝑄))
4537, 39, 41, 43, 44syl13anc 1364 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → ((𝑄 𝑠) 𝑟) = ((𝑟 𝑠) 𝑄))
4635, 36, 453eqtrd 2857 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → 𝑋 = ((𝑟 𝑠) 𝑄))
47 breq2 5061 . . . . . . . . . . . . 13 (𝑦 = (𝑟 𝑠) → (𝑄 𝑦𝑄 (𝑟 𝑠)))
4847notbid 319 . . . . . . . . . . . 12 (𝑦 = (𝑟 𝑠) → (¬ 𝑄 𝑦 ↔ ¬ 𝑄 (𝑟 𝑠)))
49 oveq1 7152 . . . . . . . . . . . . 13 (𝑦 = (𝑟 𝑠) → (𝑦 𝑄) = ((𝑟 𝑠) 𝑄))
5049eqeq2d 2829 . . . . . . . . . . . 12 (𝑦 = (𝑟 𝑠) → (𝑋 = (𝑦 𝑄) ↔ 𝑋 = ((𝑟 𝑠) 𝑄)))
5148, 50anbi12d 630 . . . . . . . . . . 11 (𝑦 = (𝑟 𝑠) → ((¬ 𝑄 𝑦𝑋 = (𝑦 𝑄)) ↔ (¬ 𝑄 (𝑟 𝑠) ∧ 𝑋 = ((𝑟 𝑠) 𝑄))))
5251rspcev 3620 . . . . . . . . . 10 (((𝑟 𝑠) ∈ 𝑁 ∧ (¬ 𝑄 (𝑟 𝑠) ∧ 𝑋 = ((𝑟 𝑠) 𝑄))) → ∃𝑦𝑁𝑄 𝑦𝑋 = (𝑦 𝑄)))
5331, 34, 46, 52syl12anc 832 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟))) ∧ (𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠)))) → ∃𝑦𝑁𝑄 𝑦𝑋 = (𝑦 𝑄)))
54533expia 1113 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → ((𝑠𝐴 ∧ (𝑄𝑠𝑧 = (𝑄 𝑠))) → ∃𝑦𝑁𝑄 𝑦𝑋 = (𝑦 𝑄))))
5554expd 416 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → (𝑠𝐴 → ((𝑄𝑠𝑧 = (𝑄 𝑠)) → ∃𝑦𝑁𝑄 𝑦𝑋 = (𝑦 𝑄)))))
5655rexlimdv 3280 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → (∃𝑠𝐴 (𝑄𝑠𝑧 = (𝑄 𝑠)) → ∃𝑦𝑁𝑄 𝑦𝑋 = (𝑦 𝑄))))
5719, 56mpd 15 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → ∃𝑦𝑁𝑄 𝑦𝑋 = (𝑦 𝑄)))
58573exp2 1346 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) → (𝑄 𝑧 → ((𝑧𝑁𝑟𝐴) → ((¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)) → ∃𝑦𝑁𝑄 𝑦𝑋 = (𝑦 𝑄))))))
59 simpr2l 1224 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → 𝑧𝑁)
60 simpr1 1186 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → ¬ 𝑄 𝑧)
61 simpll1 1204 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → 𝐾 ∈ HL)
6261hllatd 36380 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → 𝐾 ∈ Lat)
633, 10llnbase 36525 . . . . . . . . . . . 12 (𝑧𝑁𝑧 ∈ (Base‘𝐾))
6459, 63syl 17 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → 𝑧 ∈ (Base‘𝐾))
65 simpr2r 1225 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → 𝑟𝐴)
6665, 42syl 17 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → 𝑟 ∈ (Base‘𝐾))
673, 7, 8latlej1 17658 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ 𝑧 ∈ (Base‘𝐾) ∧ 𝑟 ∈ (Base‘𝐾)) → 𝑧 (𝑧 𝑟))
6862, 64, 66, 67syl3anc 1363 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → 𝑧 (𝑧 𝑟))
69 simpr3r 1227 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → 𝑋 = (𝑧 𝑟))
7068, 69breqtrrd 5085 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → 𝑧 𝑋)
71 simplr 765 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → 𝑄 𝑋)
72 simpll3 1206 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → 𝑄𝐴)
7372, 38syl 17 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → 𝑄 ∈ (Base‘𝐾))
74 simpll2 1205 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → 𝑋𝑃)
7574, 5syl 17 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → 𝑋 ∈ (Base‘𝐾))
763, 7, 8latjle12 17660 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑧 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾))) → ((𝑧 𝑋𝑄 𝑋) ↔ (𝑧 𝑄) 𝑋))
7762, 64, 73, 75, 76syl13anc 1364 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → ((𝑧 𝑋𝑄 𝑋) ↔ (𝑧 𝑄) 𝑋))
7870, 71, 77mpbi2and 708 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → (𝑧 𝑄) 𝑋)
793, 8latjcl 17649 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ 𝑧 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → (𝑧 𝑄) ∈ (Base‘𝐾))
8062, 64, 73, 79syl3anc 1363 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → (𝑧 𝑄) ∈ (Base‘𝐾))
81 eqid 2818 . . . . . . . . . . . . 13 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
823, 7, 8, 81, 9cvr1 36426 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾) ∧ 𝑄𝐴) → (¬ 𝑄 𝑧𝑧( ⋖ ‘𝐾)(𝑧 𝑄)))
8361, 64, 72, 82syl3anc 1363 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → (¬ 𝑄 𝑧𝑧( ⋖ ‘𝐾)(𝑧 𝑄)))
8460, 83mpbid 233 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → 𝑧( ⋖ ‘𝐾)(𝑧 𝑄))
853, 81, 10, 4lplni 36548 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑧 𝑄) ∈ (Base‘𝐾) ∧ 𝑧𝑁) ∧ 𝑧( ⋖ ‘𝐾)(𝑧 𝑄)) → (𝑧 𝑄) ∈ 𝑃)
8661, 80, 59, 84, 85syl31anc 1365 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → (𝑧 𝑄) ∈ 𝑃)
877, 4lplncmp 36578 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑧 𝑄) ∈ 𝑃𝑋𝑃) → ((𝑧 𝑄) 𝑋 ↔ (𝑧 𝑄) = 𝑋))
8861, 86, 74, 87syl3anc 1363 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → ((𝑧 𝑄) 𝑋 ↔ (𝑧 𝑄) = 𝑋))
8978, 88mpbid 233 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → (𝑧 𝑄) = 𝑋)
9089eqcomd 2824 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → 𝑋 = (𝑧 𝑄))
91 breq2 5061 . . . . . . . . 9 (𝑦 = 𝑧 → (𝑄 𝑦𝑄 𝑧))
9291notbid 319 . . . . . . . 8 (𝑦 = 𝑧 → (¬ 𝑄 𝑦 ↔ ¬ 𝑄 𝑧))
93 oveq1 7152 . . . . . . . . 9 (𝑦 = 𝑧 → (𝑦 𝑄) = (𝑧 𝑄))
9493eqeq2d 2829 . . . . . . . 8 (𝑦 = 𝑧 → (𝑋 = (𝑦 𝑄) ↔ 𝑋 = (𝑧 𝑄)))
9592, 94anbi12d 630 . . . . . . 7 (𝑦 = 𝑧 → ((¬ 𝑄 𝑦𝑋 = (𝑦 𝑄)) ↔ (¬ 𝑄 𝑧𝑋 = (𝑧 𝑄))))
9695rspcev 3620 . . . . . 6 ((𝑧𝑁 ∧ (¬ 𝑄 𝑧𝑋 = (𝑧 𝑄))) → ∃𝑦𝑁𝑄 𝑦𝑋 = (𝑦 𝑄)))
9759, 60, 90, 96syl12anc 832 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) ∧ (¬ 𝑄 𝑧 ∧ (𝑧𝑁𝑟𝐴) ∧ (¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)))) → ∃𝑦𝑁𝑄 𝑦𝑋 = (𝑦 𝑄)))
98973exp2 1346 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) → (¬ 𝑄 𝑧 → ((𝑧𝑁𝑟𝐴) → ((¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)) → ∃𝑦𝑁𝑄 𝑦𝑋 = (𝑦 𝑄))))))
9958, 98pm2.61d 180 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) → ((𝑧𝑁𝑟𝐴) → ((¬ 𝑟 𝑧𝑋 = (𝑧 𝑟)) → ∃𝑦𝑁𝑄 𝑦𝑋 = (𝑦 𝑄)))))
10099rexlimdvv 3290 . 2 (((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) → (∃𝑧𝑁𝑟𝐴𝑟 𝑧𝑋 = (𝑧 𝑟)) → ∃𝑦𝑁𝑄 𝑦𝑋 = (𝑦 𝑄))))
10113, 100mpd 15 1 (((𝐾 ∈ HL ∧ 𝑋𝑃𝑄𝐴) ∧ 𝑄 𝑋) → ∃𝑦𝑁𝑄 𝑦𝑋 = (𝑦 𝑄)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wcel 2105  wne 3013  wrex 3136   class class class wbr 5057  cfv 6348  (class class class)co 7145  Basecbs 16471  lecple 16560  joincjn 17542  Latclat 17643  ccvr 36278  Atomscatm 36279  HLchlt 36366  LLinesclln 36507  LPlanesclpl 36508
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-proset 17526  df-poset 17544  df-plt 17556  df-lub 17572  df-glb 17573  df-join 17574  df-meet 17575  df-p0 17637  df-lat 17644  df-clat 17706  df-oposet 36192  df-ol 36194  df-oml 36195  df-covers 36282  df-ats 36283  df-atl 36314  df-cvlat 36338  df-hlat 36367  df-llines 36514  df-lplanes 36515
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator