Metamath Proof Explorer

Theorem colperpex

Description: In dimension 2 and above, on a line ( A L B ) there is always a perpendicular P from A on a given plane (here given by C , in case C does not lie on the line). Theorem 8.21 of Schwabhauser p. 63. (Contributed by Thierry Arnoux, 20-Nov-2019)

Ref Expression
Hypotheses colperpex.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
colperpex.d ⊢ − = ( dist ‘ 𝐺 )
colperpex.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
colperpex.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
colperpex.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
colperpex.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
colperpex.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
colperpex.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
colperpex.4 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
colperpex.5 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
Assertion colperpex ( 𝜑 → ∃ 𝑝 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) )

Proof

Step Hyp Ref Expression
1 colperpex.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 colperpex.d ⊢ − = ( dist ‘ 𝐺 )
3 colperpex.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 colperpex.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 colperpex.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 colperpex.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 colperpex.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 colperpex.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9 colperpex.4 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
10 colperpex.5 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
11 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝐺 ∈ TarskiG )
12 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝐴 ∈ 𝑃 )
13 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝐵 ∈ 𝑃 )
14 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝑑 ∈ 𝑃 )
15 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝐴 ≠ 𝐵 )
16 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) ) → ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) )
17 1 2 3 4 11 12 13 14 15 16 colperpexlem3 ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) ) → ∃ 𝑝 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑠 ∈ 𝑃 ( ( 𝑠 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑠 ∈ ( 𝑑 𝐼 𝑝 ) ) ) )
18 simprl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑠 ∈ 𝑃 ( ( 𝑠 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑠 ∈ ( 𝑑 𝐼 𝑝 ) ) ) ) → ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
19 8 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑠 ∈ 𝑃 ( ( 𝑠 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑠 ∈ ( 𝑑 𝐼 𝑝 ) ) ) ) → 𝐶 ∈ 𝑃 )
20 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑠 ∈ 𝑃 ( ( 𝑠 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑠 ∈ ( 𝑑 𝐼 𝑝 ) ) ) ) → 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) )
21 20 orcd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑠 ∈ 𝑃 ( ( 𝑠 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑠 ∈ ( 𝑑 𝐼 𝑝 ) ) ) ) → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
22 5 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑠 ∈ 𝑃 ( ( 𝑠 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑠 ∈ ( 𝑑 𝐼 𝑝 ) ) ) ) → 𝐺 ∈ TarskiG )
23 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑠 ∈ 𝑃 ( ( 𝑠 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑠 ∈ ( 𝑑 𝐼 𝑝 ) ) ) ) → 𝑝 ∈ 𝑃 )
24 1 2 3 22 19 23 tgbtwntriv1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑠 ∈ 𝑃 ( ( 𝑠 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑠 ∈ ( 𝑑 𝐼 𝑝 ) ) ) ) → 𝐶 ∈ ( 𝐶 𝐼 𝑝 ) )
25 eleq1 ⊢ ( 𝑡 = 𝐶 → ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ↔ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) )
26 25 orbi1d ⊢ ( 𝑡 = 𝐶 → ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ↔ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) )
27 eleq1 ⊢ ( 𝑡 = 𝐶 → ( 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ↔ 𝐶 ∈ ( 𝐶 𝐼 𝑝 ) ) )
28 26 27 anbi12d ⊢ ( 𝑡 = 𝐶 → ( ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ↔ ( ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝐶 ∈ ( 𝐶 𝐼 𝑝 ) ) ) )
29 28 rspcev ⊢ ( ( 𝐶 ∈ 𝑃 ∧ ( ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝐶 ∈ ( 𝐶 𝐼 𝑝 ) ) ) → ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) )
30 19 21 24 29 syl12anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑠 ∈ 𝑃 ( ( 𝑠 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑠 ∈ ( 𝑑 𝐼 𝑝 ) ) ) ) → ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) )
31 18 30 jca ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑠 ∈ 𝑃 ( ( 𝑠 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑠 ∈ ( 𝑑 𝐼 𝑝 ) ) ) ) → ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) )
32 31 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑠 ∈ 𝑃 ( ( 𝑠 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑠 ∈ ( 𝑑 𝐼 𝑝 ) ) ) → ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) )
33 32 reximdva ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) ) → ( ∃ 𝑝 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑠 ∈ 𝑃 ( ( 𝑠 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑠 ∈ ( 𝑑 𝐼 𝑝 ) ) ) → ∃ 𝑝 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) )
34 17 33 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) ) → ∃ 𝑝 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) )
35 5 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝐺 ∈ TarskiG )
36 10 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝐺 DimTarskiG≥ 2 )
37 6 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝐴 ∈ 𝑃 )
38 7 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝐵 ∈ 𝑃 )
39 9 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝐴 ≠ 𝐵 )
40 1 3 4 35 36 37 38 39 tglowdim2ln ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) → ∃ 𝑑 ∈ 𝑃 ¬ 𝑑 ∈ ( 𝐴 𝐿 𝐵 ) )
41 34 40 r19.29a ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) → ∃ 𝑝 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) )
42 5 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝐺 ∈ TarskiG )
43 6 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝐴 ∈ 𝑃 )
44 7 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝐵 ∈ 𝑃 )
45 8 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝐶 ∈ 𝑃 )
46 9 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝐴 ≠ 𝐵 )
47 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) → ¬ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) )
48 1 2 3 4 42 43 44 45 46 47 colperpexlem3 ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) → ∃ 𝑝 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) )
49 41 48 pm2.61dan ⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) )