Metamath Proof Explorer

Theorem midex

Description: Existence of the midpoint, part Theorem 8.22 of Schwabhauser p. 64. Note that this proof requires a construction in 2 dimensions or more, i.e. it does not prove the existence of a midpoint in dimension 1, for a geometry restricted to a line. (Contributed by Thierry Arnoux, 25-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 )
mideu.s 
|- S = ( pInvG ` G )
mideu.1 
|- ( ph -> A e. P )
mideu.2 
|- ( ph -> B e. P )
mideu.3 
|- ( ph -> G TarskiGDim>= 2 )
Assertion midex 
|- ( ph -> E. x e. P B = ( ( S ` x ) ` A ) )

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 mideu.s 
 |-  S = ( pInvG ` G )
7 mideu.1 
 |-  ( ph -> A e. P )
8 mideu.2 
 |-  ( ph -> B e. P )
9 mideu.3 
 |-  ( ph -> G TarskiGDim>= 2 )
10 5 adantr 
 |-  ( ( ph /\ A = B ) -> G e. TarskiG )
11 7 adantr 
 |-  ( ( ph /\ A = B ) -> A e. P )
12 eqid 
 |-  ( S ` A ) = ( S ` A )
13 1 2 3 4 6 10 11 12 mircinv 
 |-  ( ( ph /\ A = B ) -> ( ( S ` A ) ` A ) = A )
14 simpr 
 |-  ( ( ph /\ A = B ) -> A = B )
15 13 14 eqtr2d 
 |-  ( ( ph /\ A = B ) -> B = ( ( S ` A ) ` A ) )
16 fveq2 
 |-  ( x = A -> ( S ` x ) = ( S ` A ) )
17 16 fveq1d 
 |-  ( x = A -> ( ( S ` x ) ` A ) = ( ( S ` A ) ` A ) )
18 17 rspceeqv 
 |-  ( ( A e. P /\ B = ( ( S ` A ) ` A ) ) -> E. x e. P B = ( ( S ` x ) ` A ) )
19 7 15 18 syl2an2r 
 |-  ( ( ph /\ A = B ) -> E. x e. P B = ( ( S ` x ) ` A ) )
20 5 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) -> G e. TarskiG )
21 20 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> G e. TarskiG )
22 7 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) -> A e. P )
23 22 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> A e. P )
24 8 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) -> B e. P )
25 24 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> B e. P )
26 simpllr 
 |-  ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) -> A =/= B )
27 26 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> A =/= B )
28 simplr 
 |-  ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) -> q e. P )
29 28 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> q e. P )
30 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> p e. P )
31 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> t e. P )
32 simp-5r 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> ( B L q ) ( perpG ` G ) ( A L B ) )
33 4 21 32 perpln1 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> ( B L q ) e. ran L )
34 1 3 4 21 23 25 27 tgelrnln 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> ( A L B ) e. ran L )
35 1 2 3 4 21 33 34 32 perpcom 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> ( A L B ) ( perpG ` G ) ( B L q ) )
36 1 3 4 21 25 29 33 tglnne 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> B =/= q )
37 1 3 4 21 25 29 36 tglinecom 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> ( B L q ) = ( q L B ) )
38 35 37 breqtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> ( A L B ) ( perpG ` G ) ( q L B ) )
39 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) )
40 39 simpld 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> ( A L p ) ( perpG ` G ) ( A L B ) )
41 4 21 40 perpln1 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> ( A L p ) e. ran L )
42 1 2 3 4 21 41 34 40 perpcom 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> ( A L B ) ( perpG ` G ) ( A L p ) )
43 27 neneqd 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> -. A = B )
44 39 simprd 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) )
45 44 simpld 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> ( t e. ( A L B ) \/ A = B ) )
46 45 orcomd 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> ( A = B \/ t e. ( A L B ) ) )
47 46 ord 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> ( -. A = B -> t e. ( A L B ) ) )
48 43 47 mpd 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> t e. ( A L B ) )
49 44 simprd 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> t e. ( q I p ) )
50 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> ( A .- p ) ( leG ` G ) ( B .- q ) )
51 1 2 3 4 21 6 23 25 27 29 30 31 38 42 48 49 50 mideulem 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( A .- p ) ( leG ` G ) ( B .- q ) ) -> E. x e. P B = ( ( S ` x ) ` A ) )
52 20 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> G e. TarskiG )
53 52 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) /\ ( x e. P /\ A = ( ( S ` x ) ` B ) ) ) -> G e. TarskiG )
54 simprl 
 |-  ( ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) /\ ( x e. P /\ A = ( ( S ` x ) ` B ) ) ) -> x e. P )
55 eqid 
 |-  ( S ` x ) = ( S ` x )
56 24 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> B e. P )
57 56 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) /\ ( x e. P /\ A = ( ( S ` x ) ` B ) ) ) -> B e. P )
58 simprr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) /\ ( x e. P /\ A = ( ( S ` x ) ` B ) ) ) -> A = ( ( S ` x ) ` B ) )
59 58 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) /\ ( x e. P /\ A = ( ( S ` x ) ` B ) ) ) -> ( ( S ` x ) ` B ) = A )
60 1 2 3 4 6 53 54 55 57 59 mircom 
 |-  ( ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) /\ ( x e. P /\ A = ( ( S ` x ) ` B ) ) ) -> ( ( S ` x ) ` A ) = B )
61 60 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) /\ ( x e. P /\ A = ( ( S ` x ) ` B ) ) ) -> B = ( ( S ` x ) ` A ) )
62 22 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> A e. P )
63 26 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> A =/= B )
64 63 necomd 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> B =/= A )
65 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> p e. P )
66 28 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> q e. P )
67 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> t e. P )
68 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) )
69 68 simpld 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> ( A L p ) ( perpG ` G ) ( A L B ) )
70 4 52 69 perpln1 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> ( A L p ) e. ran L )
71 1 3 4 52 62 65 70 tglnne 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> A =/= p )
72 1 3 4 52 62 65 71 tglinecom 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> ( A L p ) = ( p L A ) )
73 72 70 eqeltrrd 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> ( p L A ) e. ran L )
74 1 3 4 52 56 62 64 tgelrnln 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> ( B L A ) e. ran L )
75 1 3 4 52 62 56 63 tglinecom 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> ( A L B ) = ( B L A ) )
76 69 72 75 3brtr3d 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> ( p L A ) ( perpG ` G ) ( B L A ) )
77 1 2 3 4 52 73 74 76 perpcom 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> ( B L A ) ( perpG ` G ) ( p L A ) )
78 simp-5r 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> ( B L q ) ( perpG ` G ) ( A L B ) )
79 4 52 78 perpln1 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> ( B L q ) e. ran L )
80 78 75 breqtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> ( B L q ) ( perpG ` G ) ( B L A ) )
81 1 2 3 4 52 79 74 80 perpcom 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> ( B L A ) ( perpG ` G ) ( B L q ) )
82 63 neneqd 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> -. A = B )
83 68 simprd 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) )
84 83 simpld 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> ( t e. ( A L B ) \/ A = B ) )
85 84 orcomd 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> ( A = B \/ t e. ( A L B ) ) )
86 85 ord 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> ( -. A = B -> t e. ( A L B ) ) )
87 82 86 mpd 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> t e. ( A L B ) )
88 87 75 eleqtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> t e. ( B L A ) )
89 83 simprd 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> t e. ( q I p ) )
90 1 2 3 52 66 67 65 89 tgbtwncom 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> t e. ( p I q ) )
91 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> ( B .- q ) ( leG ` G ) ( A .- p ) )
92 1 2 3 4 52 6 56 62 64 65 66 67 77 81 88 90 91 mideulem 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> E. x e. P A = ( ( S ` x ) ` B ) )
93 61 92 reximddv 
 |-  ( ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) /\ ( B .- q ) ( leG ` G ) ( A .- p ) ) -> E. x e. P B = ( ( S ` x ) ` A ) )
94 eqid 
 |-  ( leG ` G ) = ( leG ` G )
95 20 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) -> G e. TarskiG )
96 22 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) -> A e. P )
97 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) -> p e. P )
98 24 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) -> B e. P )
99 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) -> q e. P )
100 1 2 3 94 95 96 97 98 99 legtrid 
 |-  ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) -> ( ( A .- p ) ( leG ` G ) ( B .- q ) \/ ( B .- q ) ( leG ` G ) ( A .- p ) ) )
101 51 93 100 mpjaodan 
 |-  ( ( ( ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) /\ p e. P ) /\ t e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) ) -> E. x e. P B = ( ( S ` x ) ` A ) )
102 9 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) -> G TarskiGDim>= 2 )
103 1 2 3 4 20 22 24 28 26 102 colperpex 
 |-  ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( 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. ( q I p ) ) ) )
104 r19.42v 
 |-  ( E. t e. P ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) <-> ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. t e. P ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) )
105 104 rexbii 
 |-  ( E. p e. P E. t e. P ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) <-> 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. ( q I p ) ) ) )
106 103 105 sylibr 
 |-  ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) -> E. p e. P E. t e. P ( ( A L p ) ( perpG ` G ) ( A L B ) /\ ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( q I p ) ) ) )
107 101 106 r19.29vva 
 |-  ( ( ( ( ph /\ A =/= B ) /\ q e. P ) /\ ( B L q ) ( perpG ` G ) ( A L B ) ) -> E. x e. P B = ( ( S ` x ) ` A ) )
108 5 adantr 
 |-  ( ( ph /\ A =/= B ) -> G e. TarskiG )
109 8 adantr 
 |-  ( ( ph /\ A =/= B ) -> B e. P )
110 7 adantr 
 |-  ( ( ph /\ A =/= B ) -> A e. P )
111 simpr 
 |-  ( ( ph /\ A =/= B ) -> A =/= B )
112 111 necomd 
 |-  ( ( ph /\ A =/= B ) -> B =/= A )
113 9 adantr 
 |-  ( ( ph /\ A =/= B ) -> G TarskiGDim>= 2 )
114 1 2 3 4 108 109 110 110 112 113 colperpex 
 |-  ( ( ph /\ A =/= B ) -> E. q e. P ( ( B L q ) ( perpG ` G ) ( B L A ) /\ E. s e. P ( ( s e. ( B L A ) \/ B = A ) /\ s e. ( A I q ) ) ) )
115 simprl 
 |-  ( ( ( ph /\ A =/= B ) /\ ( ( B L q ) ( perpG ` G ) ( B L A ) /\ E. s e. P ( ( s e. ( B L A ) \/ B = A ) /\ s e. ( A I q ) ) ) ) -> ( B L q ) ( perpG ` G ) ( B L A ) )
116 1 3 4 108 110 109 111 tglinecom 
 |-  ( ( ph /\ A =/= B ) -> ( A L B ) = ( B L A ) )
117 116 adantr 
 |-  ( ( ( ph /\ A =/= B ) /\ ( ( B L q ) ( perpG ` G ) ( B L A ) /\ E. s e. P ( ( s e. ( B L A ) \/ B = A ) /\ s e. ( A I q ) ) ) ) -> ( A L B ) = ( B L A ) )
118 115 117 breqtrrd 
 |-  ( ( ( ph /\ A =/= B ) /\ ( ( B L q ) ( perpG ` G ) ( B L A ) /\ E. s e. P ( ( s e. ( B L A ) \/ B = A ) /\ s e. ( A I q ) ) ) ) -> ( B L q ) ( perpG ` G ) ( A L B ) )
119 118 ex 
 |-  ( ( ph /\ A =/= B ) -> ( ( ( B L q ) ( perpG ` G ) ( B L A ) /\ E. s e. P ( ( s e. ( B L A ) \/ B = A ) /\ s e. ( A I q ) ) ) -> ( B L q ) ( perpG ` G ) ( A L B ) ) )
120 119 reximdv 
 |-  ( ( ph /\ A =/= B ) -> ( E. q e. P ( ( B L q ) ( perpG ` G ) ( B L A ) /\ E. s e. P ( ( s e. ( B L A ) \/ B = A ) /\ s e. ( A I q ) ) ) -> E. q e. P ( B L q ) ( perpG ` G ) ( A L B ) ) )
121 114 120 mpd 
 |-  ( ( ph /\ A =/= B ) -> E. q e. P ( B L q ) ( perpG ` G ) ( A L B ) )
122 107 121 r19.29a 
 |-  ( ( ph /\ A =/= B ) -> E. x e. P B = ( ( S ` x ) ` A ) )
123 19 122 pm2.61dane 
 |-  ( ph -> E. x e. P B = ( ( S ` x ) ` A ) )