Metamath Proof Explorer

Theorem lnopp2hpgb

Description: Theorem 9.8 of Schwabhauser p. 71. (Contributed by Thierry Arnoux, 4-Mar-2020)

Ref Expression
Hypotheses ishpg.p 
|- P = ( Base ` G )
ishpg.i 
|- I = ( Itv ` G )
ishpg.l 
|- L = ( LineG ` G )
ishpg.o 
|- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
ishpg.g 
|- ( ph -> G e. TarskiG )
ishpg.d 
|- ( ph -> D e. ran L )
hpgbr.a 
|- ( ph -> A e. P )
hpgbr.b 
|- ( ph -> B e. P )
lnopp2hpgb.c 
|- ( ph -> C e. P )
lnopp2hpgb.1 
|- ( ph -> A O C )
Assertion lnopp2hpgb 
|- ( ph -> ( B O C <-> A ( ( hpG ` G ) ` D ) B ) )

Proof

Step Hyp Ref Expression
1 ishpg.p 
 |-  P = ( Base ` G )
2 ishpg.i 
 |-  I = ( Itv ` G )
3 ishpg.l 
 |-  L = ( LineG ` G )
4 ishpg.o 
 |-  O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
5 ishpg.g 
 |-  ( ph -> G e. TarskiG )
6 ishpg.d 
 |-  ( ph -> D e. ran L )
7 hpgbr.a 
 |-  ( ph -> A e. P )
8 hpgbr.b 
 |-  ( ph -> B e. P )
9 lnopp2hpgb.c 
 |-  ( ph -> C e. P )
10 lnopp2hpgb.1 
 |-  ( ph -> A O C )
11 9 adantr 
 |-  ( ( ph /\ B O C ) -> C e. P )
12 10 adantr 
 |-  ( ( ph /\ B O C ) -> A O C )
13 simpr 
 |-  ( ( ph /\ B O C ) -> B O C )
14 breq2 
 |-  ( d = C -> ( A O d <-> A O C ) )
15 breq2 
 |-  ( d = C -> ( B O d <-> B O C ) )
16 14 15 anbi12d 
 |-  ( d = C -> ( ( A O d /\ B O d ) <-> ( A O C /\ B O C ) ) )
17 16 rspcev 
 |-  ( ( C e. P /\ ( A O C /\ B O C ) ) -> E. d e. P ( A O d /\ B O d ) )
18 11 12 13 17 syl12anc 
 |-  ( ( ph /\ B O C ) -> E. d e. P ( A O d /\ B O d ) )
19 1 2 3 4 5 6 7 8 hpgbr 
 |-  ( ph -> ( A ( ( hpG ` G ) ` D ) B <-> E. d e. P ( A O d /\ B O d ) ) )
20 19 adantr 
 |-  ( ( ph /\ B O C ) -> ( A ( ( hpG ` G ) ` D ) B <-> E. d e. P ( A O d /\ B O d ) ) )
21 18 20 mpbird 
 |-  ( ( ph /\ B O C ) -> A ( ( hpG ` G ) ` D ) B )
22 eqid 
 |-  ( dist ` G ) = ( dist ` G )
23 6 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) -> D e. ran L )
24 23 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> D e. ran L )
25 5 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) -> G e. TarskiG )
26 25 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> G e. TarskiG )
27 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
28 7 ad3antrrr 
 |-  ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) -> A e. P )
29 28 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) -> A e. P )
30 29 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> A e. P )
31 8 ad3antrrr 
 |-  ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) -> B e. P )
32 31 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) -> B e. P )
33 32 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> B e. P )
34 9 ad10antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> C e. P )
35 10 ad10antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> A O C )
36 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> z e. D )
37 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) -> y e. D )
38 1 3 2 25 23 37 tglnpt 
 |-  ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) -> y e. P )
39 38 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> y e. P )
40 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> y e. D )
41 1 22 2 4 3 24 26 30 34 35 oppne1 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> -. A e. D )
42 nelne2 
 |-  ( ( y e. D /\ -. A e. D ) -> y =/= A )
43 40 41 42 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> y =/= A )
44 1 2 3 26 39 30 43 tgelrnln 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> ( y L A ) e. ran L )
45 1 2 3 26 39 30 43 tglinerflx2 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> A e. ( y L A ) )
46 nelne1 
 |-  ( ( A e. ( y L A ) /\ -. A e. D ) -> ( y L A ) =/= D )
47 45 41 46 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> ( y L A ) =/= D )
48 47 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> D =/= ( y L A ) )
49 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> z e. P )
50 simplrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> z e. ( y I A ) )
51 1 2 3 26 39 30 49 43 50 btwnlng1 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> z e. ( y L A ) )
52 36 51 elind 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> z e. ( D i^i ( y L A ) ) )
53 1 2 3 26 39 30 43 tglinerflx1 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> y e. ( y L A ) )
54 40 53 elind 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> y e. ( D i^i ( y L A ) ) )
55 1 2 3 26 24 44 48 52 54 tglineineq 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> z = y )
56 55 43 eqnetrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> z =/= A )
57 56 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> A =/= z )
58 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) -> x e. D )
59 1 3 2 25 23 58 tglnpt 
 |-  ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) -> x e. P )
60 59 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> x e. P )
61 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> x e. D )
62 simplr 
 |-  ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) -> d e. P )
63 62 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) -> d e. P )
64 63 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> d e. P )
65 simprr 
 |-  ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) -> B O d )
66 65 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> B O d )
67 1 22 2 4 3 24 26 33 64 66 oppne1 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> -. B e. D )
68 nelne2 
 |-  ( ( x e. D /\ -. B e. D ) -> x =/= B )
69 61 67 68 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> x =/= B )
70 1 2 3 26 60 33 69 tgelrnln 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> ( x L B ) e. ran L )
71 1 2 3 26 60 33 69 tglinerflx2 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> B e. ( x L B ) )
72 nelne1 
 |-  ( ( B e. ( x L B ) /\ -. B e. D ) -> ( x L B ) =/= D )
73 71 67 72 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> ( x L B ) =/= D )
74 73 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> D =/= ( x L B ) )
75 simplrl 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> z e. ( x I B ) )
76 1 2 3 26 60 33 49 69 75 btwnlng1 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> z e. ( x L B ) )
77 36 76 elind 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> z e. ( D i^i ( x L B ) ) )
78 1 2 3 26 60 33 69 tglinerflx1 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> x e. ( x L B ) )
79 61 78 elind 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> x e. ( D i^i ( x L B ) ) )
80 1 2 3 26 24 70 74 77 79 tglineineq 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> z = x )
81 80 69 eqnetrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> z =/= B )
82 81 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> B =/= z )
83 simprl 
 |-  ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) -> A O d )
84 83 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> A O d )
85 1 22 2 4 3 24 26 30 64 84 oppne2 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> -. d e. D )
86 nelne2 
 |-  ( ( z e. D /\ -. d e. D ) -> z =/= d )
87 36 85 86 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> z =/= d )
88 87 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> d =/= z )
89 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) -> x e. ( A I d ) )
90 89 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> x e. ( A I d ) )
91 1 22 2 26 30 60 64 90 tgbtwncom 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> x e. ( d I A ) )
92 80 91 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> z e. ( d I A ) )
93 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> y e. ( B I d ) )
94 1 22 2 26 33 39 64 93 tgbtwncom 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> y e. ( d I B ) )
95 55 94 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> z e. ( d I B ) )
96 1 2 26 64 49 30 33 88 92 95 tgbtwnconn2 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> ( A e. ( z I B ) \/ B e. ( z I A ) ) )
97 1 2 27 30 33 49 26 ishlg 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> ( A ( ( hlG ` G ) ` z ) B <-> ( A =/= z /\ B =/= z /\ ( A e. ( z I B ) \/ B e. ( z I A ) ) ) ) )
98 57 82 96 97 mpbir3and 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> A ( ( hlG ` G ) ` z ) B )
99 1 22 2 4 3 24 26 27 30 33 34 35 36 98 opphl 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ z e. D ) -> B O C )
100 23 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> D e. ran L )
101 25 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> G e. TarskiG )
102 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> z e. P )
103 32 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> B e. P )
104 9 ad10antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> C e. P )
105 29 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> A e. P )
106 10 ad10antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> A O C )
107 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> y e. D )
108 38 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> y e. P )
109 simplrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> z e. ( y I A ) )
110 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> -. z e. D )
111 nelne2 
 |-  ( ( y e. D /\ -. z e. D ) -> y =/= z )
112 107 110 111 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> y =/= z )
113 112 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> z =/= y )
114 1 22 2 101 108 102 105 109 113 tgbtwnne 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> y =/= A )
115 1 2 27 108 105 102 101 105 109 114 113 btwnhl1 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> z ( ( hlG ` G ) ` y ) A )
116 1 2 27 102 105 108 101 115 hlcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> A ( ( hlG ` G ) ` y ) z )
117 1 22 2 4 3 100 101 27 105 102 104 106 107 116 opphl 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> z O C )
118 58 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> x e. D )
119 59 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> x e. P )
120 simplrl 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> z e. ( x I B ) )
121 nelne2 
 |-  ( ( x e. D /\ -. z e. D ) -> x =/= z )
122 118 110 121 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> x =/= z )
123 122 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> z =/= x )
124 1 22 2 101 119 102 103 120 123 tgbtwnne 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> x =/= B )
125 1 2 27 119 103 102 101 105 120 124 123 btwnhl1 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> z ( ( hlG ` G ) ` x ) B )
126 1 22 2 4 3 100 101 27 102 103 104 117 118 125 opphl 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) /\ -. z e. D ) -> B O C )
127 99 126 pm2.61dan 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) /\ z e. P ) /\ ( z e. ( x I B ) /\ z e. ( y I A ) ) ) -> B O C )
128 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) -> y e. ( B I d ) )
129 1 22 2 25 29 32 63 59 38 89 128 axtgpasch 
 |-  ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) -> E. z e. P ( z e. ( x I B ) /\ z e. ( y I A ) ) )
130 127 129 r19.29a 
 |-  ( ( ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) /\ y e. D ) /\ y e. ( B I d ) ) -> B O C )
131 1 22 2 4 31 62 islnopp 
 |-  ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) -> ( B O d <-> ( ( -. B e. D /\ -. d e. D ) /\ E. t e. D t e. ( B I d ) ) ) )
132 65 131 mpbid 
 |-  ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) -> ( ( -. B e. D /\ -. d e. D ) /\ E. t e. D t e. ( B I d ) ) )
133 132 simprd 
 |-  ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) -> E. t e. D t e. ( B I d ) )
134 eleq1w 
 |-  ( t = y -> ( t e. ( B I d ) <-> y e. ( B I d ) ) )
135 134 cbvrexvw 
 |-  ( E. t e. D t e. ( B I d ) <-> E. y e. D y e. ( B I d ) )
136 133 135 sylib 
 |-  ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) -> E. y e. D y e. ( B I d ) )
137 136 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) -> E. y e. D y e. ( B I d ) )
138 130 137 r19.29a 
 |-  ( ( ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) /\ x e. D ) /\ x e. ( A I d ) ) -> B O C )
139 1 22 2 4 28 62 islnopp 
 |-  ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) -> ( A O d <-> ( ( -. A e. D /\ -. d e. D ) /\ E. t e. D t e. ( A I d ) ) ) )
140 83 139 mpbid 
 |-  ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) -> ( ( -. A e. D /\ -. d e. D ) /\ E. t e. D t e. ( A I d ) ) )
141 140 simprd 
 |-  ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) -> E. t e. D t e. ( A I d ) )
142 eleq1w 
 |-  ( t = x -> ( t e. ( A I d ) <-> x e. ( A I d ) ) )
143 142 cbvrexvw 
 |-  ( E. t e. D t e. ( A I d ) <-> E. x e. D x e. ( A I d ) )
144 141 143 sylib 
 |-  ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) -> E. x e. D x e. ( A I d ) )
145 138 144 r19.29a 
 |-  ( ( ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) /\ d e. P ) /\ ( A O d /\ B O d ) ) -> B O C )
146 19 biimpa 
 |-  ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) -> E. d e. P ( A O d /\ B O d ) )
147 145 146 r19.29a 
 |-  ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) -> B O C )
148 21 147 impbida 
 |-  ( ph -> ( B O C <-> A ( ( hpG ` G ) ` D ) B ) )