Metamath Proof Explorer

Theorem plngcplem

Description: Lemma for plngcp . (Contributed by Thierry Arnoux, 17-Jun-2026)

Ref Expression
Hypotheses plngval.p 
|- P = ( Base ` G )
plngval.i 
|- I = ( Itv ` G )
plngval.1 
|- L = ( LineG ` G )
plngval.e 
|- E = ( PlnG ` G )
plngval.g 
|- ( ph -> G e. TarskiG )
plngcp.a 
|- ( ph -> A e. ran L )
plngcp.r 
|- ( ph -> R e. ( P \ A ) )
plngcp.s 
|- ( ph -> S e. ( ( A E R ) \ A ) )
plngcplem.1 
|- O = { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) }
Assertion plngcplem 
|- ( ph -> ( A E R ) = ( A E S ) )

Proof

Step Hyp Ref Expression
1 plngval.p 
 |-  P = ( Base ` G )
2 plngval.i 
 |-  I = ( Itv ` G )
3 plngval.1 
 |-  L = ( LineG ` G )
4 plngval.e 
 |-  E = ( PlnG ` G )
5 plngval.g 
 |-  ( ph -> G e. TarskiG )
6 plngcp.a 
 |-  ( ph -> A e. ran L )
7 plngcp.r 
 |-  ( ph -> R e. ( P \ A ) )
8 plngcp.s 
 |-  ( ph -> S e. ( ( A E R ) \ A ) )
9 plngcplem.1 
 |-  O = { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) }
10 5 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ S O R ) -> G e. TarskiG )
11 6 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ S O R ) -> A e. ran L )
12 7 eldifad 
 |-  ( ph -> R e. P )
13 12 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ S O R ) -> R e. P )
14 simplr 
 |-  ( ( ( ph /\ x e. P ) /\ S O R ) -> x e. P )
15 8 eldifad 
 |-  ( ph -> S e. ( A E R ) )
16 1 2 3 4 5 6 7 15 plngssp 
 |-  ( ph -> S e. P )
17 16 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ S O R ) -> S e. P )
18 eqid 
 |-  ( dist ` G ) = ( dist ` G )
19 simpr 
 |-  ( ( ( ph /\ x e. P ) /\ S O R ) -> S O R )
20 1 18 2 9 3 11 10 17 13 19 oppcom 
 |-  ( ( ( ph /\ x e. P ) /\ S O R ) -> R O S )
21 1 2 3 9 10 11 13 14 17 20 lnopp2hpgb 
 |-  ( ( ( ph /\ x e. P ) /\ S O R ) -> ( x O S <-> R ( ( hpG ` G ) ` A ) x ) )
22 21 adantlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) -> ( x O S <-> R ( ( hpG ` G ) ` A ) x ) )
23 5 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ R ( ( hpG ` G ) ` A ) x ) -> G e. TarskiG )
24 6 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ R ( ( hpG ` G ) ` A ) x ) -> A e. ran L )
25 12 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ R ( ( hpG ` G ) ` A ) x ) -> R e. P )
26 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ R ( ( hpG ` G ) ` A ) x ) -> x e. P )
27 simpr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ R ( ( hpG ` G ) ` A ) x ) -> R ( ( hpG ` G ) ` A ) x )
28 1 2 3 23 24 25 9 26 27 hpgcom 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ R ( ( hpG ` G ) ` A ) x ) -> x ( ( hpG ` G ) ` A ) R )
29 5 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ x ( ( hpG ` G ) ` A ) R ) -> G e. TarskiG )
30 6 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ x ( ( hpG ` G ) ` A ) R ) -> A e. ran L )
31 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ x ( ( hpG ` G ) ` A ) R ) -> x e. P )
32 12 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ x ( ( hpG ` G ) ` A ) R ) -> R e. P )
33 simpr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ x ( ( hpG ` G ) ` A ) R ) -> x ( ( hpG ` G ) ` A ) R )
34 1 2 3 29 30 31 9 32 33 hpgcom 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ x ( ( hpG ` G ) ` A ) R ) -> R ( ( hpG ` G ) ` A ) x )
35 28 34 impbida 
 |-  ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) -> ( R ( ( hpG ` G ) ` A ) x <-> x ( ( hpG ` G ) ` A ) R ) )
36 22 35 bitr2d 
 |-  ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) -> ( x ( ( hpG ` G ) ` A ) R <-> x O S ) )
37 1 2 3 9 10 11 17 14 13 19 lnopp2hpgb 
 |-  ( ( ( ph /\ x e. P ) /\ S O R ) -> ( x O R <-> S ( ( hpG ` G ) ` A ) x ) )
38 37 adantlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) -> ( x O R <-> S ( ( hpG ` G ) ` A ) x ) )
39 5 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ S ( ( hpG ` G ) ` A ) x ) -> G e. TarskiG )
40 6 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ S ( ( hpG ` G ) ` A ) x ) -> A e. ran L )
41 16 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ S ( ( hpG ` G ) ` A ) x ) -> S e. P )
42 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ S ( ( hpG ` G ) ` A ) x ) -> x e. P )
43 simpr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ S ( ( hpG ` G ) ` A ) x ) -> S ( ( hpG ` G ) ` A ) x )
44 1 2 3 39 40 41 9 42 43 hpgcom 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ S ( ( hpG ` G ) ` A ) x ) -> x ( ( hpG ` G ) ` A ) S )
45 5 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ x ( ( hpG ` G ) ` A ) S ) -> G e. TarskiG )
46 6 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ x ( ( hpG ` G ) ` A ) S ) -> A e. ran L )
47 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ x ( ( hpG ` G ) ` A ) S ) -> x e. P )
48 16 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ x ( ( hpG ` G ) ` A ) S ) -> S e. P )
49 simpr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ x ( ( hpG ` G ) ` A ) S ) -> x ( ( hpG ` G ) ` A ) S )
50 1 2 3 45 46 47 9 48 49 hpgcom 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) /\ x ( ( hpG ` G ) ` A ) S ) -> S ( ( hpG ` G ) ` A ) x )
51 44 50 impbida 
 |-  ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) -> ( S ( ( hpG ` G ) ` A ) x <-> x ( ( hpG ` G ) ` A ) S ) )
52 38 51 bitrd 
 |-  ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) -> ( x O R <-> x ( ( hpG ` G ) ` A ) S ) )
53 36 52 orbi12d 
 |-  ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) -> ( ( x ( ( hpG ` G ) ` A ) R \/ x O R ) <-> ( x O S \/ x ( ( hpG ` G ) ` A ) S ) ) )
54 orcom 
 |-  ( ( x O S \/ x ( ( hpG ` G ) ` A ) S ) <-> ( x ( ( hpG ` G ) ` A ) S \/ x O S ) )
55 53 54 bitrdi 
 |-  ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S O R ) -> ( ( x ( ( hpG ` G ) ` A ) R \/ x O R ) <-> ( x ( ( hpG ` G ) ` A ) S \/ x O S ) ) )
56 5 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x ( ( hpG ` G ) ` A ) R ) -> G e. TarskiG )
57 6 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x ( ( hpG ` G ) ` A ) R ) -> A e. ran L )
58 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x ( ( hpG ` G ) ` A ) R ) -> x e. P )
59 12 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x ( ( hpG ` G ) ` A ) R ) -> R e. P )
60 simpr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x ( ( hpG ` G ) ` A ) R ) -> x ( ( hpG ` G ) ` A ) R )
61 16 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x ( ( hpG ` G ) ` A ) R ) -> S e. P )
62 simplr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x ( ( hpG ` G ) ` A ) R ) -> S ( ( hpG ` G ) ` A ) R )
63 1 2 3 56 57 61 9 59 62 hpgcom 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x ( ( hpG ` G ) ` A ) R ) -> R ( ( hpG ` G ) ` A ) S )
64 1 2 3 56 57 58 9 59 60 61 63 hpgtr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x ( ( hpG ` G ) ` A ) R ) -> x ( ( hpG ` G ) ` A ) S )
65 5 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x ( ( hpG ` G ) ` A ) S ) -> G e. TarskiG )
66 6 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x ( ( hpG ` G ) ` A ) S ) -> A e. ran L )
67 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x ( ( hpG ` G ) ` A ) S ) -> x e. P )
68 16 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x ( ( hpG ` G ) ` A ) S ) -> S e. P )
69 simpr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x ( ( hpG ` G ) ` A ) S ) -> x ( ( hpG ` G ) ` A ) S )
70 12 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x ( ( hpG ` G ) ` A ) S ) -> R e. P )
71 simplr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x ( ( hpG ` G ) ` A ) S ) -> S ( ( hpG ` G ) ` A ) R )
72 1 2 3 65 66 67 9 68 69 70 71 hpgtr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x ( ( hpG ` G ) ` A ) S ) -> x ( ( hpG ` G ) ` A ) R )
73 64 72 impbida 
 |-  ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) -> ( x ( ( hpG ` G ) ` A ) R <-> x ( ( hpG ` G ) ` A ) S ) )
74 6 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O R ) -> A e. ran L )
75 5 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O R ) -> G e. TarskiG )
76 16 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O R ) -> S e. P )
77 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O R ) -> x e. P )
78 12 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O R ) -> R e. P )
79 simplr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O R ) -> S ( ( hpG ` G ) ` A ) R )
80 1 2 3 75 74 76 9 78 79 hpgcom 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O R ) -> R ( ( hpG ` G ) ` A ) S )
81 simpr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O R ) -> x O R )
82 1 18 2 9 3 74 75 77 78 81 oppcom 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O R ) -> R O x )
83 1 2 3 9 75 74 78 76 77 82 lnopp2hpgb 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O R ) -> ( S O x <-> R ( ( hpG ` G ) ` A ) S ) )
84 80 83 mpbird 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O R ) -> S O x )
85 1 18 2 9 3 74 75 76 77 84 oppcom 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O R ) -> x O S )
86 6 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O S ) -> A e. ran L )
87 5 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O S ) -> G e. TarskiG )
88 12 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O S ) -> R e. P )
89 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O S ) -> x e. P )
90 simplr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O S ) -> S ( ( hpG ` G ) ` A ) R )
91 16 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O S ) -> S e. P )
92 simpr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O S ) -> x O S )
93 1 18 2 9 3 86 87 89 91 92 oppcom 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O S ) -> S O x )
94 1 2 3 9 87 86 91 88 89 93 lnopp2hpgb 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O S ) -> ( R O x <-> S ( ( hpG ` G ) ` A ) R ) )
95 90 94 mpbird 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O S ) -> R O x )
96 1 18 2 9 3 86 87 88 89 95 oppcom 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) /\ x O S ) -> x O R )
97 85 96 impbida 
 |-  ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) -> ( x O R <-> x O S ) )
98 73 97 orbi12d 
 |-  ( ( ( ( ph /\ x e. P ) /\ -. x e. A ) /\ S ( ( hpG ` G ) ` A ) R ) -> ( ( x ( ( hpG ` G ) ` A ) R \/ x O R ) <-> ( x ( ( hpG ` G ) ` A ) S \/ x O S ) ) )
99 eleq1 
 |-  ( y = S -> ( y e. A <-> S e. A ) )
100 breq1 
 |-  ( y = S -> ( y ( ( hpG ` G ) ` A ) R <-> S ( ( hpG ` G ) ` A ) R ) )
101 oveq1 
 |-  ( y = S -> ( y I R ) = ( S I R ) )
102 101 eleq2d 
 |-  ( y = S -> ( t e. ( y I R ) <-> t e. ( S I R ) ) )
103 102 rexbidv 
 |-  ( y = S -> ( E. t e. A t e. ( y I R ) <-> E. t e. A t e. ( S I R ) ) )
104 99 100 103 3orbi123d 
 |-  ( y = S -> ( ( y e. A \/ y ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( y I R ) ) <-> ( S e. A \/ S ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( S I R ) ) ) )
105 1 2 3 4 5 6 7 plngval 
 |-  ( ph -> ( A E R ) = { y e. P | ( y e. A \/ y ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( y I R ) ) } )
106 15 105 eleqtrd 
 |-  ( ph -> S e. { y e. P | ( y e. A \/ y ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( y I R ) ) } )
107 104 106 elrabrd 
 |-  ( ph -> ( S e. A \/ S ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( S I R ) ) )
108 3orass 
 |-  ( ( S e. A \/ S ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( S I R ) ) <-> ( S e. A \/ ( S ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( S I R ) ) ) )
109 107 108 sylib 
 |-  ( ph -> ( S e. A \/ ( S ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( S I R ) ) ) )
110 8 eldifbd 
 |-  ( ph -> -. S e. A )
111 109 110 orcnd 
 |-  ( ph -> ( S ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( S I R ) ) )
112 1 18 2 9 16 12 islnopp 
 |-  ( ph -> ( S O R <-> ( ( -. S e. A /\ -. R e. A ) /\ E. t e. A t e. ( S I R ) ) ) )
113 7 eldifbd 
 |-  ( ph -> -. R e. A )
114 110 113 jca 
 |-  ( ph -> ( -. S e. A /\ -. R e. A ) )
115 114 biantrurd 
 |-  ( ph -> ( E. t e. A t e. ( S I R ) <-> ( ( -. S e. A /\ -. R e. A ) /\ E. t e. A t e. ( S I R ) ) ) )
116 112 115 bitr4d 
 |-  ( ph -> ( S O R <-> E. t e. A t e. ( S I R ) ) )
117 116 orbi2d 
 |-  ( ph -> ( ( S ( ( hpG ` G ) ` A ) R \/ S O R ) <-> ( S ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( S I R ) ) ) )
118 111 117 mpbird 
 |-  ( ph -> ( S ( ( hpG ` G ) ` A ) R \/ S O R ) )
119 118 orcomd 
 |-  ( ph -> ( S O R \/ S ( ( hpG ` G ) ` A ) R ) )
120 119 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ -. x e. A ) -> ( S O R \/ S ( ( hpG ` G ) ` A ) R ) )
121 55 98 120 mpjaodan 
 |-  ( ( ( ph /\ x e. P ) /\ -. x e. A ) -> ( ( x ( ( hpG ` G ) ` A ) R \/ x O R ) <-> ( x ( ( hpG ` G ) ` A ) S \/ x O S ) ) )
122 simpr 
 |-  ( ( ( ph /\ x e. P ) /\ -. x e. A ) -> -. x e. A )
123 113 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ -. x e. A ) -> -. R e. A )
124 122 123 jca 
 |-  ( ( ( ph /\ x e. P ) /\ -. x e. A ) -> ( -. x e. A /\ -. R e. A ) )
125 124 biantrurd 
 |-  ( ( ( ph /\ x e. P ) /\ -. x e. A ) -> ( E. t e. A t e. ( x I R ) <-> ( ( -. x e. A /\ -. R e. A ) /\ E. t e. A t e. ( x I R ) ) ) )
126 simpr 
 |-  ( ( ph /\ x e. P ) -> x e. P )
127 12 adantr 
 |-  ( ( ph /\ x e. P ) -> R e. P )
128 1 18 2 9 126 127 islnopp 
 |-  ( ( ph /\ x e. P ) -> ( x O R <-> ( ( -. x e. A /\ -. R e. A ) /\ E. t e. A t e. ( x I R ) ) ) )
129 128 adantr 
 |-  ( ( ( ph /\ x e. P ) /\ -. x e. A ) -> ( x O R <-> ( ( -. x e. A /\ -. R e. A ) /\ E. t e. A t e. ( x I R ) ) ) )
130 125 129 bitr4d 
 |-  ( ( ( ph /\ x e. P ) /\ -. x e. A ) -> ( E. t e. A t e. ( x I R ) <-> x O R ) )
131 130 orbi2d 
 |-  ( ( ( ph /\ x e. P ) /\ -. x e. A ) -> ( ( x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) <-> ( x ( ( hpG ` G ) ` A ) R \/ x O R ) ) )
132 110 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ -. x e. A ) -> -. S e. A )
133 122 132 jca 
 |-  ( ( ( ph /\ x e. P ) /\ -. x e. A ) -> ( -. x e. A /\ -. S e. A ) )
134 133 biantrurd 
 |-  ( ( ( ph /\ x e. P ) /\ -. x e. A ) -> ( E. t e. A t e. ( x I S ) <-> ( ( -. x e. A /\ -. S e. A ) /\ E. t e. A t e. ( x I S ) ) ) )
135 16 adantr 
 |-  ( ( ph /\ x e. P ) -> S e. P )
136 1 18 2 9 126 135 islnopp 
 |-  ( ( ph /\ x e. P ) -> ( x O S <-> ( ( -. x e. A /\ -. S e. A ) /\ E. t e. A t e. ( x I S ) ) ) )
137 136 adantr 
 |-  ( ( ( ph /\ x e. P ) /\ -. x e. A ) -> ( x O S <-> ( ( -. x e. A /\ -. S e. A ) /\ E. t e. A t e. ( x I S ) ) ) )
138 134 137 bitr4d 
 |-  ( ( ( ph /\ x e. P ) /\ -. x e. A ) -> ( E. t e. A t e. ( x I S ) <-> x O S ) )
139 138 orbi2d 
 |-  ( ( ( ph /\ x e. P ) /\ -. x e. A ) -> ( ( x ( ( hpG ` G ) ` A ) S \/ E. t e. A t e. ( x I S ) ) <-> ( x ( ( hpG ` G ) ` A ) S \/ x O S ) ) )
140 121 131 139 3bitr4d 
 |-  ( ( ( ph /\ x e. P ) /\ -. x e. A ) -> ( ( x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) <-> ( x ( ( hpG ` G ) ` A ) S \/ E. t e. A t e. ( x I S ) ) ) )
141 140 pm5.74da 
 |-  ( ( ph /\ x e. P ) -> ( ( -. x e. A -> ( x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) ) <-> ( -. x e. A -> ( x ( ( hpG ` G ) ` A ) S \/ E. t e. A t e. ( x I S ) ) ) ) )
142 3orass 
 |-  ( ( x e. A \/ x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) <-> ( x e. A \/ ( x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) ) )
143 df-or 
 |-  ( ( x e. A \/ ( x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) ) <-> ( -. x e. A -> ( x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) ) )
144 142 143 bitri 
 |-  ( ( x e. A \/ x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) <-> ( -. x e. A -> ( x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) ) )
145 3orass 
 |-  ( ( x e. A \/ x ( ( hpG ` G ) ` A ) S \/ E. t e. A t e. ( x I S ) ) <-> ( x e. A \/ ( x ( ( hpG ` G ) ` A ) S \/ E. t e. A t e. ( x I S ) ) ) )
146 df-or 
 |-  ( ( x e. A \/ ( x ( ( hpG ` G ) ` A ) S \/ E. t e. A t e. ( x I S ) ) ) <-> ( -. x e. A -> ( x ( ( hpG ` G ) ` A ) S \/ E. t e. A t e. ( x I S ) ) ) )
147 145 146 bitri 
 |-  ( ( x e. A \/ x ( ( hpG ` G ) ` A ) S \/ E. t e. A t e. ( x I S ) ) <-> ( -. x e. A -> ( x ( ( hpG ` G ) ` A ) S \/ E. t e. A t e. ( x I S ) ) ) )
148 141 144 147 3bitr4g 
 |-  ( ( ph /\ x e. P ) -> ( ( x e. A \/ x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) <-> ( x e. A \/ x ( ( hpG ` G ) ` A ) S \/ E. t e. A t e. ( x I S ) ) ) )
149 148 rabbidva 
 |-  ( ph -> { x e. P | ( x e. A \/ x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) } = { x e. P | ( x e. A \/ x ( ( hpG ` G ) ` A ) S \/ E. t e. A t e. ( x I S ) ) } )
150 1 2 3 4 5 6 7 plngval 
 |-  ( ph -> ( A E R ) = { x e. P | ( x e. A \/ x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) } )
151 16 110 eldifd 
 |-  ( ph -> S e. ( P \ A ) )
152 1 2 3 4 5 6 151 plngval 
 |-  ( ph -> ( A E S ) = { x e. P | ( x e. A \/ x ( ( hpG ` G ) ` A ) S \/ E. t e. A t e. ( x I S ) ) } )
153 149 150 152 3eqtr4d 
 |-  ( ph -> ( A E R ) = ( A E S ) )