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 ⊢ ( 𝜑 → ( 𝑈 ( 𝐾 ‘ 𝑅 ) 𝐴 ↔ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) )