Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  colperp Structured version   Unicode version

Theorem colperp 23245
 Description: In dimension 2 and above, on a line there is always a perpendicular from on a given plane (here given by , in case does not lie on the line). Theorem 8.21 of [Schwabhauser] p. 63. (Contributed by Thierry Arnoux, 20-Nov-2019.)
Hypotheses
Ref Expression
colperp.p
colperp.d
colperp.i Itv
colperp.l LineG
colperp.g TarskiG
colperp.1
colperp.2
colperp.3
colperp.4
colperp.5 DimTarskiG
Assertion
Ref Expression
colperp ⟂G
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,,   ,,   ,,   ,,

Proof of Theorem colperp
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 colperp.p . . . . 5
2 colperp.d . . . . 5
3 colperp.i . . . . 5 Itv
4 colperp.l . . . . 5 LineG
5 colperp.g . . . . . 6 TarskiG
65ad3antrrr 729 . . . . 5 TarskiG
7 colperp.1 . . . . . 6
87ad3antrrr 729 . . . . 5
9 colperp.2 . . . . . 6
109ad3antrrr 729 . . . . 5
11 simplr 754 . . . . 5
12 colperp.4 . . . . . 6
1312ad3antrrr 729 . . . . 5
14 simpr 461 . . . . 5
151, 2, 3, 4, 6, 8, 10, 11, 13, 14colperplem3 23244 . . . 4 ⟂G
16 simprl 755 . . . . . . 7 ⟂G ⟂G
17 colperp.3 . . . . . . . . 9
1817ad5antr 733 . . . . . . . 8 ⟂G
19 simp-5r 768 . . . . . . . . 9 ⟂G
2019orcd 392 . . . . . . . 8 ⟂G
216ad2antrr 725 . . . . . . . . 9 ⟂G TarskiG
22 simplr 754 . . . . . . . . 9 ⟂G
231, 2, 3, 21, 18, 22tgbtwntriv1 23064 . . . . . . . 8 ⟂G
24 eleq1 2523 . . . . . . . . . . 11
2524orbi1d 702 . . . . . . . . . 10
26 eleq1 2523 . . . . . . . . . 10
2725, 26anbi12d 710 . . . . . . . . 9
2827rspcev 3171 . . . . . . . 8
2918, 20, 23, 28syl12anc 1217 . . . . . . 7 ⟂G
3016, 29jca 532 . . . . . 6 ⟂G ⟂G
3130ex 434 . . . . 5 ⟂G ⟂G
3231reximdva 2926 . . . 4 ⟂G ⟂G
3315, 32mpd 15 . . 3 ⟂G
345adantr 465 . . . 4 TarskiG
35 colperp.5 . . . . 5 DimTarskiG
3635adantr 465 . . . 4 DimTarskiG
377adantr 465 . . . 4
389adantr 465 . . . 4
3912adantr 465 . . . 4
401, 3, 4, 34, 36, 37, 38, 39tglowdim2ln 23181 . . 3
4133, 40r19.29a 2960 . 2 ⟂G
425adantr 465 . . 3 TarskiG