Metamath Proof Explorer


Theorem 3dim1

Description: Construct a 3-dimensional volume (height-4 element) on top of a given atom P . (Contributed by NM, 25-Jul-2012)

Ref Expression
Hypotheses 3dim0.j = ( join ‘ 𝐾 )
3dim0.l = ( le ‘ 𝐾 )
3dim0.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 3dim1 ( ( 𝐾 ∈ HL ∧ 𝑃𝐴 ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) )

Proof

Step Hyp Ref Expression
1 3dim0.j = ( join ‘ 𝐾 )
2 3dim0.l = ( le ‘ 𝐾 )
3 3dim0.a 𝐴 = ( Atoms ‘ 𝐾 )
4 1 2 3 3dim0 ( 𝐾 ∈ HL → ∃ 𝑡𝐴𝑢𝐴𝑣𝐴𝑤𝐴 ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) )
5 4 adantr ( ( 𝐾 ∈ HL ∧ 𝑃𝐴 ) → ∃ 𝑡𝐴𝑢𝐴𝑣𝐴𝑤𝐴 ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) )
6 simpl2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ 𝑃 = 𝑡 ) → ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) )
7 1 2 3 3dimlem1 ( ( ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ∧ 𝑃 = 𝑡 ) → ( 𝑃𝑢 ∧ ¬ 𝑣 ( 𝑃 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑃 𝑢 ) 𝑣 ) ) )
8 7 3ad2antl3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ 𝑃 = 𝑡 ) → ( 𝑃𝑢 ∧ ¬ 𝑣 ( 𝑃 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑃 𝑢 ) 𝑣 ) ) )
9 1 2 3 3dim1lem5 ( ( ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑃𝑢 ∧ ¬ 𝑣 ( 𝑃 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑃 𝑢 ) 𝑣 ) ) ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) )
10 6 8 9 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ 𝑃 = 𝑡 ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) )
11 simp13 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) → 𝑡𝐴 )
12 simp22 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) → 𝑣𝐴 )
13 simp23 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) → 𝑤𝐴 )
14 11 12 13 3jca ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) → ( 𝑡𝐴𝑣𝐴𝑤𝐴 ) )
15 14 ad2antrr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ 𝑃𝑡 ) ∧ 𝑃 ( 𝑡 𝑢 ) ) → ( 𝑡𝐴𝑣𝐴𝑤𝐴 ) )
16 simpll1 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ 𝑃𝑡 ) ∧ 𝑃 ( 𝑡 𝑢 ) ) → ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) )
17 simp21 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) → 𝑢𝐴 )
18 simp32 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) → ¬ 𝑣 ( 𝑡 𝑢 ) )
19 simp33 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) → ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) )
20 17 18 19 3jca ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) → ( 𝑢𝐴 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) )
21 20 ad2antrr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ 𝑃𝑡 ) ∧ 𝑃 ( 𝑡 𝑢 ) ) → ( 𝑢𝐴 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) )
22 simplr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ 𝑃𝑡 ) ∧ 𝑃 ( 𝑡 𝑢 ) ) → 𝑃𝑡 )
23 simpr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ 𝑃𝑡 ) ∧ 𝑃 ( 𝑡 𝑢 ) ) → 𝑃 ( 𝑡 𝑢 ) )
24 1 2 3 3dimlem2 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ∧ ( 𝑃𝑡𝑃 ( 𝑡 𝑢 ) ) ) → ( 𝑃𝑡 ∧ ¬ 𝑣 ( 𝑃 𝑡 ) ∧ ¬ 𝑤 ( ( 𝑃 𝑡 ) 𝑣 ) ) )
25 16 21 22 23 24 syl112anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ 𝑃𝑡 ) ∧ 𝑃 ( 𝑡 𝑢 ) ) → ( 𝑃𝑡 ∧ ¬ 𝑣 ( 𝑃 𝑡 ) ∧ ¬ 𝑤 ( ( 𝑃 𝑡 ) 𝑣 ) ) )
26 1 2 3 3dim1lem5 ( ( ( 𝑡𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑣 ( 𝑃 𝑡 ) ∧ ¬ 𝑤 ( ( 𝑃 𝑡 ) 𝑣 ) ) ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) )
27 15 25 26 syl2anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ 𝑃𝑡 ) ∧ 𝑃 ( 𝑡 𝑢 ) ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) )
28 11 17 13 3jca ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) → ( 𝑡𝐴𝑢𝐴𝑤𝐴 ) )
29 28 ad2antrr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) ∧ 𝑃 ( ( 𝑡 𝑢 ) 𝑣 ) ) → ( 𝑡𝐴𝑢𝐴𝑤𝐴 ) )
30 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) )
31 17 12 jca ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) → ( 𝑢𝐴𝑣𝐴 ) )
32 simp31 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) → 𝑡𝑢 )
33 32 19 jca ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) → ( 𝑡𝑢 ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) )
34 30 31 33 3jca ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) )
35 34 ad2antrr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) ∧ 𝑃 ( ( 𝑡 𝑢 ) 𝑣 ) ) → ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) )
36 simplrl ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) ∧ 𝑃 ( ( 𝑡 𝑢 ) 𝑣 ) ) → 𝑃𝑡 )
37 simplrr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) ∧ 𝑃 ( ( 𝑡 𝑢 ) 𝑣 ) ) → ¬ 𝑃 ( 𝑡 𝑢 ) )
38 simpr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) ∧ 𝑃 ( ( 𝑡 𝑢 ) 𝑣 ) ) → 𝑃 ( ( 𝑡 𝑢 ) 𝑣 ) )
39 1 2 3 3dimlem3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ∧ 𝑃 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) → ( 𝑃𝑡 ∧ ¬ 𝑢 ( 𝑃 𝑡 ) ∧ ¬ 𝑤 ( ( 𝑃 𝑡 ) 𝑢 ) ) )
40 35 36 37 38 39 syl13anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) ∧ 𝑃 ( ( 𝑡 𝑢 ) 𝑣 ) ) → ( 𝑃𝑡 ∧ ¬ 𝑢 ( 𝑃 𝑡 ) ∧ ¬ 𝑤 ( ( 𝑃 𝑡 ) 𝑢 ) ) )
41 1 2 3 3dim1lem5 ( ( ( 𝑡𝐴𝑢𝐴𝑤𝐴 ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑢 ( 𝑃 𝑡 ) ∧ ¬ 𝑤 ( ( 𝑃 𝑡 ) 𝑢 ) ) ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) )
42 29 40 41 syl2anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) ∧ 𝑃 ( ( 𝑡 𝑢 ) 𝑣 ) ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) )
43 11 17 12 3jca ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) → ( 𝑡𝐴𝑢𝐴𝑣𝐴 ) )
44 43 ad2antrr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) ∧ ¬ 𝑃 ( ( 𝑡 𝑢 ) 𝑣 ) ) → ( 𝑡𝐴𝑢𝐴𝑣𝐴 ) )
45 simpl1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) )
46 simpl21 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) → 𝑢𝐴 )
47 simpl22 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) → 𝑣𝐴 )
48 46 47 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) → ( 𝑢𝐴𝑣𝐴 ) )
49 simpl31 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) → 𝑡𝑢 )
50 simpl32 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) → ¬ 𝑣 ( 𝑡 𝑢 ) )
51 49 50 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) → ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ) )
52 45 48 51 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ) ) )
53 52 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) ∧ ¬ 𝑃 ( ( 𝑡 𝑢 ) 𝑣 ) ) → ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ) ) )
54 simplr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) ∧ ¬ 𝑃 ( ( 𝑡 𝑢 ) 𝑣 ) ) → ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) )
55 simpr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) ∧ ¬ 𝑃 ( ( 𝑡 𝑢 ) 𝑣 ) ) → ¬ 𝑃 ( ( 𝑡 𝑢 ) 𝑣 ) )
56 1 2 3 3dimlem4 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ∧ ¬ 𝑃 ( ( 𝑡 𝑢 ) 𝑣 ) ) → ( 𝑃𝑡 ∧ ¬ 𝑢 ( 𝑃 𝑡 ) ∧ ¬ 𝑣 ( ( 𝑃 𝑡 ) 𝑢 ) ) )
57 53 54 55 56 syl3anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) ∧ ¬ 𝑃 ( ( 𝑡 𝑢 ) 𝑣 ) ) → ( 𝑃𝑡 ∧ ¬ 𝑢 ( 𝑃 𝑡 ) ∧ ¬ 𝑣 ( ( 𝑃 𝑡 ) 𝑢 ) ) )
58 1 2 3 3dim1lem5 ( ( ( 𝑡𝐴𝑢𝐴𝑣𝐴 ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑢 ( 𝑃 𝑡 ) ∧ ¬ 𝑣 ( ( 𝑃 𝑡 ) 𝑢 ) ) ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) )
59 44 57 58 syl2anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) ∧ ¬ 𝑃 ( ( 𝑡 𝑢 ) 𝑣 ) ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) )
60 42 59 pm2.61dan ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ ( 𝑃𝑡 ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) )
61 60 anassrs ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ 𝑃𝑡 ) ∧ ¬ 𝑃 ( 𝑡 𝑢 ) ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) )
62 27 61 pm2.61dan ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) ∧ 𝑃𝑡 ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) )
63 10 62 pm2.61dane ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) ∧ ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) ∧ ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) )
64 63 3exp ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) → ( ( 𝑢𝐴𝑣𝐴𝑤𝐴 ) → ( ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) ) ) )
65 64 3expd ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑡𝐴 ) → ( 𝑢𝐴 → ( 𝑣𝐴 → ( 𝑤𝐴 → ( ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) ) ) ) ) )
66 65 3exp ( 𝐾 ∈ HL → ( 𝑃𝐴 → ( 𝑡𝐴 → ( 𝑢𝐴 → ( 𝑣𝐴 → ( 𝑤𝐴 → ( ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) ) ) ) ) ) ) )
67 66 imp43 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴 ) ∧ ( 𝑡𝐴𝑢𝐴 ) ) → ( 𝑣𝐴 → ( 𝑤𝐴 → ( ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) ) ) ) )
68 67 impd ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴 ) ∧ ( 𝑡𝐴𝑢𝐴 ) ) → ( ( 𝑣𝐴𝑤𝐴 ) → ( ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) ) ) )
69 68 rexlimdvv ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴 ) ∧ ( 𝑡𝐴𝑢𝐴 ) ) → ( ∃ 𝑣𝐴𝑤𝐴 ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) ) )
70 69 rexlimdvva ( ( 𝐾 ∈ HL ∧ 𝑃𝐴 ) → ( ∃ 𝑡𝐴𝑢𝐴𝑣𝐴𝑤𝐴 ( 𝑡𝑢 ∧ ¬ 𝑣 ( 𝑡 𝑢 ) ∧ ¬ 𝑤 ( ( 𝑡 𝑢 ) 𝑣 ) ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) ) )
71 5 70 mpd ( ( 𝐾 ∈ HL ∧ 𝑃𝐴 ) → ∃ 𝑞𝐴𝑟𝐴𝑠𝐴 ( 𝑃𝑞 ∧ ¬ 𝑟 ( 𝑃 𝑞 ) ∧ ¬ 𝑠 ( ( 𝑃 𝑞 ) 𝑟 ) ) )