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 𝑃 = ( Base ‘ 𝐺 )
hpg.d = ( dist ‘ 𝐺 )
hpg.i 𝐼 = ( Itv ‘ 𝐺 )
hpg.o 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑏 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
opphl.l 𝐿 = ( LineG ‘ 𝐺 )
opphl.d ( 𝜑𝐷 ∈ ran 𝐿 )
opphl.g ( 𝜑𝐺 ∈ TarskiG )
opphl.k 𝐾 = ( hlG ‘ 𝐺 )
opphllem5.n 𝑁 = ( ( pInvG ‘ 𝐺 ) ‘ 𝑀 )
opphllem5.a ( 𝜑𝐴𝑃 )
opphllem5.c ( 𝜑𝐶𝑃 )
opphllem5.r ( 𝜑𝑅𝐷 )
opphllem5.s ( 𝜑𝑆𝐷 )
opphllem5.m ( 𝜑𝑀𝑃 )
opphllem5.o ( 𝜑𝐴 𝑂 𝐶 )
opphllem5.p ( 𝜑𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑅 ) )
opphllem5.q ( 𝜑𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 𝑆 ) )
opphllem3.t ( 𝜑𝑅𝑆 )
opphllem3.l ( 𝜑 → ( 𝑆 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 𝐴 ) )
opphllem3.u ( 𝜑𝑈𝑃 )
opphllem3.v ( 𝜑 → ( 𝑁𝑅 ) = 𝑆 )
Assertion opphllem3 ( 𝜑 → ( 𝑈 ( 𝐾𝑅 ) 𝐴 ↔ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) )

Proof

Step Hyp Ref Expression
1 hpg.p 𝑃 = ( Base ‘ 𝐺 )
2 hpg.d = ( dist ‘ 𝐺 )
3 hpg.i 𝐼 = ( Itv ‘ 𝐺 )
4 hpg.o 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑏 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
5 opphl.l 𝐿 = ( LineG ‘ 𝐺 )
6 opphl.d ( 𝜑𝐷 ∈ ran 𝐿 )
7 opphl.g ( 𝜑𝐺 ∈ TarskiG )
8 opphl.k 𝐾 = ( hlG ‘ 𝐺 )
9 opphllem5.n 𝑁 = ( ( pInvG ‘ 𝐺 ) ‘ 𝑀 )
10 opphllem5.a ( 𝜑𝐴𝑃 )
11 opphllem5.c ( 𝜑𝐶𝑃 )
12 opphllem5.r ( 𝜑𝑅𝐷 )
13 opphllem5.s ( 𝜑𝑆𝐷 )
14 opphllem5.m ( 𝜑𝑀𝑃 )
15 opphllem5.o ( 𝜑𝐴 𝑂 𝐶 )
16 opphllem5.p ( 𝜑𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑅 ) )
17 opphllem5.q ( 𝜑𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 𝑆 ) )
18 opphllem3.t ( 𝜑𝑅𝑆 )
19 opphllem3.l ( 𝜑 → ( 𝑆 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 𝐴 ) )
20 opphllem3.u ( 𝜑𝑈𝑃 )
21 opphllem3.v ( 𝜑 → ( 𝑁𝑅 ) = 𝑆 )
22 20 ad4antr ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝑈𝑃 )
23 10 ad4antr ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝐴𝑃 )
24 1 5 3 7 6 12 tglnpt ( 𝜑𝑅𝑃 )
25 24 ad4antr ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝑅𝑃 )
26 7 ad4antr ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝐺 ∈ TarskiG )
27 simplr ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝑝𝑃 )
28 simprl ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) )
29 5 7 16 perpln2 ( 𝜑 → ( 𝐴 𝐿 𝑅 ) ∈ ran 𝐿 )
30 1 3 5 7 10 24 29 tglnne ( 𝜑𝐴𝑅 )
31 30 ad4antr ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝐴𝑅 )
32 11 ad4antr ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝐶𝑃 )
33 1 5 3 7 6 13 tglnpt ( 𝜑𝑆𝑃 )
34 33 ad4antr ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝑆𝑃 )
35 simprr ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) )
36 1 2 3 26 34 32 25 27 35 tgcgrcomlr ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → ( 𝐶 𝑆 ) = ( 𝑝 𝑅 ) )
37 17 ad4antr ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 𝑆 ) )
38 5 26 37 perpln2 ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → ( 𝐶 𝐿 𝑆 ) ∈ ran 𝐿 )
39 1 3 5 26 32 34 38 tglnne ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝐶𝑆 )
40 1 2 3 26 32 34 27 25 36 39 tgcgrneq ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝑝𝑅 )
41 1 3 8 22 23 25 26 27 28 31 40 hlbtwn ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → ( 𝑈 ( 𝐾𝑅 ) 𝐴𝑈 ( 𝐾𝑅 ) 𝑝 ) )
42 eqid ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
43 26 adantr ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑈 ( 𝐾𝑅 ) 𝑝 ) → 𝐺 ∈ TarskiG )
44 14 ad5antr ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑈 ( 𝐾𝑅 ) 𝑝 ) → 𝑀𝑃 )
45 22 adantr ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑈 ( 𝐾𝑅 ) 𝑝 ) → 𝑈𝑃 )
46 simpllr ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑈 ( 𝐾𝑅 ) 𝑝 ) → 𝑝𝑃 )
47 25 adantr ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑈 ( 𝐾𝑅 ) 𝑝 ) → 𝑅𝑃 )
48 simpr ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑈 ( 𝐾𝑅 ) 𝑝 ) → 𝑈 ( 𝐾𝑅 ) 𝑝 )
49 1 2 3 5 42 43 9 8 44 45 46 47 48 mirhl ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑈 ( 𝐾𝑅 ) 𝑝 ) → ( 𝑁𝑈 ) ( 𝐾 ‘ ( 𝑁𝑅 ) ) ( 𝑁𝑝 ) )
50 eqidd ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑈 ( 𝐾𝑅 ) 𝑝 ) → ( 𝑁𝑈 ) = ( 𝑁𝑈 ) )
51 21 ad5antr ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑈 ( 𝐾𝑅 ) 𝑝 ) → ( 𝑁𝑅 ) = 𝑆 )
52 51 fveq2d ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑈 ( 𝐾𝑅 ) 𝑝 ) → ( 𝐾 ‘ ( 𝑁𝑅 ) ) = ( 𝐾𝑆 ) )
53 simprr ( ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑚𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) )
54 26 ad2antrr ( ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑚𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → 𝐺 ∈ TarskiG )
55 simplr ( ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑚𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → 𝑚𝑃 )
56 14 ad6antr ( ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑚𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → 𝑀𝑃 )
57 34 ad2antrr ( ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑚𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → 𝑆𝑃 )
58 25 ad2antrr ( ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑚𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → 𝑅𝑃 )
59 simprl ( ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑚𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) )
60 59 eqcomd ( ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑚𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) = 𝑅 )
61 9 fveq1i ( 𝑁𝑆 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑀 ) ‘ 𝑆 )
62 1 2 3 5 42 7 14 9 24 21 mircom ( 𝜑 → ( 𝑁𝑆 ) = 𝑅 )
63 61 62 eqtr3id ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑀 ) ‘ 𝑆 ) = 𝑅 )
64 63 ad6antr ( ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑚𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑀 ) ‘ 𝑆 ) = 𝑅 )
65 1 2 3 5 42 54 55 56 57 58 60 64 miduniq ( ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑚𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → 𝑚 = 𝑀 )
66 65 fveq2d ( ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑚𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑀 ) )
67 66 9 eqtr4di ( ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑚𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) = 𝑁 )
68 67 fveq1d ( ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑚𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) = ( 𝑁𝑝 ) )
69 53 68 eqtr2d ( ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑚𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → ( 𝑁𝑝 ) = 𝐶 )
70 18 ad4antr ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝑅𝑆 )
71 70 necomd ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝑆𝑅 )
72 6 ad4antr ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝐷 ∈ ran 𝐿 )
73 simp-4r ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝑡𝐷 )
74 1 5 3 26 72 73 tglnpt ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝑡𝑃 )
75 13 ad4antr ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝑆𝐷 )
76 12 ad4antr ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝑅𝐷 )
77 1 3 5 26 34 25 71 71 72 75 76 tglinethru ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝐷 = ( 𝑆 𝐿 𝑅 ) )
78 16 ad4antr ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑅 ) )
79 77 78 eqbrtrrd ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → ( 𝑆 𝐿 𝑅 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑅 ) )
80 1 3 5 26 32 34 39 tglinecom ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → ( 𝐶 𝐿 𝑆 ) = ( 𝑆 𝐿 𝐶 ) )
81 37 77 80 3brtr3d ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → ( 𝑆 𝐿 𝑅 ) ( ⟂G ‘ 𝐺 ) ( 𝑆 𝐿 𝐶 ) )
82 73 77 eleqtrd ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝑡 ∈ ( 𝑆 𝐿 𝑅 ) )
83 simpllr ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) )
84 1 2 3 5 26 42 34 25 71 23 32 74 79 81 82 83 27 28 35 opphllem ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → ∃ 𝑚𝑃 ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) )
85 69 84 r19.29a ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → ( 𝑁𝑝 ) = 𝐶 )
86 85 adantr ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑈 ( 𝐾𝑅 ) 𝑝 ) → ( 𝑁𝑝 ) = 𝐶 )
87 50 52 86 breq123d ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑈 ( 𝐾𝑅 ) 𝑝 ) → ( ( 𝑁𝑈 ) ( 𝐾 ‘ ( 𝑁𝑅 ) ) ( 𝑁𝑝 ) ↔ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) )
88 49 87 mpbid ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ 𝑈 ( 𝐾𝑅 ) 𝑝 ) → ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 )
89 26 adantr ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) → 𝐺 ∈ TarskiG )
90 14 ad5antr ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) → 𝑀𝑃 )
91 1 2 3 5 42 7 14 9 20 mircl ( 𝜑 → ( 𝑁𝑈 ) ∈ 𝑃 )
92 91 ad5antr ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) → ( 𝑁𝑈 ) ∈ 𝑃 )
93 32 adantr ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) → 𝐶𝑃 )
94 34 adantr ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) → 𝑆𝑃 )
95 simpr ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) → ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 )
96 1 2 3 5 42 89 9 8 90 92 93 94 95 mirhl ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) → ( 𝑁 ‘ ( 𝑁𝑈 ) ) ( 𝐾 ‘ ( 𝑁𝑆 ) ) ( 𝑁𝐶 ) )
97 22 adantr ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) → 𝑈𝑃 )
98 1 2 3 5 42 89 90 9 97 mirmir ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) → ( 𝑁 ‘ ( 𝑁𝑈 ) ) = 𝑈 )
99 25 adantr ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) → 𝑅𝑃 )
100 21 ad5antr ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) → ( 𝑁𝑅 ) = 𝑆 )
101 1 2 3 5 42 89 90 9 99 100 mircom ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) → ( 𝑁𝑆 ) = 𝑅 )
102 101 fveq2d ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) → ( 𝐾 ‘ ( 𝑁𝑆 ) ) = ( 𝐾𝑅 ) )
103 simpllr ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) → 𝑝𝑃 )
104 85 adantr ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) → ( 𝑁𝑝 ) = 𝐶 )
105 1 2 3 5 42 89 90 9 103 104 mircom ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) → ( 𝑁𝐶 ) = 𝑝 )
106 98 102 105 breq123d ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) → ( ( 𝑁 ‘ ( 𝑁𝑈 ) ) ( 𝐾 ‘ ( 𝑁𝑆 ) ) ( 𝑁𝐶 ) ↔ 𝑈 ( 𝐾𝑅 ) 𝑝 ) )
107 96 106 mpbid ( ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) ∧ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) → 𝑈 ( 𝐾𝑅 ) 𝑝 )
108 88 107 impbida ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → ( 𝑈 ( 𝐾𝑅 ) 𝑝 ↔ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) )
109 41 108 bitrd ( ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) → ( 𝑈 ( 𝐾𝑅 ) 𝐴 ↔ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) )
110 eqid ( ≤G ‘ 𝐺 ) = ( ≤G ‘ 𝐺 )
111 1 2 3 110 7 33 11 24 10 legov ( 𝜑 → ( ( 𝑆 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 𝐴 ) ↔ ∃ 𝑝𝑃 ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) ) )
112 19 111 mpbid ( 𝜑 → ∃ 𝑝𝑃 ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) )
113 112 ad2antrr ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → ∃ 𝑝𝑃 ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 𝐶 ) = ( 𝑅 𝑝 ) ) )
114 109 113 r19.29a ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → ( 𝑈 ( 𝐾𝑅 ) 𝐴 ↔ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) )
115 1 2 3 4 10 11 islnopp ( 𝜑 → ( 𝐴 𝑂 𝐶 ↔ ( ( ¬ 𝐴𝐷 ∧ ¬ 𝐶𝐷 ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ) )
116 15 115 mpbid ( 𝜑 → ( ( ¬ 𝐴𝐷 ∧ ¬ 𝐶𝐷 ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) )
117 116 simprd ( 𝜑 → ∃ 𝑡𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) )
118 114 117 r19.29a ( 𝜑 → ( 𝑈 ( 𝐾𝑅 ) 𝐴 ↔ ( 𝑁𝑈 ) ( 𝐾𝑆 ) 𝐶 ) )