Metamath Proof Explorer

Theorem opphllem6

Description: First part of Lemma 9.4 of Schwabhauser p. 68. (Contributed by Thierry Arnoux, 3-Mar-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 ‘ 𝐺 ) ( 𝐶 𝐿 𝑆 ) )
opphllem5.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
opphllem6.v ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑅 ) = 𝑆 )
Assertion opphllem6 ( 𝜑 → ( 𝑈 ( 𝐾 ‘ 𝑅 ) 𝐴 ↔ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) )

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 opphllem5.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
19 opphllem6.v ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑅 ) = 𝑆 )
20 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
21 7 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → 𝐺 ∈ TarskiG )
22 14 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → 𝑀 ∈ 𝑃 )
23 10 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → 𝐴 ∈ 𝑃 )
24 11 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → 𝐶 ∈ 𝑃 )
25 18 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → 𝑈 ∈ 𝑃 )
26 1 5 3 7 6 12 tglnpt ⊢ ( 𝜑 → 𝑅 ∈ 𝑃 )
27 5 7 16 perpln2 ⊢ ( 𝜑 → ( 𝐴 𝐿 𝑅 ) ∈ ran 𝐿 )
28 1 3 5 7 10 26 27 tglnne ⊢ ( 𝜑 → 𝐴 ≠ 𝑅 )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → 𝐴 ≠ 𝑅 )
30 19 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → ( 𝑁 ‘ 𝑅 ) = 𝑆 )
31 simpr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → 𝑅 = 𝑆 )
32 30 31 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → ( 𝑁 ‘ 𝑅 ) = 𝑅 )
33 1 2 3 5 20 7 14 9 26 mirinv ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑅 ) = 𝑅 ↔ 𝑀 = 𝑅 ) )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → ( ( 𝑁 ‘ 𝑅 ) = 𝑅 ↔ 𝑀 = 𝑅 ) )
35 32 34 mpbid ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → 𝑀 = 𝑅 )
36 29 35 neeqtrrd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → 𝐴 ≠ 𝑀 )
37 1 5 3 7 6 13 tglnpt ⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
38 5 7 17 perpln2 ⊢ ( 𝜑 → ( 𝐶 𝐿 𝑆 ) ∈ ran 𝐿 )
39 1 3 5 7 11 37 38 tglnne ⊢ ( 𝜑 → 𝐶 ≠ 𝑆 )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → 𝐶 ≠ 𝑆 )
41 35 31 eqtrd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → 𝑀 = 𝑆 )
42 40 41 neeqtrrd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → 𝐶 ≠ 𝑀 )
43 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 = 𝑡 ) → 𝑅 = 𝑡 )
44 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝐺 ∈ TarskiG )
45 11 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝐶 ∈ 𝑃 )
46 26 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑅 ∈ 𝑃 )
47 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐺 ∈ TarskiG )
48 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐷 ∈ ran 𝐿 )
49 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑡 ∈ 𝐷 )
50 1 5 3 47 48 49 tglnpt ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑡 ∈ 𝑃 )
51 50 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑡 ∈ 𝑃 )
52 10 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝐴 ∈ 𝑃 )
53 37 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑆 ∈ 𝑃 )
54 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑅 = 𝑆 )
55 1 3 5 7 11 37 39 tglinerflx2 ⊢ ( 𝜑 → 𝑆 ∈ ( 𝐶 𝐿 𝑆 ) )
56 55 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑆 ∈ ( 𝐶 𝐿 𝑆 ) )
57 54 56 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑅 ∈ ( 𝐶 𝐿 𝑆 ) )
58 57 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑅 ∈ ( 𝐶 𝐿 𝑆 ) )
59 1 2 3 5 7 6 38 17 perpcom ⊢ ( 𝜑 → ( 𝐶 𝐿 𝑆 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
60 59 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → ( 𝐶 𝐿 𝑆 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
61 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑅 ≠ 𝑡 )
62 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝐷 ∈ ran 𝐿 )
63 12 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑅 ∈ 𝐷 )
64 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑡 ∈ 𝐷 )
65 1 3 5 44 46 51 61 61 62 63 64 tglinethru ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝐷 = ( 𝑅 𝐿 𝑡 ) )
66 60 65 breqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → ( 𝐶 𝐿 𝑆 ) ( ⟂G ‘ 𝐺 ) ( 𝑅 𝐿 𝑡 ) )
67 1 2 3 5 44 45 53 58 51 66 perprag ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → ⟨“ 𝐶 𝑅 𝑡 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
68 1 3 5 7 10 26 28 tglinerflx2 ⊢ ( 𝜑 → 𝑅 ∈ ( 𝐴 𝐿 𝑅 ) )
69 68 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑅 ∈ ( 𝐴 𝐿 𝑅 ) )
70 1 2 3 5 7 6 27 16 perpcom ⊢ ( 𝜑 → ( 𝐴 𝐿 𝑅 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
71 70 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → ( 𝐴 𝐿 𝑅 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
72 71 65 breqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → ( 𝐴 𝐿 𝑅 ) ( ⟂G ‘ 𝐺 ) ( 𝑅 𝐿 𝑡 ) )
73 1 2 3 5 44 52 46 69 51 72 perprag ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → ⟨“ 𝐴 𝑅 𝑡 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
74 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) )
75 1 2 3 44 52 51 45 74 tgbtwncom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑡 ∈ ( 𝐶 𝐼 𝐴 ) )
76 1 2 3 5 20 44 45 46 51 52 67 73 75 ragflat2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑅 = 𝑡 )
77 43 76 pm2.61dane ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑅 = 𝑡 )
78 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) )
79 77 78 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑅 ∈ ( 𝐴 𝐼 𝐶 ) )
80 1 2 3 4 10 11 islnopp ⊢ ( 𝜑 → ( 𝐴 𝑂 𝐶 ↔ ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ) )
81 15 80 mpbid ⊢ ( 𝜑 → ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) )
82 81 simprd ⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) )
83 82 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) )
84 79 83 r19.29a ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → 𝑅 ∈ ( 𝐴 𝐼 𝐶 ) )
85 35 84 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → 𝑀 ∈ ( 𝐴 𝐼 𝐶 ) )
86 1 2 3 5 20 21 9 8 22 23 24 25 36 42 85 mirbtwnhl ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → ( 𝑈 ( 𝐾 ‘ 𝑀 ) 𝐴 ↔ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑀 ) 𝐶 ) )
87 35 fveq2d ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → ( 𝐾 ‘ 𝑀 ) = ( 𝐾 ‘ 𝑅 ) )
88 87 breqd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → ( 𝑈 ( 𝐾 ‘ 𝑀 ) 𝐴 ↔ 𝑈 ( 𝐾 ‘ 𝑅 ) 𝐴 ) )
89 41 fveq2d ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → ( 𝐾 ‘ 𝑀 ) = ( 𝐾 ‘ 𝑆 ) )
90 89 breqd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → ( ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑀 ) 𝐶 ↔ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) )
91 86 88 90 3bitr3d ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → ( 𝑈 ( 𝐾 ‘ 𝑅 ) 𝐴 ↔ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) )
92 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝐷 ∈ ran 𝐿 )
93 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝐺 ∈ TarskiG )
94 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝐴 ∈ 𝑃 )
95 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝐶 ∈ 𝑃 )
96 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝑅 ∈ 𝐷 )
97 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝑆 ∈ 𝐷 )
98 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝑀 ∈ 𝑃 )
99 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝐴 𝑂 𝐶 )
100 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑅 ) )
101 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 𝑆 ) )
102 simplr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝑅 ≠ 𝑆 )
103 simpr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) )
104 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝑈 ∈ 𝑃 )
105 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → ( 𝑁 ‘ 𝑅 ) = 𝑆 )
106 1 2 3 4 5 92 93 8 9 94 95 96 97 98 99 100 101 102 103 104 105 opphllem3 ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → ( 𝑈 ( 𝐾 ‘ 𝑅 ) 𝐴 ↔ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) )
107 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝐷 ∈ ran 𝐿 )
108 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝐺 ∈ TarskiG )
109 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝐶 ∈ 𝑃 )
110 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝐴 ∈ 𝑃 )
111 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝑆 ∈ 𝐷 )
112 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝑅 ∈ 𝐷 )
113 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝑀 ∈ 𝑃 )
114 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝐴 𝑂 𝐶 )
115 1 2 3 4 5 107 108 110 109 114 oppcom ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝐶 𝑂 𝐴 )
116 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 𝑆 ) )
117 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑅 ) )
118 simpr ⊢ ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) → 𝑅 ≠ 𝑆 )
119 118 necomd ⊢ ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) → 𝑆 ≠ 𝑅 )
120 119 adantr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝑆 ≠ 𝑅 )
121 simpr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) )
122 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝑈 ∈ 𝑃 )
123 1 2 3 5 20 108 113 9 122 mircl ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → ( 𝑁 ‘ 𝑈 ) ∈ 𝑃 )
124 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝑅 ∈ 𝑃 )
125 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → ( 𝑁 ‘ 𝑅 ) = 𝑆 )
126 1 2 3 5 20 108 113 9 124 125 mircom ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → ( 𝑁 ‘ 𝑆 ) = 𝑅 )
127 1 2 3 4 5 107 108 8 9 109 110 111 112 113 115 116 117 120 121 123 126 opphllem3 ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → ( ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ↔ ( 𝑁 ‘ ( 𝑁 ‘ 𝑈 ) ) ( 𝐾 ‘ 𝑅 ) 𝐴 ) )
128 1 2 3 5 20 108 113 9 122 mirmir ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑈 ) ) = 𝑈 )
129 128 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → ( ( 𝑁 ‘ ( 𝑁 ‘ 𝑈 ) ) ( 𝐾 ‘ 𝑅 ) 𝐴 ↔ 𝑈 ( 𝐾 ‘ 𝑅 ) 𝐴 ) )
130 127 129 bitr2d ⊢ ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → ( 𝑈 ( 𝐾 ‘ 𝑅 ) 𝐴 ↔ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) )
131 eqid ⊢ ( ≤G ‘ 𝐺 ) = ( ≤G ‘ 𝐺 )
132 1 2 3 131 7 37 11 26 10 legtrid ⊢ ( 𝜑 → ( ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ∨ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) )
133 132 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) → ( ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ∨ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) )
134 106 130 133 mpjaodan ⊢ ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) → ( 𝑈 ( 𝐾 ‘ 𝑅 ) 𝐴 ↔ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) )
135 91 134 pm2.61dane ⊢ ( 𝜑 → ( 𝑈 ( 𝐾 ‘ 𝑅 ) 𝐴 ↔ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) )