Metamath Proof Explorer

Theorem colperpexlem3

Description: Lemma for colperpex . Case 1 of theorem 8.21 of Schwabhauser p. 63. (Contributed by Thierry Arnoux, 20-Nov-2019)

Ref Expression
Hypotheses colperpex.p 
|- P = ( Base ` G )
colperpex.d 
|- .- = ( dist ` G )
colperpex.i 
|- I = ( Itv ` G )
colperpex.l 
|- L = ( LineG ` G )
colperpex.g 
|- ( ph -> G e. TarskiG )
colperpex.1 
|- ( ph -> A e. P )
colperpex.2 
|- ( ph -> B e. P )
colperpex.3 
|- ( ph -> C e. P )
colperpex.4 
|- ( ph -> A =/= B )
colperpexlem3.1 
|- ( ph -> -. C e. ( A L B ) )
Assertion colperpexlem3 
|- ( ph -> E. p e. P ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. t e. P ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) )

Proof

Step Hyp Ref Expression
1 colperpex.p 
 |-  P = ( Base ` G )
2 colperpex.d 
 |-  .- = ( dist ` G )
3 colperpex.i 
 |-  I = ( Itv ` G )
4 colperpex.l 
 |-  L = ( LineG ` G )
5 colperpex.g 
 |-  ( ph -> G e. TarskiG )
6 colperpex.1 
 |-  ( ph -> A e. P )
7 colperpex.2 
 |-  ( ph -> B e. P )
8 colperpex.3 
 |-  ( ph -> C e. P )
9 colperpex.4 
 |-  ( ph -> A =/= B )
10 colperpexlem3.1 
 |-  ( ph -> -. C e. ( A L B ) )
11 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
12 5 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> G e. TarskiG )
13 eqid 
 |-  ( ( pInvG ` G ) ` p ) = ( ( pInvG ` G ) ` p )
14 1 3 4 5 6 7 9 tgelrnln 
 |-  ( ph -> ( A L B ) e. ran L )
15 14 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> ( A L B ) e. ran L )
16 simplr 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> x e. ( A L B ) )
17 1 4 3 12 15 16 tglnpt 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> x e. P )
18 eqid 
 |-  ( ( pInvG ` G ) ` x ) = ( ( pInvG ` G ) ` x )
19 8 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> C e. P )
20 1 2 3 4 11 12 17 18 19 mircl 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> ( ( ( pInvG ` G ) ` x ) ` C ) e. P )
21 6 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> A e. P )
22 eqid 
 |-  ( ( pInvG ` G ) ` A ) = ( ( pInvG ` G ) ` A )
23 1 2 3 4 11 12 21 22 19 mircl 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> ( ( ( pInvG ` G ) ` A ) ` C ) e. P )
24 1 2 3 4 11 12 21 22 19 mircgr 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> ( A .- ( ( ( pInvG ` G ) ` A ) ` C ) ) = ( A .- C ) )
25 7 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> B e. P )
26 10 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> -. C e. ( A L B ) )
27 nelne2 
 |-  ( ( x e. ( A L B ) /\ -. C e. ( A L B ) ) -> x =/= C )
28 16 26 27 syl2anc 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> x =/= C )
29 1 3 4 12 17 19 28 tgelrnln 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> ( x L C ) e. ran L )
30 1 3 4 12 17 19 28 tglinecom 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> ( x L C ) = ( C L x ) )
31 simpr 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> ( C L x ) ( perpG ` G ) ( A L B ) )
32 30 31 eqbrtrd 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> ( x L C ) ( perpG ` G ) ( A L B ) )
33 1 2 3 4 12 29 15 32 perpcom 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> ( A L B ) ( perpG ` G ) ( x L C ) )
34 1 2 3 4 12 21 25 16 19 33 perprag 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> <" A x C "> e. ( raG ` G ) )
35 1 2 3 4 11 12 21 17 19 israg 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> ( <" A x C "> e. ( raG ` G ) <-> ( A .- C ) = ( A .- ( ( ( pInvG ` G ) ` x ) ` C ) ) ) )
36 34 35 mpbid 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> ( A .- C ) = ( A .- ( ( ( pInvG ` G ) ` x ) ` C ) ) )
37 24 36 eqtr2d 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> ( A .- ( ( ( pInvG ` G ) ` x ) ` C ) ) = ( A .- ( ( ( pInvG ` G ) ` A ) ` C ) ) )
38 1 2 3 4 11 12 13 20 23 21 37 midexlem 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> E. p e. P ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) )
39 12 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> G e. TarskiG )
40 23 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( ( ( pInvG ` G ) ` A ) ` C ) e. P )
41 21 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> A e. P )
42 19 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> C e. P )
43 20 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( ( ( pInvG ` G ) ` x ) ` C ) e. P )
44 17 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> x e. P )
45 simplr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> p e. P )
46 1 2 3 4 11 39 41 22 42 mirbtwn 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> A e. ( ( ( ( pInvG ` G ) ` A ) ` C ) I C ) )
47 1 2 3 4 11 39 44 18 42 mirbtwn 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> x e. ( ( ( ( pInvG ` G ) ` x ) ` C ) I C ) )
48 1 2 3 4 11 39 45 13 43 mirbtwn 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> p e. ( ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) I ( ( ( pInvG ` G ) ` x ) ` C ) ) )
49 simpr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) )
50 49 eqcomd 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) = ( ( ( pInvG ` G ) ` A ) ` C ) )
51 50 oveq1d 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) I ( ( ( pInvG ` G ) ` x ) ` C ) ) = ( ( ( ( pInvG ` G ) ` A ) ` C ) I ( ( ( pInvG ` G ) ` x ) ` C ) ) )
52 48 51 eleqtrd 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> p e. ( ( ( ( pInvG ` G ) ` A ) ` C ) I ( ( ( pInvG ` G ) ` x ) ` C ) ) )
53 1 2 3 39 40 41 42 43 44 45 46 47 52 tgtrisegint 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> E. t e. P ( t e. ( p I C ) /\ t e. ( A I x ) ) )
54 39 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> G e. TarskiG )
55 41 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> A e. P )
56 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> t e. P )
57 simplrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> t e. ( A I x ) )
58 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> x = A )
59 58 oveq2d 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( A I x ) = ( A I A ) )
60 57 59 eleqtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> t e. ( A I A ) )
61 1 2 3 54 55 56 60 axtgbtwnid 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> A = t )
62 61 eqcomd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> t = A )
63 62 oveq1d 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( t L p ) = ( A L p ) )
64 50 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) = ( ( ( pInvG ` G ) ` A ) ` C ) )
65 58 fveq2d 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( ( pInvG ` G ) ` x ) = ( ( pInvG ` G ) ` A ) )
66 65 fveq1d 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( ( ( pInvG ` G ) ` x ) ` C ) = ( ( ( pInvG ` G ) ` A ) ` C ) )
67 64 66 eqtr4d 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) = ( ( ( pInvG ` G ) ` x ) ` C ) )
68 45 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> p e. P )
69 43 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( ( ( pInvG ` G ) ` x ) ` C ) e. P )
70 1 2 3 4 11 54 68 13 69 mirinv 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) = ( ( ( pInvG ` G ) ` x ) ` C ) <-> p = ( ( ( pInvG ` G ) ` x ) ` C ) ) )
71 67 70 mpbid 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> p = ( ( ( pInvG ` G ) ` x ) ` C ) )
72 44 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> x e. P )
73 58 oveq1d 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( x I x ) = ( A I x ) )
74 57 73 eleqtrrd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> t e. ( x I x ) )
75 1 2 3 54 72 56 74 axtgbtwnid 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> x = t )
76 75 eqcomd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> t = x )
77 71 76 oveq12d 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( p L t ) = ( ( ( ( pInvG ` G ) ` x ) ` C ) L x ) )
78 34 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> <" A x C "> e. ( raG ` G ) )
79 1 2 3 4 11 39 45 13 43 50 mircom 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` A ) ` C ) ) = ( ( ( pInvG ` G ) ` x ) ` C ) )
80 28 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> x =/= C )
81 1 2 3 4 39 11 22 18 13 41 44 42 45 78 79 80 colperpexlem2 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> A =/= p )
82 81 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> A =/= p )
83 62 82 eqnetrd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> t =/= p )
84 1 3 4 54 56 68 83 tglinecom 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( t L p ) = ( p L t ) )
85 42 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> C e. P )
86 80 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> x =/= C )
87 54 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) /\ ( ( ( pInvG ` G ) ` x ) ` C ) = x ) -> G e. TarskiG )
88 72 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) /\ ( ( ( pInvG ` G ) ` x ) ` C ) = x ) -> x e. P )
89 85 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) /\ ( ( ( pInvG ` G ) ` x ) ` C ) = x ) -> C e. P )
90 1 2 3 4 11 87 88 18 mircinv 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) /\ ( ( ( pInvG ` G ) ` x ) ` C ) = x ) -> ( ( ( pInvG ` G ) ` x ) ` x ) = x )
91 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) /\ ( ( ( pInvG ` G ) ` x ) ` C ) = x ) -> ( ( ( pInvG ` G ) ` x ) ` C ) = x )
92 90 91 eqtr4d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) /\ ( ( ( pInvG ` G ) ` x ) ` C ) = x ) -> ( ( ( pInvG ` G ) ` x ) ` x ) = ( ( ( pInvG ` G ) ` x ) ` C ) )
93 1 2 3 4 11 87 88 18 88 89 92 mireq 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) /\ ( ( ( pInvG ` G ) ` x ) ` C ) = x ) -> x = C )
94 86 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) /\ ( ( ( pInvG ` G ) ` x ) ` C ) = x ) -> x =/= C )
95 94 neneqd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) /\ ( ( ( pInvG ` G ) ` x ) ` C ) = x ) -> -. x = C )
96 93 95 pm2.65da 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> -. ( ( ( pInvG ` G ) ` x ) ` C ) = x )
97 96 neqned 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( ( ( pInvG ` G ) ` x ) ` C ) =/= x )
98 47 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> x e. ( ( ( ( pInvG ` G ) ` x ) ` C ) I C ) )
99 1 3 4 54 72 85 69 86 98 btwnlng2 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( ( ( pInvG ` G ) ` x ) ` C ) e. ( x L C ) )
100 1 3 4 54 72 85 86 69 97 99 tglineelsb2 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( x L C ) = ( x L ( ( ( pInvG ` G ) ` x ) ` C ) ) )
101 28 necomd 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> C =/= x )
102 101 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> C =/= x )
103 1 3 4 54 85 72 102 tglinecom 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( C L x ) = ( x L C ) )
104 1 3 4 54 69 72 97 tglinecom 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( ( ( ( pInvG ` G ) ` x ) ` C ) L x ) = ( x L ( ( ( pInvG ` G ) ` x ) ` C ) ) )
105 100 103 104 3eqtr4d 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( C L x ) = ( ( ( ( pInvG ` G ) ` x ) ` C ) L x ) )
106 77 84 105 3eqtr4d 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( t L p ) = ( C L x ) )
107 63 106 eqtr3d 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( A L p ) = ( C L x ) )
108 31 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( C L x ) ( perpG ` G ) ( A L B ) )
109 107 108 eqbrtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( A L p ) ( perpG ` G ) ( A L B ) )
110 39 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> G e. TarskiG )
111 41 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> A e. P )
112 45 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> p e. P )
113 81 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> A =/= p )
114 1 3 4 110 111 112 113 tgelrnln 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> ( A L p ) e. ran L )
115 15 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> ( A L B ) e. ran L )
116 1 3 4 110 111 112 113 tglinerflx1 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> A e. ( A L p ) )
117 9 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> A =/= B )
118 1 3 4 12 21 25 117 tglinerflx1 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> A e. ( A L B ) )
119 118 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> A e. ( A L B ) )
120 116 119 elind 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> A e. ( ( A L p ) i^i ( A L B ) ) )
121 1 3 4 110 111 112 113 tglinerflx2 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> p e. ( A L p ) )
122 16 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> x e. ( A L B ) )
123 113 necomd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> p =/= A )
124 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> x =/= A )
125 44 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> x e. P )
126 1 2 3 4 39 11 22 18 13 41 44 42 45 78 79 colperpexlem1 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> <" x A p "> e. ( raG ` G ) )
127 126 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> <" x A p "> e. ( raG ` G ) )
128 1 2 3 4 11 110 125 111 112 127 ragcom 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> <" p A x "> e. ( raG ` G ) )
129 1 2 3 4 110 114 115 120 121 122 123 124 128 ragperp 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> ( A L p ) ( perpG ` G ) ( A L B ) )
130 109 129 pm2.61dane 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) -> ( A L p ) ( perpG ` G ) ( A L B ) )
131 118 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> A e. ( A L B ) )
132 62 131 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> t e. ( A L B ) )
133 132 orcd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x = A ) -> ( t e. ( A L B ) \/ A = B ) )
134 25 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> B e. P )
135 117 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> A =/= B )
136 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> t e. P )
137 124 necomd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> A =/= x )
138 simplrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> t e. ( A I x ) )
139 1 3 4 110 111 125 136 137 138 btwnlng1 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> t e. ( A L x ) )
140 1 3 4 110 111 134 135 125 124 122 136 139 tglineeltr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> t e. ( A L B ) )
141 140 orcd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) /\ x =/= A ) -> ( t e. ( A L B ) \/ A = B ) )
142 133 141 pm2.61dane 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) -> ( t e. ( A L B ) \/ A = B ) )
143 39 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) -> G e. TarskiG )
144 45 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) -> p e. P )
145 simplr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) -> t e. P )
146 42 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) -> C e. P )
147 simprl 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) -> t e. ( p I C ) )
148 1 2 3 143 144 145 146 147 tgbtwncom 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) -> t e. ( C I p ) )
149 130 142 148 jca32 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) /\ ( t e. ( p I C ) /\ t e. ( A I x ) ) ) -> ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) )
150 149 ex 
 |-  ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ t e. P ) -> ( ( t e. ( p I C ) /\ t e. ( A I x ) ) -> ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) ) )
151 150 reximdva 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( E. t e. P ( t e. ( p I C ) /\ t e. ( A I x ) ) -> E. t e. P ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) ) )
152 53 151 mpd 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> E. t e. P ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) )
153 r19.42v 
 |-  ( E. t e. P ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) <-> ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. t e. P ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) )
154 152 153 sylib 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. t e. P ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) )
155 154 ex 
 |-  ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) -> ( ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) -> ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. t e. P ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) ) )
156 155 reximdva 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> ( E. p e. P ( ( ( pInvG ` G ) ` A ) ` C ) = ( ( ( pInvG ` G ) ` p ) ` ( ( ( pInvG ` G ) ` x ) ` C ) ) -> E. p e. P ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. t e. P ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) ) )
157 38 156 mpd 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> E. p e. P ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. t e. P ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) )
158 1 2 3 4 5 14 8 10 footex 
 |-  ( ph -> E. x e. ( A L B ) ( C L x ) ( perpG ` G ) ( A L B ) )
159 157 158 r19.29a 
 |-  ( ph -> E. p e. P ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. t e. P ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) )