Metamath Proof Explorer

Theorem opphllem5

Description: Second part of Lemma 9.4 of Schwabhauser p. 68. (Contributed by Thierry Arnoux, 2-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 ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
opphllem5.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
opphllem5.1 ⊢ ( 𝜑 → 𝑈 ( 𝐾 ‘ 𝑅 ) 𝐴 )
opphllem5.2 ⊢ ( 𝜑 → 𝑉 ( 𝐾 ‘ 𝑆 ) 𝐶 )
Assertion opphllem5 ( 𝜑 → 𝑈 𝑂 𝑉 )

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 opphllem5.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
20 opphllem5.1 ⊢ ( 𝜑 → 𝑈 ( 𝐾 ‘ 𝑅 ) 𝐴 )
21 opphllem5.2 ⊢ ( 𝜑 → 𝑉 ( 𝐾 ‘ 𝑆 ) 𝐶 )
22 1 5 3 7 6 12 tglnpt ⊢ ( 𝜑 → 𝑅 ∈ 𝑃 )
23 1 3 8 18 10 22 7 20 hlne2 ⊢ ( 𝜑 → 𝐴 ≠ 𝑅 )
24 1 3 5 7 10 22 23 tglinecom ⊢ ( 𝜑 → ( 𝐴 𝐿 𝑅 ) = ( 𝑅 𝐿 𝐴 ) )
25 16 24 breqtrd ⊢ ( 𝜑 → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑅 𝐿 𝐴 ) )
26 1 3 8 18 10 22 7 20 hlcomd ⊢ ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝑅 ) 𝑈 )
27 1 2 3 5 7 6 8 12 10 18 25 26 hlperpnel ⊢ ( 𝜑 → ¬ 𝑈 ∈ 𝐷 )
28 27 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → ¬ 𝑈 ∈ 𝐷 )
29 1 5 3 7 6 13 tglnpt ⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
30 1 3 8 19 11 29 7 21 hlne2 ⊢ ( 𝜑 → 𝐶 ≠ 𝑆 )
31 1 3 5 7 11 29 30 tglinecom ⊢ ( 𝜑 → ( 𝐶 𝐿 𝑆 ) = ( 𝑆 𝐿 𝐶 ) )
32 17 31 breqtrd ⊢ ( 𝜑 → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑆 𝐿 𝐶 ) )
33 1 3 8 19 11 29 7 21 hlcomd ⊢ ( 𝜑 → 𝐶 ( 𝐾 ‘ 𝑆 ) 𝑉 )
34 1 2 3 5 7 6 8 13 11 19 32 33 hlperpnel ⊢ ( 𝜑 → ¬ 𝑉 ∈ 𝐷 )
35 34 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → ¬ 𝑉 ∈ 𝐷 )
36 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑡 ∈ 𝐷 )
37 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 = 𝑡 ) → 𝑅 = 𝑡 )
38 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
39 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝐺 ∈ TarskiG )
40 11 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝐶 ∈ 𝑃 )
41 22 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑅 ∈ 𝑃 )
42 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐺 ∈ TarskiG )
43 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐷 ∈ ran 𝐿 )
44 1 5 3 42 43 36 tglnpt ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑡 ∈ 𝑃 )
45 44 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑡 ∈ 𝑃 )
46 10 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝐴 ∈ 𝑃 )
47 29 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑆 ∈ 𝑃 )
48 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑅 = 𝑆 )
49 1 3 5 7 11 29 30 tglinerflx2 ⊢ ( 𝜑 → 𝑆 ∈ ( 𝐶 𝐿 𝑆 ) )
50 49 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑆 ∈ ( 𝐶 𝐿 𝑆 ) )
51 48 50 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑅 ∈ ( 𝐶 𝐿 𝑆 ) )
52 51 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑅 ∈ ( 𝐶 𝐿 𝑆 ) )
53 5 7 17 perpln2 ⊢ ( 𝜑 → ( 𝐶 𝐿 𝑆 ) ∈ ran 𝐿 )
54 1 2 3 5 7 6 53 17 perpcom ⊢ ( 𝜑 → ( 𝐶 𝐿 𝑆 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
55 54 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → ( 𝐶 𝐿 𝑆 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
56 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑅 ≠ 𝑡 )
57 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝐷 ∈ ran 𝐿 )
58 12 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑅 ∈ 𝐷 )
59 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑡 ∈ 𝐷 )
60 1 3 5 39 41 45 56 56 57 58 59 tglinethru ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝐷 = ( 𝑅 𝐿 𝑡 ) )
61 55 60 breqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → ( 𝐶 𝐿 𝑆 ) ( ⟂G ‘ 𝐺 ) ( 𝑅 𝐿 𝑡 ) )
62 1 2 3 5 39 40 47 52 45 61 perprag ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → ⟨“ 𝐶 𝑅 𝑡 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
63 1 3 5 7 10 22 23 tglinerflx2 ⊢ ( 𝜑 → 𝑅 ∈ ( 𝐴 𝐿 𝑅 ) )
64 63 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑅 ∈ ( 𝐴 𝐿 𝑅 ) )
65 5 7 16 perpln2 ⊢ ( 𝜑 → ( 𝐴 𝐿 𝑅 ) ∈ ran 𝐿 )
66 1 2 3 5 7 6 65 16 perpcom ⊢ ( 𝜑 → ( 𝐴 𝐿 𝑅 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
67 66 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → ( 𝐴 𝐿 𝑅 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
68 67 60 breqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → ( 𝐴 𝐿 𝑅 ) ( ⟂G ‘ 𝐺 ) ( 𝑅 𝐿 𝑡 ) )
69 1 2 3 5 39 46 41 64 45 68 perprag ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → ⟨“ 𝐴 𝑅 𝑡 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
70 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) )
71 1 2 3 39 46 45 40 70 tgbtwncom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑡 ∈ ( 𝐶 𝐼 𝐴 ) )
72 1 2 3 5 38 39 40 41 45 46 62 69 71 ragflat2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑅 ≠ 𝑡 ) → 𝑅 = 𝑡 )
73 37 72 pm2.61dane ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑅 = 𝑡 )
74 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐴 ∈ 𝑃 )
75 18 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑈 ∈ 𝑃 )
76 19 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑉 ∈ 𝑃 )
77 22 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑅 ∈ 𝑃 )
78 26 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐴 ( 𝐾 ‘ 𝑅 ) 𝑈 )
79 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐶 ∈ 𝑃 )
80 21 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑉 ( 𝐾 ‘ 𝑆 ) 𝐶 )
81 48 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → ( 𝐾 ‘ 𝑅 ) = ( 𝐾 ‘ 𝑆 ) )
82 81 breqd ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → ( 𝑉 ( 𝐾 ‘ 𝑅 ) 𝐶 ↔ 𝑉 ( 𝐾 ‘ 𝑆 ) 𝐶 ) )
83 80 82 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑉 ( 𝐾 ‘ 𝑅 ) 𝐶 )
84 1 3 8 76 79 77 42 83 hlcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐶 ( 𝐾 ‘ 𝑅 ) 𝑉 )
85 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) )
86 73 85 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑅 ∈ ( 𝐴 𝐼 𝐶 ) )
87 1 2 3 42 74 77 79 86 tgbtwncom ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑅 ∈ ( 𝐶 𝐼 𝐴 ) )
88 1 3 8 79 76 74 42 77 84 87 btwnhl ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑅 ∈ ( 𝑉 𝐼 𝐴 ) )
89 1 2 3 42 76 77 74 88 tgbtwncom ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑅 ∈ ( 𝐴 𝐼 𝑉 ) )
90 1 3 8 74 75 76 42 77 78 89 btwnhl ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑅 ∈ ( 𝑈 𝐼 𝑉 ) )
91 73 90 eqeltrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑡 ∈ ( 𝑈 𝐼 𝑉 ) )
92 rspe ⊢ ( ( 𝑡 ∈ 𝐷 ∧ 𝑡 ∈ ( 𝑈 𝐼 𝑉 ) ) → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑈 𝐼 𝑉 ) )
93 36 91 92 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑈 𝐼 𝑉 ) )
94 28 35 93 jca31 ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → ( ( ¬ 𝑈 ∈ 𝐷 ∧ ¬ 𝑉 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑈 𝐼 𝑉 ) ) )
95 1 2 3 4 18 19 islnopp ⊢ ( 𝜑 → ( 𝑈 𝑂 𝑉 ↔ ( ( ¬ 𝑈 ∈ 𝐷 ∧ ¬ 𝑉 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑈 𝐼 𝑉 ) ) ) )
96 95 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → ( 𝑈 𝑂 𝑉 ↔ ( ( ¬ 𝑈 ∈ 𝐷 ∧ ¬ 𝑉 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑈 𝐼 𝑉 ) ) ) )
97 94 96 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑅 = 𝑆 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝑈 𝑂 𝑉 )
98 1 2 3 4 10 11 islnopp ⊢ ( 𝜑 → ( 𝐴 𝑂 𝐶 ↔ ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ) )
99 15 98 mpbid ⊢ ( 𝜑 → ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) )
100 99 simprd ⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) )
101 100 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) )
102 97 101 r19.29a ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑆 ) → 𝑈 𝑂 𝑉 )
103 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝐷 ∈ ran 𝐿 )
104 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝐺 ∈ TarskiG )
105 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 )
106 10 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝐴 ∈ 𝑃 )
107 11 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝐶 ∈ 𝑃 )
108 12 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝑅 ∈ 𝐷 )
109 13 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝑆 ∈ 𝐷 )
110 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝑚 ∈ 𝑃 )
111 15 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝐴 𝑂 𝐶 )
112 16 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑅 ) )
113 17 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 𝑆 ) )
114 simpr ⊢ ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) → 𝑅 ≠ 𝑆 )
115 114 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝑅 ≠ 𝑆 )
116 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) )
117 18 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝑈 ∈ 𝑃 )
118 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) )
119 118 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) = 𝑆 )
120 19 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝑉 ∈ 𝑃 )
121 20 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝑈 ( 𝐾 ‘ 𝑅 ) 𝐴 )
122 21 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝑉 ( 𝐾 ‘ 𝑆 ) 𝐶 )
123 1 2 3 4 5 103 104 8 105 106 107 108 109 110 111 112 113 115 116 117 119 120 121 122 opphllem4 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) → 𝑈 𝑂 𝑉 )
124 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝐷 ∈ ran 𝐿 )
125 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝐺 ∈ TarskiG )
126 19 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝑉 ∈ 𝑃 )
127 18 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝑈 ∈ 𝑃 )
128 11 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝐶 ∈ 𝑃 )
129 10 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝐴 ∈ 𝑃 )
130 13 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝑆 ∈ 𝐷 )
131 12 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝑅 ∈ 𝐷 )
132 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝑚 ∈ 𝑃 )
133 15 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝐴 𝑂 𝐶 )
134 1 2 3 4 5 124 125 129 128 133 oppcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝐶 𝑂 𝐴 )
135 17 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 𝑆 ) )
136 16 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑅 ) )
137 114 necomd ⊢ ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) → 𝑆 ≠ 𝑅 )
138 137 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝑆 ≠ 𝑅 )
139 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) )
140 22 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝑅 ∈ 𝑃 )
141 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) )
142 141 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) = 𝑆 )
143 1 2 3 5 38 125 132 105 140 142 mircom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) = 𝑅 )
144 21 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝑉 ( 𝐾 ‘ 𝑆 ) 𝐶 )
145 20 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝑈 ( 𝐾 ‘ 𝑅 ) 𝐴 )
146 1 2 3 4 5 124 125 8 105 128 129 130 131 132 134 135 136 138 139 126 143 127 144 145 opphllem4 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝑉 𝑂 𝑈 )
147 1 2 3 4 5 124 125 126 127 146 oppcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) ∧ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) → 𝑈 𝑂 𝑉 )
148 eqid ⊢ ( ≤G ‘ 𝐺 ) = ( ≤G ‘ 𝐺 )
149 1 2 3 148 7 29 11 22 10 legtrid ⊢ ( 𝜑 → ( ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ∨ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) )
150 149 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) → ( ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ∨ ( 𝑅 − 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝑆 − 𝐶 ) ) )
151 123 147 150 mpjaodan ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) ∧ 𝑚 ∈ 𝑃 ) ∧ 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) ) → 𝑈 𝑂 𝑉 )
152 7 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) → 𝐺 ∈ TarskiG )
153 22 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) → 𝑅 ∈ 𝑃 )
154 29 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) → 𝑆 ∈ 𝑃 )
155 1 2 3 4 5 6 7 10 11 15 opptgdim2 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
156 155 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) → 𝐺 DimTarskiG≥ 2 )
157 1 2 3 5 152 38 153 154 156 midex ⊢ ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) → ∃ 𝑚 ∈ 𝑃 𝑆 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑅 ) )
158 151 157 r19.29a ⊢ ( ( 𝜑 ∧ 𝑅 ≠ 𝑆 ) → 𝑈 𝑂 𝑉 )
159 102 158 pm2.61dane ⊢ ( 𝜑 → 𝑈 𝑂 𝑉 )