Metamath Proof Explorer

Theorem opphl

Description: If two points A and C lie on opposite sides of a line D , then any point of the half line ( R A ) also lies opposite to C . Theorem 9.5 of Schwabhauser p. 69. (Contributed by Thierry Arnoux, 3-Mar-2019)

Ref Expression
Hypotheses hpg.p 
|- P = ( Base ` G )
hpg.d 
|- .- = ( dist ` G )
hpg.i 
|- I = ( Itv ` G )
hpg.o 
|- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
opphl.l 
|- L = ( LineG ` G )
opphl.d 
|- ( ph -> D e. ran L )
opphl.g 
|- ( ph -> G e. TarskiG )
opphl.k 
|- K = ( hlG ` G )
opphl.a 
|- ( ph -> A e. P )
opphl.b 
|- ( ph -> B e. P )
opphl.c 
|- ( ph -> C e. P )
opphl.1 
|- ( ph -> A O C )
opphl.2 
|- ( ph -> R e. D )
opphl.3 
|- ( ph -> A ( K ` R ) B )
Assertion opphl 
|- ( ph -> B O C )

Proof

Step Hyp Ref Expression
1 hpg.p 
 |-  P = ( Base ` G )
2 hpg.d 
 |-  .- = ( dist ` G )
3 hpg.i 
 |-  I = ( Itv ` G )
4 hpg.o 
 |-  O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
5 opphl.l 
 |-  L = ( LineG ` G )
6 opphl.d 
 |-  ( ph -> D e. ran L )
7 opphl.g 
 |-  ( ph -> G e. TarskiG )
8 opphl.k 
 |-  K = ( hlG ` G )
9 opphl.a 
 |-  ( ph -> A e. P )
10 opphl.b 
 |-  ( ph -> B e. P )
11 opphl.c 
 |-  ( ph -> C e. P )
12 opphl.1 
 |-  ( ph -> A O C )
13 opphl.2 
 |-  ( ph -> R e. D )
14 opphl.3 
 |-  ( ph -> A ( K ` R ) B )
15 6 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> D e. ran L )
16 7 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> G e. TarskiG )
17 eqid 
 |-  ( ( pInvG ` G ) ` m ) = ( ( pInvG ` G ) ` m )
18 10 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> B e. P )
19 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
20 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> m e. P )
21 9 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> A e. P )
22 1 2 3 5 19 16 20 17 21 mircl 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> ( ( ( pInvG ` G ) ` m ) ` A ) e. P )
23 simplr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> y e. D )
24 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> z e. D )
25 13 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> R e. D )
26 11 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> C e. P )
27 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> x e. D )
28 12 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> A O C )
29 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> ( A L x ) ( perpG ` G ) D )
30 5 16 29 perpln1 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> ( A L x ) e. ran L )
31 1 2 3 5 16 30 15 29 perpcom 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> D ( perpG ` G ) ( A L x ) )
32 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> ( C L z ) ( perpG ` G ) D )
33 5 16 32 perpln1 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> ( C L z ) e. ran L )
34 1 2 3 5 16 33 15 32 perpcom 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> D ( perpG ` G ) ( C L z ) )
35 1 5 3 16 15 27 tglnpt 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> x e. P )
36 1 3 5 16 21 35 30 tglnne 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> A =/= x )
37 1 3 8 21 21 35 16 36 hlid 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> A ( K ` x ) A )
38 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> z = ( ( ( pInvG ` G ) ` m ) ` x ) )
39 38 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> ( ( ( pInvG ` G ) ` m ) ` x ) = z )
40 1 2 3 4 5 15 16 8 17 21 26 27 24 20 28 31 34 21 39 opphllem6 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> ( A ( K ` x ) A <-> ( ( ( pInvG ` G ) ` m ) ` A ) ( K ` z ) C ) )
41 37 40 mpbid 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> ( ( ( pInvG ` G ) ` m ) ` A ) ( K ` z ) C )
42 1 2 3 4 5 15 16 8 17 21 26 27 24 20 28 31 34 21 22 37 41 opphllem5 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> A O ( ( ( pInvG ` G ) ` m ) ` A ) )
43 39 24 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> ( ( ( pInvG ` G ) ` m ) ` x ) e. D )
44 1 2 3 5 19 16 17 15 20 27 43 mirln2 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> m e. D )
45 1 2 3 5 19 16 20 17 21 mirmir 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> ( ( ( pInvG ` G ) ` m ) ` ( ( ( pInvG ` G ) ` m ) ` A ) ) = A )
46 45 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> A = ( ( ( pInvG ` G ) ` m ) ` ( ( ( pInvG ` G ) ` m ) ` A ) ) )
47 1 5 3 7 6 13 tglnpt 
 |-  ( ph -> R e. P )
48 1 3 8 9 10 47 7 14 hlne1 
 |-  ( ph -> A =/= R )
49 48 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> A =/= R )
50 1 3 8 9 10 47 7 14 hlne2 
 |-  ( ph -> B =/= R )
51 50 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> B =/= R )
52 1 3 8 9 10 47 7 ishlg 
 |-  ( ph -> ( A ( K ` R ) B <-> ( A =/= R /\ B =/= R /\ ( A e. ( R I B ) \/ B e. ( R I A ) ) ) ) )
53 14 52 mpbid 
 |-  ( ph -> ( A =/= R /\ B =/= R /\ ( A e. ( R I B ) \/ B e. ( R I A ) ) ) )
54 53 simp3d 
 |-  ( ph -> ( A e. ( R I B ) \/ B e. ( R I A ) ) )
55 54 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> ( A e. ( R I B ) \/ B e. ( R I A ) ) )
56 1 2 3 4 5 15 16 17 21 18 22 25 42 44 46 49 51 55 opphllem2 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> B O ( ( ( pInvG ` G ) ` m ) ` A ) )
57 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> ( B L y ) ( perpG ` G ) D )
58 5 16 57 perpln1 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> ( B L y ) e. ran L )
59 1 2 3 5 16 58 15 57 perpcom 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> D ( perpG ` G ) ( B L y ) )
60 1 5 3 16 15 24 tglnpt 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> z e. P )
61 1 3 8 22 26 60 16 41 hlne1 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> ( ( ( pInvG ` G ) ` m ) ` A ) =/= z )
62 1 3 8 22 26 60 16 5 41 hlln 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> ( ( ( pInvG ` G ) ` m ) ` A ) e. ( C L z ) )
63 1 3 5 16 26 60 33 tglnne 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> C =/= z )
64 1 3 5 16 26 60 63 tglinerflx2 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> z e. ( C L z ) )
65 1 3 5 16 22 60 61 61 33 62 64 tglinethru 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> ( C L z ) = ( ( ( ( pInvG ` G ) ` m ) ` A ) L z ) )
66 34 65 breqtrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> D ( perpG ` G ) ( ( ( ( pInvG ` G ) ` m ) ` A ) L z ) )
67 1 5 3 16 15 23 tglnpt 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> y e. P )
68 1 3 5 16 18 67 58 tglnne 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> B =/= y )
69 1 3 8 18 21 67 16 68 hlid 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> B ( K ` y ) B )
70 1 3 8 22 26 60 16 41 hlcomd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> C ( K ` z ) ( ( ( pInvG ` G ) ` m ) ` A ) )
71 1 2 3 4 5 15 16 8 17 18 22 23 24 20 56 59 66 18 26 69 70 opphllem5 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) /\ y e. D ) /\ ( B L y ) ( perpG ` G ) D ) -> B O C )
72 1 2 3 4 5 6 7 9 11 12 oppne1 
 |-  ( ph -> -. A e. D )
73 1 3 8 9 10 47 7 5 14 hlln 
 |-  ( ph -> A e. ( B L R ) )
74 73 adantr 
 |-  ( ( ph /\ B e. D ) -> A e. ( B L R ) )
75 7 adantr 
 |-  ( ( ph /\ B e. D ) -> G e. TarskiG )
76 10 adantr 
 |-  ( ( ph /\ B e. D ) -> B e. P )
77 47 adantr 
 |-  ( ( ph /\ B e. D ) -> R e. P )
78 50 adantr 
 |-  ( ( ph /\ B e. D ) -> B =/= R )
79 6 adantr 
 |-  ( ( ph /\ B e. D ) -> D e. ran L )
80 simpr 
 |-  ( ( ph /\ B e. D ) -> B e. D )
81 13 adantr 
 |-  ( ( ph /\ B e. D ) -> R e. D )
82 1 3 5 75 76 77 78 78 79 80 81 tglinethru 
 |-  ( ( ph /\ B e. D ) -> D = ( B L R ) )
83 74 82 eleqtrrd 
 |-  ( ( ph /\ B e. D ) -> A e. D )
84 72 83 mtand 
 |-  ( ph -> -. B e. D )
85 1 2 3 5 7 6 10 84 footex 
 |-  ( ph -> E. y e. D ( B L y ) ( perpG ` G ) D )
86 85 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) -> E. y e. D ( B L y ) ( perpG ` G ) D )
87 71 86 r19.29a 
 |-  ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) /\ m e. P ) /\ z = ( ( ( pInvG ` G ) ` m ) ` x ) ) -> B O C )
88 7 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) -> G e. TarskiG )
89 6 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) -> D e. ran L )
90 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) -> x e. D )
91 1 5 3 88 89 90 tglnpt 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) -> x e. P )
92 simplr 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) -> z e. D )
93 1 5 3 88 89 92 tglnpt 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) -> z e. P )
94 1 2 3 4 5 6 7 9 11 12 opptgdim2 
 |-  ( ph -> G TarskiGDim>= 2 )
95 94 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) -> G TarskiGDim>= 2 )
96 1 2 3 5 88 19 91 93 95 midex 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) -> E. m e. P z = ( ( ( pInvG ` G ) ` m ) ` x ) )
97 87 96 r19.29a 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ z e. D ) /\ ( C L z ) ( perpG ` G ) D ) -> B O C )
98 1 2 3 4 5 6 7 9 11 12 oppne2 
 |-  ( ph -> -. C e. D )
99 1 2 3 5 7 6 11 98 footex 
 |-  ( ph -> E. z e. D ( C L z ) ( perpG ` G ) D )
100 99 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) -> E. z e. D ( C L z ) ( perpG ` G ) D )
101 97 100 r19.29a 
 |-  ( ( ( ph /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) -> B O C )
102 1 2 3 5 7 6 9 72 footex 
 |-  ( ph -> E. x e. D ( A L x ) ( perpG ` G ) D )
103 101 102 r19.29a 
 |-  ( ph -> B O C )