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 ( 𝜑𝑈 𝑂 𝑉 )