Metamath Proof Explorer

Theorem opphllem3

Description: Lemma for opphl : We assume opphllem3.l "without loss of generality". (Contributed by Thierry Arnoux, 21-Feb-2020)

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 )
opphllem5.n 
|- N = ( ( pInvG ` G ) ` M )
opphllem5.a 
|- ( ph -> A e. P )
opphllem5.c 
|- ( ph -> C e. P )
opphllem5.r 
|- ( ph -> R e. D )
opphllem5.s 
|- ( ph -> S e. D )
opphllem5.m 
|- ( ph -> M e. P )
opphllem5.o 
|- ( ph -> A O C )
opphllem5.p 
|- ( ph -> D ( perpG ` G ) ( A L R ) )
opphllem5.q 
|- ( ph -> D ( perpG ` G ) ( C L S ) )
opphllem3.t 
|- ( ph -> R =/= S )
opphllem3.l 
|- ( ph -> ( S .- C ) ( leG ` G ) ( R .- A ) )
opphllem3.u 
|- ( ph -> U e. P )
opphllem3.v 
|- ( ph -> ( N ` R ) = S )
Assertion opphllem3 
|- ( ph -> ( U ( K ` R ) A <-> ( N ` U ) ( K ` S ) 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 opphllem5.n 
 |-  N = ( ( pInvG ` G ) ` M )
10 opphllem5.a 
 |-  ( ph -> A e. P )
11 opphllem5.c 
 |-  ( ph -> C e. P )
12 opphllem5.r 
 |-  ( ph -> R e. D )
13 opphllem5.s 
 |-  ( ph -> S e. D )
14 opphllem5.m 
 |-  ( ph -> M e. P )
15 opphllem5.o 
 |-  ( ph -> A O C )
16 opphllem5.p 
 |-  ( ph -> D ( perpG ` G ) ( A L R ) )
17 opphllem5.q 
 |-  ( ph -> D ( perpG ` G ) ( C L S ) )
18 opphllem3.t 
 |-  ( ph -> R =/= S )
19 opphllem3.l 
 |-  ( ph -> ( S .- C ) ( leG ` G ) ( R .- A ) )
20 opphllem3.u 
 |-  ( ph -> U e. P )
21 opphllem3.v 
 |-  ( ph -> ( N ` R ) = S )
22 20 ad4antr 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> U e. P )
23 10 ad4antr 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> A e. P )
24 1 5 3 7 6 12 tglnpt 
 |-  ( ph -> R e. P )
25 24 ad4antr 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> R e. P )
26 7 ad4antr 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> G e. TarskiG )
27 simplr 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> p e. P )
28 simprl 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> p e. ( R I A ) )
29 5 7 16 perpln2 
 |-  ( ph -> ( A L R ) e. ran L )
30 1 3 5 7 10 24 29 tglnne 
 |-  ( ph -> A =/= R )
31 30 ad4antr 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> A =/= R )
32 11 ad4antr 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> C e. P )
33 1 5 3 7 6 13 tglnpt 
 |-  ( ph -> S e. P )
34 33 ad4antr 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> S e. P )
35 simprr 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> ( S .- C ) = ( R .- p ) )
36 1 2 3 26 34 32 25 27 35 tgcgrcomlr 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> ( C .- S ) = ( p .- R ) )
37 17 ad4antr 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> D ( perpG ` G ) ( C L S ) )
38 5 26 37 perpln2 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> ( C L S ) e. ran L )
39 1 3 5 26 32 34 38 tglnne 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> C =/= S )
40 1 2 3 26 32 34 27 25 36 39 tgcgrneq 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> p =/= R )
41 1 3 8 22 23 25 26 27 28 31 40 hlbtwn 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> ( U ( K ` R ) A <-> U ( K ` R ) p ) )
42 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
43 26 adantr 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ U ( K ` R ) p ) -> G e. TarskiG )
44 14 ad5antr 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ U ( K ` R ) p ) -> M e. P )
45 22 adantr 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ U ( K ` R ) p ) -> U e. P )
46 simpllr 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ U ( K ` R ) p ) -> p e. P )
47 25 adantr 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ U ( K ` R ) p ) -> R e. P )
48 simpr 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ U ( K ` R ) p ) -> U ( K ` R ) p )
49 1 2 3 5 42 43 9 8 44 45 46 47 48 mirhl 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ U ( K ` R ) p ) -> ( N ` U ) ( K ` ( N ` R ) ) ( N ` p ) )
50 eqidd 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ U ( K ` R ) p ) -> ( N ` U ) = ( N ` U ) )
51 21 ad5antr 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ U ( K ` R ) p ) -> ( N ` R ) = S )
52 51 fveq2d 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ U ( K ` R ) p ) -> ( K ` ( N ` R ) ) = ( K ` S ) )
53 simprr 
 |-  ( ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ m e. P ) /\ ( R = ( ( ( pInvG ` G ) ` m ) ` S ) /\ C = ( ( ( pInvG ` G ) ` m ) ` p ) ) ) -> C = ( ( ( pInvG ` G ) ` m ) ` p ) )
54 26 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ m e. P ) /\ ( R = ( ( ( pInvG ` G ) ` m ) ` S ) /\ C = ( ( ( pInvG ` G ) ` m ) ` p ) ) ) -> G e. TarskiG )
55 simplr 
 |-  ( ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ m e. P ) /\ ( R = ( ( ( pInvG ` G ) ` m ) ` S ) /\ C = ( ( ( pInvG ` G ) ` m ) ` p ) ) ) -> m e. P )
56 14 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ m e. P ) /\ ( R = ( ( ( pInvG ` G ) ` m ) ` S ) /\ C = ( ( ( pInvG ` G ) ` m ) ` p ) ) ) -> M e. P )
57 34 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ m e. P ) /\ ( R = ( ( ( pInvG ` G ) ` m ) ` S ) /\ C = ( ( ( pInvG ` G ) ` m ) ` p ) ) ) -> S e. P )
58 25 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ m e. P ) /\ ( R = ( ( ( pInvG ` G ) ` m ) ` S ) /\ C = ( ( ( pInvG ` G ) ` m ) ` p ) ) ) -> R e. P )
59 simprl 
 |-  ( ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ m e. P ) /\ ( R = ( ( ( pInvG ` G ) ` m ) ` S ) /\ C = ( ( ( pInvG ` G ) ` m ) ` p ) ) ) -> R = ( ( ( pInvG ` G ) ` m ) ` S ) )
60 59 eqcomd 
 |-  ( ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ m e. P ) /\ ( R = ( ( ( pInvG ` G ) ` m ) ` S ) /\ C = ( ( ( pInvG ` G ) ` m ) ` p ) ) ) -> ( ( ( pInvG ` G ) ` m ) ` S ) = R )
61 9 fveq1i 
 |-  ( N ` S ) = ( ( ( pInvG ` G ) ` M ) ` S )
62 1 2 3 5 42 7 14 9 24 21 mircom 
 |-  ( ph -> ( N ` S ) = R )
63 61 62 eqtr3id 
 |-  ( ph -> ( ( ( pInvG ` G ) ` M ) ` S ) = R )
64 63 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ m e. P ) /\ ( R = ( ( ( pInvG ` G ) ` m ) ` S ) /\ C = ( ( ( pInvG ` G ) ` m ) ` p ) ) ) -> ( ( ( pInvG ` G ) ` M ) ` S ) = R )
65 1 2 3 5 42 54 55 56 57 58 60 64 miduniq 
 |-  ( ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ m e. P ) /\ ( R = ( ( ( pInvG ` G ) ` m ) ` S ) /\ C = ( ( ( pInvG ` G ) ` m ) ` p ) ) ) -> m = M )
66 65 fveq2d 
 |-  ( ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ m e. P ) /\ ( R = ( ( ( pInvG ` G ) ` m ) ` S ) /\ C = ( ( ( pInvG ` G ) ` m ) ` p ) ) ) -> ( ( pInvG ` G ) ` m ) = ( ( pInvG ` G ) ` M ) )
67 66 9 eqtr4di 
 |-  ( ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ m e. P ) /\ ( R = ( ( ( pInvG ` G ) ` m ) ` S ) /\ C = ( ( ( pInvG ` G ) ` m ) ` p ) ) ) -> ( ( pInvG ` G ) ` m ) = N )
68 67 fveq1d 
 |-  ( ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ m e. P ) /\ ( R = ( ( ( pInvG ` G ) ` m ) ` S ) /\ C = ( ( ( pInvG ` G ) ` m ) ` p ) ) ) -> ( ( ( pInvG ` G ) ` m ) ` p ) = ( N ` p ) )
69 53 68 eqtr2d 
 |-  ( ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ m e. P ) /\ ( R = ( ( ( pInvG ` G ) ` m ) ` S ) /\ C = ( ( ( pInvG ` G ) ` m ) ` p ) ) ) -> ( N ` p ) = C )
70 18 ad4antr 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> R =/= S )
71 70 necomd 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> S =/= R )
72 6 ad4antr 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> D e. ran L )
73 simp-4r 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> t e. D )
74 1 5 3 26 72 73 tglnpt 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> t e. P )
75 13 ad4antr 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> S e. D )
76 12 ad4antr 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> R e. D )
77 1 3 5 26 34 25 71 71 72 75 76 tglinethru 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> D = ( S L R ) )
78 16 ad4antr 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> D ( perpG ` G ) ( A L R ) )
79 77 78 eqbrtrrd 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> ( S L R ) ( perpG ` G ) ( A L R ) )
80 1 3 5 26 32 34 39 tglinecom 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> ( C L S ) = ( S L C ) )
81 37 77 80 3brtr3d 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> ( S L R ) ( perpG ` G ) ( S L C ) )
82 73 77 eleqtrd 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> t e. ( S L R ) )
83 simpllr 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> t e. ( A I C ) )
84 1 2 3 5 26 42 34 25 71 23 32 74 79 81 82 83 27 28 35 opphllem 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> E. m e. P ( R = ( ( ( pInvG ` G ) ` m ) ` S ) /\ C = ( ( ( pInvG ` G ) ` m ) ` p ) ) )
85 69 84 r19.29a 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> ( N ` p ) = C )
86 85 adantr 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ U ( K ` R ) p ) -> ( N ` p ) = C )
87 50 52 86 breq123d 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ U ( K ` R ) p ) -> ( ( N ` U ) ( K ` ( N ` R ) ) ( N ` p ) <-> ( N ` U ) ( K ` S ) C ) )
88 49 87 mpbid 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ U ( K ` R ) p ) -> ( N ` U ) ( K ` S ) C )
89 26 adantr 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ ( N ` U ) ( K ` S ) C ) -> G e. TarskiG )
90 14 ad5antr 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ ( N ` U ) ( K ` S ) C ) -> M e. P )
91 1 2 3 5 42 7 14 9 20 mircl 
 |-  ( ph -> ( N ` U ) e. P )
92 91 ad5antr 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ ( N ` U ) ( K ` S ) C ) -> ( N ` U ) e. P )
93 32 adantr 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ ( N ` U ) ( K ` S ) C ) -> C e. P )
94 34 adantr 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ ( N ` U ) ( K ` S ) C ) -> S e. P )
95 simpr 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ ( N ` U ) ( K ` S ) C ) -> ( N ` U ) ( K ` S ) C )
96 1 2 3 5 42 89 9 8 90 92 93 94 95 mirhl 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ ( N ` U ) ( K ` S ) C ) -> ( N ` ( N ` U ) ) ( K ` ( N ` S ) ) ( N ` C ) )
97 22 adantr 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ ( N ` U ) ( K ` S ) C ) -> U e. P )
98 1 2 3 5 42 89 90 9 97 mirmir 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ ( N ` U ) ( K ` S ) C ) -> ( N ` ( N ` U ) ) = U )
99 25 adantr 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ ( N ` U ) ( K ` S ) C ) -> R e. P )
100 21 ad5antr 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ ( N ` U ) ( K ` S ) C ) -> ( N ` R ) = S )
101 1 2 3 5 42 89 90 9 99 100 mircom 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ ( N ` U ) ( K ` S ) C ) -> ( N ` S ) = R )
102 101 fveq2d 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ ( N ` U ) ( K ` S ) C ) -> ( K ` ( N ` S ) ) = ( K ` R ) )
103 simpllr 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ ( N ` U ) ( K ` S ) C ) -> p e. P )
104 85 adantr 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ ( N ` U ) ( K ` S ) C ) -> ( N ` p ) = C )
105 1 2 3 5 42 89 90 9 103 104 mircom 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ ( N ` U ) ( K ` S ) C ) -> ( N ` C ) = p )
106 98 102 105 breq123d 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ ( N ` U ) ( K ` S ) C ) -> ( ( N ` ( N ` U ) ) ( K ` ( N ` S ) ) ( N ` C ) <-> U ( K ` R ) p ) )
107 96 106 mpbid 
 |-  ( ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) /\ ( N ` U ) ( K ` S ) C ) -> U ( K ` R ) p )
108 88 107 impbida 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> ( U ( K ` R ) p <-> ( N ` U ) ( K ` S ) C ) )
109 41 108 bitrd 
 |-  ( ( ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) /\ p e. P ) /\ ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) -> ( U ( K ` R ) A <-> ( N ` U ) ( K ` S ) C ) )
110 eqid 
 |-  ( leG ` G ) = ( leG ` G )
111 1 2 3 110 7 33 11 24 10 legov 
 |-  ( ph -> ( ( S .- C ) ( leG ` G ) ( R .- A ) <-> E. p e. P ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) ) )
112 19 111 mpbid 
 |-  ( ph -> E. p e. P ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) )
113 112 ad2antrr 
 |-  ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) -> E. p e. P ( p e. ( R I A ) /\ ( S .- C ) = ( R .- p ) ) )
114 109 113 r19.29a 
 |-  ( ( ( ph /\ t e. D ) /\ t e. ( A I C ) ) -> ( U ( K ` R ) A <-> ( N ` U ) ( K ` S ) C ) )
115 1 2 3 4 10 11 islnopp 
 |-  ( ph -> ( A O C <-> ( ( -. A e. D /\ -. C e. D ) /\ E. t e. D t e. ( A I C ) ) ) )
116 15 115 mpbid 
 |-  ( ph -> ( ( -. A e. D /\ -. C e. D ) /\ E. t e. D t e. ( A I C ) ) )
117 116 simprd 
 |-  ( ph -> E. t e. D t e. ( A I C ) )
118 114 117 r19.29a 
 |-  ( ph -> ( U ( K ` R ) A <-> ( N ` U ) ( K ` S ) C ) )