Metamath Proof Explorer

Theorem prlngex

Description: There exists at least one parallel line b to a given line A through a given point X . Theorem 12.10 of Schwabhauser p. 122. (Contributed by Thierry Arnoux, 5-Jul-2026)

Ref Expression
Hypotheses prlngeu.p 
|- P = ( Base ` G )
prlngeu.l 
|- L = ( LineG ` G )
prlngeu.r 
|- .|| = ( parlnG ` G )
prlngeu.g 
|- ( ph -> G e. TarskiG )
prlngeu.a 
|- ( ph -> A e. ran L )
prlngex.6 
|- ( ph -> X e. P )
Assertion prlngex 
|- ( ph -> E. b e. ran L ( A .|| b /\ X e. b ) )

Proof

Step Hyp Ref Expression
1 prlngeu.p 
 |-  P = ( Base ` G )
2 prlngeu.l 
 |-  L = ( LineG ` G )
3 prlngeu.r 
 |-  .|| = ( parlnG ` G )
4 prlngeu.g 
 |-  ( ph -> G e. TarskiG )
5 prlngeu.a 
 |-  ( ph -> A e. ran L )
6 prlngex.6 
 |-  ( ph -> X e. P )
7 breq2 
 |-  ( b = A -> ( A .|| b <-> A .|| A ) )
8 eleq2 
 |-  ( b = A -> ( X e. b <-> X e. A ) )
9 7 8 anbi12d 
 |-  ( b = A -> ( ( A .|| b /\ X e. b ) <-> ( A .|| A /\ X e. A ) ) )
10 5 adantr 
 |-  ( ( ph /\ X e. A ) -> A e. ran L )
11 eqid 
 |-  ( PlnG ` G ) = ( PlnG ` G )
12 4 adantr 
 |-  ( ( ph /\ X e. A ) -> G e. TarskiG )
13 2 11 3 12 10 prlngref 
 |-  ( ( ph /\ X e. A ) -> A .|| A )
14 simpr 
 |-  ( ( ph /\ X e. A ) -> X e. A )
15 13 14 jca 
 |-  ( ( ph /\ X e. A ) -> ( A .|| A /\ X e. A ) )
16 9 10 15 rspcedvdw 
 |-  ( ( ph /\ X e. A ) -> E. b e. ran L ( A .|| b /\ X e. b ) )
17 breq2 
 |-  ( b = ( w L X ) -> ( A .|| b <-> A .|| ( w L X ) ) )
18 eleq2 
 |-  ( b = ( w L X ) -> ( X e. b <-> X e. ( w L X ) ) )
19 17 18 anbi12d 
 |-  ( b = ( w L X ) -> ( ( A .|| b /\ X e. b ) <-> ( A .|| ( w L X ) /\ X e. ( w L X ) ) ) )
20 4 adantr 
 |-  ( ( ph /\ -. X e. A ) -> G e. TarskiG )
21 20 ad2antrr 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) -> G e. TarskiG )
22 21 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) -> G e. TarskiG )
23 22 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> G e. TarskiG )
24 simplr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( X L y ) ( perpG ` G ) ( w L X ) )
25 2 23 24 perpln2 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( w L X ) e. ran L )
26 5 adantr 
 |-  ( ( ph /\ -. X e. A ) -> A e. ran L )
27 26 ad2antrr 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) -> A e. ran L )
28 27 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> A e. ran L )
29 6 adantr 
 |-  ( ( ph /\ -. X e. A ) -> X e. P )
30 29 ad2antrr 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) -> X e. P )
31 simpllr 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) -> -. X e. A )
32 30 31 eldifd 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) -> X e. ( P \ A ) )
33 32 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> X e. ( P \ A ) )
34 1 2 11 23 28 33 tgelrnpln 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( A ( PlnG ` G ) X ) e. ran ( PlnG ` G ) )
35 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
36 1 35 2 11 23 28 33 elplnglnid 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> A C_ ( A ( PlnG ` G ) X ) )
37 simplr 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) -> y e. A )
38 1 2 35 21 27 37 tglnpt 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) -> y e. P )
39 nelne2 
 |-  ( ( y e. A /\ -. X e. A ) -> y =/= X )
40 37 31 39 syl2anc 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) -> y =/= X )
41 40 necomd 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) -> X =/= y )
42 1 35 2 21 30 38 41 tgelrnln 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) -> ( X L y ) e. ran L )
43 42 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) -> ( X L y ) e. ran L )
44 43 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( X L y ) e. ran L )
45 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> w e. P )
46 27 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) -> A e. ran L )
47 simplr 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) -> t e. ( A \ ( X L y ) ) )
48 47 eldifad 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) -> t e. A )
49 1 2 35 22 46 48 tglnpt 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) -> t e. P )
50 47 eldifbd 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) -> -. t e. ( X L y ) )
51 49 50 eldifd 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) -> t e. ( P \ ( X L y ) ) )
52 51 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> t e. ( P \ ( X L y ) ) )
53 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> w ( ( hpG ` G ) ` ( X L y ) ) t )
54 1 2 11 44 45 52 23 53 hpgssplng 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> w e. ( ( X L y ) ( PlnG ` G ) t ) )
55 30 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) -> X e. P )
56 55 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> X e. P )
57 31 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> -. X e. A )
58 49 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> t e. P )
59 38 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) -> y e. P )
60 59 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> y e. P )
61 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> t =/= y )
62 48 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> t e. A )
63 37 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> y e. A )
64 1 35 2 23 58 60 61 61 28 62 63 tglinethru 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> A = ( t L y ) )
65 57 64 neleqtrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> -. X e. ( t L y ) )
66 56 65 eldifd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> X e. ( P \ ( t L y ) ) )
67 41 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) -> X =/= y )
68 67 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> X =/= y )
69 1 35 2 11 23 66 60 52 68 plngrot 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( ( X L y ) ( PlnG ` G ) t ) = ( ( t L y ) ( PlnG ` G ) X ) )
70 64 oveq1d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( A ( PlnG ` G ) X ) = ( ( t L y ) ( PlnG ` G ) X ) )
71 69 70 eqtr4d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( ( X L y ) ( PlnG ` G ) t ) = ( A ( PlnG ` G ) X ) )
72 54 71 eleqtrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> w e. ( A ( PlnG ` G ) X ) )
73 1 35 2 11 23 28 33 elplngid 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> X e. ( A ( PlnG ` G ) X ) )
74 1 35 2 23 45 56 25 tglnne 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> w =/= X )
75 1 35 2 11 23 34 72 73 74 lnssplng1 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( w L X ) C_ ( A ( PlnG ` G ) X ) )
76 36 63 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> y e. ( A ( PlnG ` G ) X ) )
77 1 35 2 11 23 34 73 76 68 lnssplng1 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( X L y ) C_ ( A ( PlnG ` G ) X ) )
78 eqid 
 |-  ( dist ` G ) = ( dist ` G )
79 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( X L y ) ( perpG ` G ) A )
80 1 78 35 2 23 44 28 79 perpcom 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> A ( perpG ` G ) ( X L y ) )
81 1 78 35 2 23 44 25 24 perpcom 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( w L X ) ( perpG ` G ) ( X L y ) )
82 1 2 11 3 23 34 36 75 77 80 81 perpprlng 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> A .|| ( w L X ) )
83 1 35 2 23 45 56 74 tglinerflx2 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> X e. ( w L X ) )
84 82 83 jca 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( A .|| ( w L X ) /\ X e. ( w L X ) ) )
85 19 25 84 rspcedvdw 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> E. b e. ran L ( A .|| b /\ X e. b ) )
86 85 anasss 
 |-  ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( ( X L y ) ( perpG ` G ) ( w L X ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) ) -> E. b e. ran L ( A .|| b /\ X e. b ) )
87 21 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) -> G e. TarskiG )
88 29 ad4antr 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) -> X e. P )
89 38 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) -> y e. P )
90 27 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) -> A e. ran L )
91 simplr 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) -> z e. A )
92 1 2 35 87 90 91 tglnpt 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) -> z e. P )
93 42 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) -> ( X L y ) e. ran L )
94 simpllr 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) -> ( X L y ) ( perpG ` G ) A )
95 1 78 35 2 87 93 90 94 perpneq 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) -> ( X L y ) =/= A )
96 95 neneqd 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) -> -. ( X L y ) = A )
97 87 adantr 
 |-  ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) /\ z e. ( X L y ) ) -> G e. TarskiG )
98 92 adantr 
 |-  ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) /\ z e. ( X L y ) ) -> z e. P )
99 89 adantr 
 |-  ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) /\ z e. ( X L y ) ) -> y e. P )
100 simplr 
 |-  ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) /\ z e. ( X L y ) ) -> y =/= z )
101 100 necomd 
 |-  ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) /\ z e. ( X L y ) ) -> z =/= y )
102 93 adantr 
 |-  ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) /\ z e. ( X L y ) ) -> ( X L y ) e. ran L )
103 simpr 
 |-  ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) /\ z e. ( X L y ) ) -> z e. ( X L y ) )
104 88 adantr 
 |-  ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) /\ z e. ( X L y ) ) -> X e. P )
105 41 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) /\ z e. ( X L y ) ) -> X =/= y )
106 1 35 2 97 104 99 105 tglinerflx2 
 |-  ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) /\ z e. ( X L y ) ) -> y e. ( X L y ) )
107 1 35 2 97 98 99 101 101 102 103 106 tglinethru 
 |-  ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) /\ z e. ( X L y ) ) -> ( X L y ) = ( z L y ) )
108 90 adantr 
 |-  ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) /\ z e. ( X L y ) ) -> A e. ran L )
109 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) /\ z e. ( X L y ) ) -> z e. A )
110 37 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) /\ z e. ( X L y ) ) -> y e. A )
111 1 35 2 97 98 99 101 101 108 109 110 tglinethru 
 |-  ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) /\ z e. ( X L y ) ) -> A = ( z L y ) )
112 107 111 eqtr4d 
 |-  ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) /\ z e. ( X L y ) ) -> ( X L y ) = A )
113 96 112 mtand 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) -> -. z e. ( X L y ) )
114 41 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) -> X =/= y )
115 114 neneqd 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) -> -. X = y )
116 ioran 
 |-  ( -. ( z e. ( X L y ) \/ X = y ) <-> ( -. z e. ( X L y ) /\ -. X = y ) )
117 113 115 116 sylanbrc 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) -> -. ( z e. ( X L y ) \/ X = y ) )
118 1 2 35 87 88 89 92 117 ncoltgdim2 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ z e. A ) /\ y =/= z ) -> G TarskiGDim>= 2 )
119 1 35 2 21 27 37 tglnpt2 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) -> E. z e. A y =/= z )
120 118 119 r19.29a 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) -> G TarskiGDim>= 2 )
121 120 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) -> G TarskiGDim>= 2 )
122 1 35 2 22 55 59 67 tglinerflx1 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) -> X e. ( X L y ) )
123 1 2 22 121 43 122 49 50 lnperpexs 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) -> E. w e. P ( ( X L y ) ( perpG ` G ) ( w L X ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) )
124 86 123 r19.29a 
 |-  ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) -> E. b e. ran L ( A .|| b /\ X e. b ) )
125 simpr 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) -> ( X L y ) ( perpG ` G ) A )
126 1 78 35 2 21 42 27 125 perpneq 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) -> ( X L y ) =/= A )
127 126 necomd 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) -> A =/= ( X L y ) )
128 1 35 2 21 27 42 37 127 tglnpt4 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) -> E. t e. ( A \ ( X L y ) ) t =/= y )
129 124 128 r19.29a 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) -> E. b e. ran L ( A .|| b /\ X e. b ) )
130 simpr 
 |-  ( ( ph /\ -. X e. A ) -> -. X e. A )
131 1 78 35 2 20 26 29 130 footex 
 |-  ( ( ph /\ -. X e. A ) -> E. y e. A ( X L y ) ( perpG ` G ) A )
132 129 131 r19.29a 
 |-  ( ( ph /\ -. X e. A ) -> E. b e. ran L ( A .|| b /\ X e. b ) )
133 16 132 pm2.61dan 
 |-  ( ph -> E. b e. ran L ( A .|| b /\ X e. b ) )