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

Theorem 3dim1 33565
Description: Construct a 3-dimensional volume (height-4 element) on top of a given atom 𝑃. (Contributed by NM, 25-Jul-2012.)
Hypotheses
Ref Expression
3dim0.j = (join‘𝐾)
3dim0.l = (le‘𝐾)
3dim0.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
3dim1 ((𝐾 ∈ HL ∧ 𝑃𝐴) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)))
Distinct variable groups:   𝑟,𝑞,𝑠,𝐴   ,𝑟,𝑠,𝑞   ,𝑞,𝑟,𝑠   𝑃,𝑞,𝑟,𝑠
Allowed substitution hints:   𝐾(𝑠,𝑟,𝑞)

Proof of Theorem 3dim1
Dummy variables 𝑢 𝑡 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 3dim0.j . . . 4 = (join‘𝐾)
2 3dim0.l . . . 4 = (le‘𝐾)
3 3dim0.a . . . 4 𝐴 = (Atoms‘𝐾)
41, 2, 33dim0 33555 . . 3 (𝐾 ∈ HL → ∃𝑡𝐴𝑢𝐴𝑣𝐴𝑤𝐴 (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣)))
54adantr 480 . 2 ((𝐾 ∈ HL ∧ 𝑃𝐴) → ∃𝑡𝐴𝑢𝐴𝑣𝐴𝑤𝐴 (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣)))
6 simpl2 1058 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ 𝑃 = 𝑡) → (𝑢𝐴𝑣𝐴𝑤𝐴))
71, 2, 33dimlem1 33556 . . . . . . . . . . . 12 (((𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣)) ∧ 𝑃 = 𝑡) → (𝑃𝑢 ∧ ¬ 𝑣 (𝑃 𝑢) ∧ ¬ 𝑤 ((𝑃 𝑢) 𝑣)))
873ad2antl3 1218 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ 𝑃 = 𝑡) → (𝑃𝑢 ∧ ¬ 𝑣 (𝑃 𝑢) ∧ ¬ 𝑤 ((𝑃 𝑢) 𝑣)))
91, 2, 33dim1lem5 33564 . . . . . . . . . . 11 (((𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑃𝑢 ∧ ¬ 𝑣 (𝑃 𝑢) ∧ ¬ 𝑤 ((𝑃 𝑢) 𝑣))) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)))
106, 8, 9syl2anc 691 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ 𝑃 = 𝑡) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)))
11 simp13 1086 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) → 𝑡𝐴)
12 simp22 1088 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) → 𝑣𝐴)
13 simp23 1089 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) → 𝑤𝐴)
1411, 12, 133jca 1235 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) → (𝑡𝐴𝑣𝐴𝑤𝐴))
1514ad2antrr 758 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ 𝑃𝑡) ∧ 𝑃 (𝑡 𝑢)) → (𝑡𝐴𝑣𝐴𝑤𝐴))
16 simpll1 1093 . . . . . . . . . . . . 13 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ 𝑃𝑡) ∧ 𝑃 (𝑡 𝑢)) → (𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴))
17 simp21 1087 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) → 𝑢𝐴)
18 simp32 1091 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) → ¬ 𝑣 (𝑡 𝑢))
19 simp33 1092 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) → ¬ 𝑤 ((𝑡 𝑢) 𝑣))
2017, 18, 193jca 1235 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) → (𝑢𝐴 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣)))
2120ad2antrr 758 . . . . . . . . . . . . 13 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ 𝑃𝑡) ∧ 𝑃 (𝑡 𝑢)) → (𝑢𝐴 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣)))
22 simplr 788 . . . . . . . . . . . . 13 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ 𝑃𝑡) ∧ 𝑃 (𝑡 𝑢)) → 𝑃𝑡)
23 simpr 476 . . . . . . . . . . . . 13 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ 𝑃𝑡) ∧ 𝑃 (𝑡 𝑢)) → 𝑃 (𝑡 𝑢))
241, 2, 33dimlem2 33557 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣)) ∧ (𝑃𝑡𝑃 (𝑡 𝑢))) → (𝑃𝑡 ∧ ¬ 𝑣 (𝑃 𝑡) ∧ ¬ 𝑤 ((𝑃 𝑡) 𝑣)))
2516, 21, 22, 23, 24syl112anc 1322 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ 𝑃𝑡) ∧ 𝑃 (𝑡 𝑢)) → (𝑃𝑡 ∧ ¬ 𝑣 (𝑃 𝑡) ∧ ¬ 𝑤 ((𝑃 𝑡) 𝑣)))
261, 2, 33dim1lem5 33564 . . . . . . . . . . . 12 (((𝑡𝐴𝑣𝐴𝑤𝐴) ∧ (𝑃𝑡 ∧ ¬ 𝑣 (𝑃 𝑡) ∧ ¬ 𝑤 ((𝑃 𝑡) 𝑣))) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)))
2715, 25, 26syl2anc 691 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ 𝑃𝑡) ∧ 𝑃 (𝑡 𝑢)) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)))
2811, 17, 133jca 1235 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) → (𝑡𝐴𝑢𝐴𝑤𝐴))
2928ad2antrr 758 . . . . . . . . . . . . . 14 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) ∧ 𝑃 ((𝑡 𝑢) 𝑣)) → (𝑡𝐴𝑢𝐴𝑤𝐴))
30 simp1 1054 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) → (𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴))
3117, 12jca 553 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) → (𝑢𝐴𝑣𝐴))
32 simp31 1090 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) → 𝑡𝑢)
3332, 19jca 553 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) → (𝑡𝑢 ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣)))
3430, 31, 333jca 1235 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) → ((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))))
3534ad2antrr 758 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) ∧ 𝑃 ((𝑡 𝑢) 𝑣)) → ((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))))
36 simplrl 796 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) ∧ 𝑃 ((𝑡 𝑢) 𝑣)) → 𝑃𝑡)
37 simplrr 797 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) ∧ 𝑃 ((𝑡 𝑢) 𝑣)) → ¬ 𝑃 (𝑡 𝑢))
38 simpr 476 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) ∧ 𝑃 ((𝑡 𝑢) 𝑣)) → 𝑃 ((𝑡 𝑢) 𝑣))
391, 2, 33dimlem3 33559 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢) ∧ 𝑃 ((𝑡 𝑢) 𝑣))) → (𝑃𝑡 ∧ ¬ 𝑢 (𝑃 𝑡) ∧ ¬ 𝑤 ((𝑃 𝑡) 𝑢)))
4035, 36, 37, 38, 39syl13anc 1320 . . . . . . . . . . . . . 14 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) ∧ 𝑃 ((𝑡 𝑢) 𝑣)) → (𝑃𝑡 ∧ ¬ 𝑢 (𝑃 𝑡) ∧ ¬ 𝑤 ((𝑃 𝑡) 𝑢)))
411, 2, 33dim1lem5 33564 . . . . . . . . . . . . . 14 (((𝑡𝐴𝑢𝐴𝑤𝐴) ∧ (𝑃𝑡 ∧ ¬ 𝑢 (𝑃 𝑡) ∧ ¬ 𝑤 ((𝑃 𝑡) 𝑢))) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)))
4229, 40, 41syl2anc 691 . . . . . . . . . . . . 13 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) ∧ 𝑃 ((𝑡 𝑢) 𝑣)) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)))
4311, 17, 123jca 1235 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) → (𝑡𝐴𝑢𝐴𝑣𝐴))
4443ad2antrr 758 . . . . . . . . . . . . . 14 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) ∧ ¬ 𝑃 ((𝑡 𝑢) 𝑣)) → (𝑡𝐴𝑢𝐴𝑣𝐴))
45 simpl1 1057 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) → (𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴))
46 simpl21 1132 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) → 𝑢𝐴)
47 simpl22 1133 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) → 𝑣𝐴)
4846, 47jca 553 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) → (𝑢𝐴𝑣𝐴))
49 simpl31 1135 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) → 𝑡𝑢)
50 simpl32 1136 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) → ¬ 𝑣 (𝑡 𝑢))
5149, 50jca 553 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) → (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢)))
5245, 48, 513jca 1235 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) → ((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢))))
5352adantr 480 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) ∧ ¬ 𝑃 ((𝑡 𝑢) 𝑣)) → ((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢))))
54 simplr 788 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) ∧ ¬ 𝑃 ((𝑡 𝑢) 𝑣)) → (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢)))
55 simpr 476 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) ∧ ¬ 𝑃 ((𝑡 𝑢) 𝑣)) → ¬ 𝑃 ((𝑡 𝑢) 𝑣))
561, 2, 33dimlem4 33562 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢)) ∧ ¬ 𝑃 ((𝑡 𝑢) 𝑣)) → (𝑃𝑡 ∧ ¬ 𝑢 (𝑃 𝑡) ∧ ¬ 𝑣 ((𝑃 𝑡) 𝑢)))
5753, 54, 55, 56syl3anc 1318 . . . . . . . . . . . . . 14 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) ∧ ¬ 𝑃 ((𝑡 𝑢) 𝑣)) → (𝑃𝑡 ∧ ¬ 𝑢 (𝑃 𝑡) ∧ ¬ 𝑣 ((𝑃 𝑡) 𝑢)))
581, 2, 33dim1lem5 33564 . . . . . . . . . . . . . 14 (((𝑡𝐴𝑢𝐴𝑣𝐴) ∧ (𝑃𝑡 ∧ ¬ 𝑢 (𝑃 𝑡) ∧ ¬ 𝑣 ((𝑃 𝑡) 𝑢))) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)))
5944, 57, 58syl2anc 691 . . . . . . . . . . . . 13 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) ∧ ¬ 𝑃 ((𝑡 𝑢) 𝑣)) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)))
6042, 59pm2.61dan 828 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ (𝑃𝑡 ∧ ¬ 𝑃 (𝑡 𝑢))) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)))
6160anassrs 678 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ 𝑃𝑡) ∧ ¬ 𝑃 (𝑡 𝑢)) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)))
6227, 61pm2.61dan 828 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) ∧ 𝑃𝑡) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)))
6310, 62pm2.61dane 2869 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) ∧ (𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣))) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)))
64633exp 1256 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) → ((𝑢𝐴𝑣𝐴𝑤𝐴) → ((𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣)) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)))))
65643expd 1276 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴) → (𝑢𝐴 → (𝑣𝐴 → (𝑤𝐴 → ((𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣)) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)))))))
66653exp 1256 . . . . . 6 (𝐾 ∈ HL → (𝑃𝐴 → (𝑡𝐴 → (𝑢𝐴 → (𝑣𝐴 → (𝑤𝐴 → ((𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣)) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)))))))))
6766imp43 619 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑡𝐴𝑢𝐴)) → (𝑣𝐴 → (𝑤𝐴 → ((𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣)) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟))))))
6867impd 446 . . . 4 (((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑡𝐴𝑢𝐴)) → ((𝑣𝐴𝑤𝐴) → ((𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣)) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)))))
6968rexlimdvv 3019 . . 3 (((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑡𝐴𝑢𝐴)) → (∃𝑣𝐴𝑤𝐴 (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣)) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟))))
7069rexlimdvva 3020 . 2 ((𝐾 ∈ HL ∧ 𝑃𝐴) → (∃𝑡𝐴𝑢𝐴𝑣𝐴𝑤𝐴 (𝑡𝑢 ∧ ¬ 𝑣 (𝑡 𝑢) ∧ ¬ 𝑤 ((𝑡 𝑢) 𝑣)) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟))))
715, 70mpd 15 1 ((𝐾 ∈ HL ∧ 𝑃𝐴) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383  w3a 1031   = wceq 1475  wcel 1977  wne 2780  wrex 2897   class class class wbr 4578  cfv 5790  (class class class)co 6527  lecple 15724  joincjn 16716  Atomscatm 33362  HLchlt 33449
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4694  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4368  df-iun 4452  df-br 4579  df-opab 4639  df-mpt 4640  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-preset 16700  df-poset 16718  df-plt 16730  df-lub 16746  df-glb 16747  df-join 16748  df-meet 16749  df-p0 16811  df-p1 16812  df-lat 16818  df-clat 16880  df-oposet 33275  df-ol 33277  df-oml 33278  df-covers 33365  df-ats 33366  df-atl 33397  df-cvlat 33421  df-hlat 33450
This theorem is referenced by:  3dim2  33566  2dim  33568
  Copyright terms: Public domain W3C validator