Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  midex Structured version   Visualization version   GIF version

Theorem midex 26205
 Description: Existence of the midpoint, part Theorem 8.22 of [Schwabhauser] p. 64. Note that this proof requires a construction in 2 dimensions or more, i.e. it does not prove the existence of a midpoint in dimension 1, for a geometry restricted to a line. (Contributed by Thierry Arnoux, 25-Nov-2019.)
Hypotheses
Ref Expression
colperpex.p 𝑃 = (Base‘𝐺)
colperpex.d = (dist‘𝐺)
colperpex.i 𝐼 = (Itv‘𝐺)
colperpex.l 𝐿 = (LineG‘𝐺)
colperpex.g (𝜑𝐺 ∈ TarskiG)
mideu.s 𝑆 = (pInvG‘𝐺)
mideu.1 (𝜑𝐴𝑃)
mideu.2 (𝜑𝐵𝑃)
mideu.3 (𝜑𝐺DimTarskiG≥2)
Assertion
Ref Expression
midex (𝜑 → ∃𝑥𝑃 𝐵 = ((𝑆𝑥)‘𝐴))
Distinct variable groups:   𝑥,   𝑥,𝐴   𝑥,𝐵   𝑥,𝐺   𝑥,𝐼   𝑥,𝐿   𝑥,𝑃   𝑥,𝑆   𝜑,𝑥

Proof of Theorem midex
Dummy variables 𝑝 𝑞 𝑠 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mideu.1 . . 3 (𝜑𝐴𝑃)
2 colperpex.p . . . . 5 𝑃 = (Base‘𝐺)
3 colperpex.d . . . . 5 = (dist‘𝐺)
4 colperpex.i . . . . 5 𝐼 = (Itv‘𝐺)
5 colperpex.l . . . . 5 𝐿 = (LineG‘𝐺)
6 mideu.s . . . . 5 𝑆 = (pInvG‘𝐺)
7 colperpex.g . . . . . 6 (𝜑𝐺 ∈ TarskiG)
87adantr 481 . . . . 5 ((𝜑𝐴 = 𝐵) → 𝐺 ∈ TarskiG)
91adantr 481 . . . . 5 ((𝜑𝐴 = 𝐵) → 𝐴𝑃)
10 eqid 2795 . . . . 5 (𝑆𝐴) = (𝑆𝐴)
112, 3, 4, 5, 6, 8, 9, 10mircinv 26136 . . . 4 ((𝜑𝐴 = 𝐵) → ((𝑆𝐴)‘𝐴) = 𝐴)
12 simpr 485 . . . 4 ((𝜑𝐴 = 𝐵) → 𝐴 = 𝐵)
1311, 12eqtr2d 2832 . . 3 ((𝜑𝐴 = 𝐵) → 𝐵 = ((𝑆𝐴)‘𝐴))
14 fveq2 6538 . . . . 5 (𝑥 = 𝐴 → (𝑆𝑥) = (𝑆𝐴))
1514fveq1d 6540 . . . 4 (𝑥 = 𝐴 → ((𝑆𝑥)‘𝐴) = ((𝑆𝐴)‘𝐴))
1615rspceeqv 3577 . . 3 ((𝐴𝑃𝐵 = ((𝑆𝐴)‘𝐴)) → ∃𝑥𝑃 𝐵 = ((𝑆𝑥)‘𝐴))
171, 13, 16syl2an2r 681 . 2 ((𝜑𝐴 = 𝐵) → ∃𝑥𝑃 𝐵 = ((𝑆𝑥)‘𝐴))
187ad3antrrr 726 . . . . . . 7 ((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐺 ∈ TarskiG)
1918ad4antr 728 . . . . . 6 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → 𝐺 ∈ TarskiG)
201ad3antrrr 726 . . . . . . 7 ((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐴𝑃)
2120ad4antr 728 . . . . . 6 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → 𝐴𝑃)
22 mideu.2 . . . . . . . 8 (𝜑𝐵𝑃)
2322ad3antrrr 726 . . . . . . 7 ((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐵𝑃)
2423ad4antr 728 . . . . . 6 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → 𝐵𝑃)
25 simpllr 772 . . . . . . 7 ((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐴𝐵)
2625ad4antr 728 . . . . . 6 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → 𝐴𝐵)
27 simplr 765 . . . . . . 7 ((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝑞𝑃)
2827ad4antr 728 . . . . . 6 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → 𝑞𝑃)
29 simp-4r 780 . . . . . 6 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → 𝑝𝑃)
30 simpllr 772 . . . . . 6 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → 𝑡𝑃)
31 simp-5r 782 . . . . . . . . 9 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵))
325, 19, 31perpln1 26178 . . . . . . . 8 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → (𝐵𝐿𝑞) ∈ ran 𝐿)
332, 4, 5, 19, 21, 24, 26tgelrnln 26098 . . . . . . . 8 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → (𝐴𝐿𝐵) ∈ ran 𝐿)
342, 3, 4, 5, 19, 32, 33, 31perpcom 26181 . . . . . . 7 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐵𝐿𝑞))
352, 4, 5, 19, 24, 28, 32tglnne 26096 . . . . . . . 8 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → 𝐵𝑞)
362, 4, 5, 19, 24, 28, 35tglinecom 26103 . . . . . . 7 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → (𝐵𝐿𝑞) = (𝑞𝐿𝐵))
3734, 36breqtrd 4988 . . . . . 6 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑞𝐿𝐵))
38 simplr 765 . . . . . . . . 9 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝))))
3938simpld 495 . . . . . . . 8 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → (𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵))
405, 19, 39perpln1 26178 . . . . . . 7 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → (𝐴𝐿𝑝) ∈ ran 𝐿)
412, 3, 4, 5, 19, 40, 33, 39perpcom 26181 . . . . . 6 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑝))
4226neneqd 2989 . . . . . . 7 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → ¬ 𝐴 = 𝐵)
4338simprd 496 . . . . . . . . . 10 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))
4443simpld 495 . . . . . . . . 9 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → (𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
4544orcomd 866 . . . . . . . 8 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → (𝐴 = 𝐵𝑡 ∈ (𝐴𝐿𝐵)))
4645ord 859 . . . . . . 7 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → (¬ 𝐴 = 𝐵𝑡 ∈ (𝐴𝐿𝐵)))
4742, 46mpd 15 . . . . . 6 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → 𝑡 ∈ (𝐴𝐿𝐵))
4843simprd 496 . . . . . 6 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → 𝑡 ∈ (𝑞𝐼𝑝))
49 simpr 485 . . . . . 6 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞))
502, 3, 4, 5, 19, 6, 21, 24, 26, 28, 29, 30, 37, 41, 47, 48, 49mideulem 26204 . . . . 5 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞)) → ∃𝑥𝑃 𝐵 = ((𝑆𝑥)‘𝐴))
5118ad4antr 728 . . . . . . . . 9 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → 𝐺 ∈ TarskiG)
5251adantr 481 . . . . . . . 8 (((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) ∧ (𝑥𝑃𝐴 = ((𝑆𝑥)‘𝐵))) → 𝐺 ∈ TarskiG)
53 simprl 767 . . . . . . . 8 (((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) ∧ (𝑥𝑃𝐴 = ((𝑆𝑥)‘𝐵))) → 𝑥𝑃)
54 eqid 2795 . . . . . . . 8 (𝑆𝑥) = (𝑆𝑥)
5523ad4antr 728 . . . . . . . . 9 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → 𝐵𝑃)
5655adantr 481 . . . . . . . 8 (((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) ∧ (𝑥𝑃𝐴 = ((𝑆𝑥)‘𝐵))) → 𝐵𝑃)
57 simprr 769 . . . . . . . . 9 (((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) ∧ (𝑥𝑃𝐴 = ((𝑆𝑥)‘𝐵))) → 𝐴 = ((𝑆𝑥)‘𝐵))
5857eqcomd 2801 . . . . . . . 8 (((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) ∧ (𝑥𝑃𝐴 = ((𝑆𝑥)‘𝐵))) → ((𝑆𝑥)‘𝐵) = 𝐴)
592, 3, 4, 5, 6, 52, 53, 54, 56, 58mircom 26131 . . . . . . 7 (((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) ∧ (𝑥𝑃𝐴 = ((𝑆𝑥)‘𝐵))) → ((𝑆𝑥)‘𝐴) = 𝐵)
6059eqcomd 2801 . . . . . 6 (((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) ∧ (𝑥𝑃𝐴 = ((𝑆𝑥)‘𝐵))) → 𝐵 = ((𝑆𝑥)‘𝐴))
6120ad4antr 728 . . . . . . 7 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → 𝐴𝑃)
6225ad4antr 728 . . . . . . . 8 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → 𝐴𝐵)
6362necomd 3039 . . . . . . 7 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → 𝐵𝐴)
64 simp-4r 780 . . . . . . 7 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → 𝑝𝑃)
6527ad4antr 728 . . . . . . 7 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → 𝑞𝑃)
66 simpllr 772 . . . . . . 7 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → 𝑡𝑃)
67 simplr 765 . . . . . . . . . . . . 13 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝))))
6867simpld 495 . . . . . . . . . . . 12 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → (𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵))
695, 51, 68perpln1 26178 . . . . . . . . . . 11 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → (𝐴𝐿𝑝) ∈ ran 𝐿)
702, 4, 5, 51, 61, 64, 69tglnne 26096 . . . . . . . . . 10 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → 𝐴𝑝)
712, 4, 5, 51, 61, 64, 70tglinecom 26103 . . . . . . . . 9 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → (𝐴𝐿𝑝) = (𝑝𝐿𝐴))
7271, 69eqeltrrd 2884 . . . . . . . 8 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → (𝑝𝐿𝐴) ∈ ran 𝐿)
732, 4, 5, 51, 55, 61, 63tgelrnln 26098 . . . . . . . 8 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → (𝐵𝐿𝐴) ∈ ran 𝐿)
742, 4, 5, 51, 61, 55, 62tglinecom 26103 . . . . . . . . 9 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → (𝐴𝐿𝐵) = (𝐵𝐿𝐴))
7568, 71, 743brtr3d 4993 . . . . . . . 8 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → (𝑝𝐿𝐴)(⟂G‘𝐺)(𝐵𝐿𝐴))
762, 3, 4, 5, 51, 72, 73, 75perpcom 26181 . . . . . . 7 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → (𝐵𝐿𝐴)(⟂G‘𝐺)(𝑝𝐿𝐴))
77 simp-5r 782 . . . . . . . . 9 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵))
785, 51, 77perpln1 26178 . . . . . . . 8 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → (𝐵𝐿𝑞) ∈ ran 𝐿)
7977, 74breqtrd 4988 . . . . . . . 8 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐵𝐿𝐴))
802, 3, 4, 5, 51, 78, 73, 79perpcom 26181 . . . . . . 7 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → (𝐵𝐿𝐴)(⟂G‘𝐺)(𝐵𝐿𝑞))
8162neneqd 2989 . . . . . . . . 9 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → ¬ 𝐴 = 𝐵)
8267simprd 496 . . . . . . . . . . . 12 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))
8382simpld 495 . . . . . . . . . . 11 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → (𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
8483orcomd 866 . . . . . . . . . 10 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → (𝐴 = 𝐵𝑡 ∈ (𝐴𝐿𝐵)))
8584ord 859 . . . . . . . . 9 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → (¬ 𝐴 = 𝐵𝑡 ∈ (𝐴𝐿𝐵)))
8681, 85mpd 15 . . . . . . . 8 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → 𝑡 ∈ (𝐴𝐿𝐵))
8786, 74eleqtrd 2885 . . . . . . 7 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → 𝑡 ∈ (𝐵𝐿𝐴))
8882simprd 496 . . . . . . . 8 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → 𝑡 ∈ (𝑞𝐼𝑝))
892, 3, 4, 51, 65, 66, 64, 88tgbtwncom 25956 . . . . . . 7 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → 𝑡 ∈ (𝑝𝐼𝑞))
90 simpr 485 . . . . . . 7 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝))
912, 3, 4, 5, 51, 6, 55, 61, 63, 64, 65, 66, 76, 80, 87, 89, 90mideulem 26204 . . . . . 6 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → ∃𝑥𝑃 𝐴 = ((𝑆𝑥)‘𝐵))
9260, 91reximddv 3238 . . . . 5 ((((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) ∧ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)) → ∃𝑥𝑃 𝐵 = ((𝑆𝑥)‘𝐴))
93 eqid 2795 . . . . . 6 (≤G‘𝐺) = (≤G‘𝐺)
9418ad3antrrr 726 . . . . . 6 (((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) → 𝐺 ∈ TarskiG)
9520ad3antrrr 726 . . . . . 6 (((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) → 𝐴𝑃)
96 simpllr 772 . . . . . 6 (((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) → 𝑝𝑃)
9723ad3antrrr 726 . . . . . 6 (((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) → 𝐵𝑃)
98 simp-5r 782 . . . . . 6 (((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) → 𝑞𝑃)
992, 3, 4, 93, 94, 95, 96, 97, 98legtrid 26059 . . . . 5 (((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) → ((𝐴 𝑝)(≤G‘𝐺)(𝐵 𝑞) ∨ (𝐵 𝑞)(≤G‘𝐺)(𝐴 𝑝)))
10050, 92, 99mpjaodan 953 . . . 4 (((((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑝𝑃) ∧ 𝑡𝑃) ∧ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝)))) → ∃𝑥𝑃 𝐵 = ((𝑆𝑥)‘𝐴))
101 mideu.3 . . . . . . 7 (𝜑𝐺DimTarskiG≥2)
102101ad3antrrr 726 . . . . . 6 ((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐺DimTarskiG≥2)
1032, 3, 4, 5, 18, 20, 23, 27, 25, 102colperpex 26201 . . . . 5 ((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ∃𝑝𝑃 ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ∃𝑡𝑃 ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝))))
104 r19.42v 3311 . . . . . 6 (∃𝑡𝑃 ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝))) ↔ ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ∃𝑡𝑃 ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝))))
105104rexbii 3211 . . . . 5 (∃𝑝𝑃𝑡𝑃 ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝))) ↔ ∃𝑝𝑃 ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ∃𝑡𝑃 ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝))))
106103, 105sylibr 235 . . . 4 ((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ∃𝑝𝑃𝑡𝑃 ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝑞𝐼𝑝))))
107100, 106r19.29vva 3297 . . 3 ((((𝜑𝐴𝐵) ∧ 𝑞𝑃) ∧ (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ∃𝑥𝑃 𝐵 = ((𝑆𝑥)‘𝐴))
1087adantr 481 . . . . 5 ((𝜑𝐴𝐵) → 𝐺 ∈ TarskiG)
10922adantr 481 . . . . 5 ((𝜑𝐴𝐵) → 𝐵𝑃)
1101adantr 481 . . . . 5 ((𝜑𝐴𝐵) → 𝐴𝑃)
111 simpr 485 . . . . . 6 ((𝜑𝐴𝐵) → 𝐴𝐵)
112111necomd 3039 . . . . 5 ((𝜑𝐴𝐵) → 𝐵𝐴)
113101adantr 481 . . . . 5 ((𝜑𝐴𝐵) → 𝐺DimTarskiG≥2)
1142, 3, 4, 5, 108, 109, 110, 110, 112, 113colperpex 26201 . . . 4 ((𝜑𝐴𝐵) → ∃𝑞𝑃 ((𝐵𝐿𝑞)(⟂G‘𝐺)(𝐵𝐿𝐴) ∧ ∃𝑠𝑃 ((𝑠 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴) ∧ 𝑠 ∈ (𝐴𝐼𝑞))))
115 simprl 767 . . . . . . 7 (((𝜑𝐴𝐵) ∧ ((𝐵𝐿𝑞)(⟂G‘𝐺)(𝐵𝐿𝐴) ∧ ∃𝑠𝑃 ((𝑠 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴) ∧ 𝑠 ∈ (𝐴𝐼𝑞)))) → (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐵𝐿𝐴))
1162, 4, 5, 108, 110, 109, 111tglinecom 26103 . . . . . . . 8 ((𝜑𝐴𝐵) → (𝐴𝐿𝐵) = (𝐵𝐿𝐴))
117116adantr 481 . . . . . . 7 (((𝜑𝐴𝐵) ∧ ((𝐵𝐿𝑞)(⟂G‘𝐺)(𝐵𝐿𝐴) ∧ ∃𝑠𝑃 ((𝑠 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴) ∧ 𝑠 ∈ (𝐴𝐼𝑞)))) → (𝐴𝐿𝐵) = (𝐵𝐿𝐴))
118115, 117breqtrrd 4990 . . . . . 6 (((𝜑𝐴𝐵) ∧ ((𝐵𝐿𝑞)(⟂G‘𝐺)(𝐵𝐿𝐴) ∧ ∃𝑠𝑃 ((𝑠 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴) ∧ 𝑠 ∈ (𝐴𝐼𝑞)))) → (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵))
119118ex 413 . . . . 5 ((𝜑𝐴𝐵) → (((𝐵𝐿𝑞)(⟂G‘𝐺)(𝐵𝐿𝐴) ∧ ∃𝑠𝑃 ((𝑠 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴) ∧ 𝑠 ∈ (𝐴𝐼𝑞))) → (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)))
120119reximdv 3236 . . . 4 ((𝜑𝐴𝐵) → (∃𝑞𝑃 ((𝐵𝐿𝑞)(⟂G‘𝐺)(𝐵𝐿𝐴) ∧ ∃𝑠𝑃 ((𝑠 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴) ∧ 𝑠 ∈ (𝐴𝐼𝑞))) → ∃𝑞𝑃 (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵)))
121114, 120mpd 15 . . 3 ((𝜑𝐴𝐵) → ∃𝑞𝑃 (𝐵𝐿𝑞)(⟂G‘𝐺)(𝐴𝐿𝐵))
122107, 121r19.29a 3252 . 2 ((𝜑𝐴𝐵) → ∃𝑥𝑃 𝐵 = ((𝑆𝑥)‘𝐴))
12317, 122pm2.61dane 3072 1 (𝜑 → ∃𝑥𝑃 𝐵 = ((𝑆𝑥)‘𝐴))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ wo 842   = wceq 1522   ∈ wcel 2081   ≠ wne 2984  ∃wrex 3106   class class class wbr 4962  ran crn 5444  ‘cfv 6225  (class class class)co 7016  2c2 11540  Basecbs 16312  distcds 16403  TarskiGcstrkg 25898  DimTarskiG≥cstrkgld 25902  Itvcitv 25904  LineGclng 25905  ≤Gcleg 26050  pInvGcmir 26120  ⟂Gcperpg 26163 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-cnex 10439  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459  ax-pre-mulgt0 10460 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-om 7437  df-1st 7545  df-2nd 7546  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-1o 7953  df-oadd 7957  df-er 8139  df-map 8258  df-pm 8259  df-en 8358  df-dom 8359  df-sdom 8360  df-fin 8361  df-dju 9176  df-card 9214  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527  df-sub 10719  df-neg 10720  df-nn 11487  df-2 11548  df-3 11549  df-n0 11746  df-xnn0 11816  df-z 11830  df-uz 12094  df-fz 12743  df-fzo 12884  df-hash 13541  df-word 13708  df-concat 13769  df-s1 13794  df-s2 14046  df-s3 14047  df-trkgc 25916  df-trkgb 25917  df-trkgcb 25918  df-trkgld 25920  df-trkg 25921  df-cgrg 25979  df-leg 26051  df-mir 26121  df-rag 26162  df-perpg 26164 This theorem is referenced by:  mideu  26206  opphllem5  26219  opphl  26222
 Copyright terms: Public domain W3C validator