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

Theorem lmieu 26497
Description: Uniqueness of the line mirror point. Theorem 10.2 of [Schwabhauser] p. 88. (Contributed by Thierry Arnoux, 1-Dec-2019.)
Hypotheses
Ref Expression
ismid.p 𝑃 = (Base‘𝐺)
ismid.d = (dist‘𝐺)
ismid.i 𝐼 = (Itv‘𝐺)
ismid.g (𝜑𝐺 ∈ TarskiG)
ismid.1 (𝜑𝐺DimTarskiG≥2)
lmieu.l 𝐿 = (LineG‘𝐺)
lmieu.1 (𝜑𝐷 ∈ ran 𝐿)
lmieu.a (𝜑𝐴𝑃)
Assertion
Ref Expression
lmieu (𝜑 → ∃!𝑏𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)))
Distinct variable groups:   𝐺,𝑏   𝑃,𝑏   𝜑,𝑏   𝐴,𝑏   𝐷,𝑏   𝐿,𝑏
Allowed substitution hints:   𝐼(𝑏)   (𝑏)

Proof of Theorem lmieu
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 lmieu.a . . . 4 (𝜑𝐴𝑃)
21adantr 481 . . 3 ((𝜑𝐴𝐷) → 𝐴𝑃)
3 simpr 485 . . . . . . . . . . . 12 (((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) → ¬ 𝐴 = 𝑏)
4 eqidd 2819 . . . . . . . . . . . . . . 15 (((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) → (𝐴(midG‘𝐺)𝑏) = (𝐴(midG‘𝐺)𝑏))
5 ismid.p . . . . . . . . . . . . . . . 16 𝑃 = (Base‘𝐺)
6 ismid.d . . . . . . . . . . . . . . . 16 = (dist‘𝐺)
7 ismid.i . . . . . . . . . . . . . . . 16 𝐼 = (Itv‘𝐺)
8 ismid.g . . . . . . . . . . . . . . . . 17 (𝜑𝐺 ∈ TarskiG)
98ad4antr 728 . . . . . . . . . . . . . . . 16 (((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) → 𝐺 ∈ TarskiG)
10 ismid.1 . . . . . . . . . . . . . . . . 17 (𝜑𝐺DimTarskiG≥2)
1110ad4antr 728 . . . . . . . . . . . . . . . 16 (((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) → 𝐺DimTarskiG≥2)
122ad3antrrr 726 . . . . . . . . . . . . . . . 16 (((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) → 𝐴𝑃)
13 simpllr 772 . . . . . . . . . . . . . . . 16 (((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) → 𝑏𝑃)
14 eqid 2818 . . . . . . . . . . . . . . . 16 (pInvG‘𝐺) = (pInvG‘𝐺)
155, 6, 7, 9, 11, 12, 13midcl 26490 . . . . . . . . . . . . . . . 16 (((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) → (𝐴(midG‘𝐺)𝑏) ∈ 𝑃)
165, 6, 7, 9, 11, 12, 13, 14, 15ismidb 26491 . . . . . . . . . . . . . . 15 (((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) → (𝑏 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝑏))‘𝐴) ↔ (𝐴(midG‘𝐺)𝑏) = (𝐴(midG‘𝐺)𝑏)))
174, 16mpbird 258 . . . . . . . . . . . . . 14 (((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) → 𝑏 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝑏))‘𝐴))
1817adantr 481 . . . . . . . . . . . . 13 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷 ≠ (𝐴𝐿𝑏)) → 𝑏 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝑏))‘𝐴))
19 lmieu.l . . . . . . . . . . . . . . . 16 𝐿 = (LineG‘𝐺)
209adantr 481 . . . . . . . . . . . . . . . 16 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷 ≠ (𝐴𝐿𝑏)) → 𝐺 ∈ TarskiG)
21 lmieu.1 . . . . . . . . . . . . . . . . . 18 (𝜑𝐷 ∈ ran 𝐿)
2221ad4antr 728 . . . . . . . . . . . . . . . . 17 (((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) → 𝐷 ∈ ran 𝐿)
2322adantr 481 . . . . . . . . . . . . . . . 16 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷 ≠ (𝐴𝐿𝑏)) → 𝐷 ∈ ran 𝐿)
2412adantr 481 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷 ≠ (𝐴𝐿𝑏)) → 𝐴𝑃)
2513adantr 481 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷 ≠ (𝐴𝐿𝑏)) → 𝑏𝑃)
263neqned 3020 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) → 𝐴𝑏)
2726adantr 481 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷 ≠ (𝐴𝐿𝑏)) → 𝐴𝑏)
285, 7, 19, 20, 24, 25, 27tgelrnln 26343 . . . . . . . . . . . . . . . 16 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷 ≠ (𝐴𝐿𝑏)) → (𝐴𝐿𝑏) ∈ ran 𝐿)
29 simpr 485 . . . . . . . . . . . . . . . 16 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷 ≠ (𝐴𝐿𝑏)) → 𝐷 ≠ (𝐴𝐿𝑏))
30 simp-4r 780 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) → 𝐴𝐷)
3130adantr 481 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷 ≠ (𝐴𝐿𝑏)) → 𝐴𝐷)
325, 7, 19, 20, 24, 25, 27tglinerflx1 26346 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷 ≠ (𝐴𝐿𝑏)) → 𝐴 ∈ (𝐴𝐿𝑏))
3331, 32elind 4168 . . . . . . . . . . . . . . . 16 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷 ≠ (𝐴𝐿𝑏)) → 𝐴 ∈ (𝐷 ∩ (𝐴𝐿𝑏)))
34 simpllr 772 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷 ≠ (𝐴𝐿𝑏)) → (𝐴(midG‘𝐺)𝑏) ∈ 𝐷)
355, 6, 7, 9, 11, 12, 13midbtwn 26492 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) → (𝐴(midG‘𝐺)𝑏) ∈ (𝐴𝐼𝑏))
365, 7, 19, 9, 12, 13, 15, 26, 35btwnlng1 26332 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) → (𝐴(midG‘𝐺)𝑏) ∈ (𝐴𝐿𝑏))
3736adantr 481 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷 ≠ (𝐴𝐿𝑏)) → (𝐴(midG‘𝐺)𝑏) ∈ (𝐴𝐿𝑏))
3834, 37elind 4168 . . . . . . . . . . . . . . . 16 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷 ≠ (𝐴𝐿𝑏)) → (𝐴(midG‘𝐺)𝑏) ∈ (𝐷 ∩ (𝐴𝐿𝑏)))
395, 7, 19, 20, 23, 28, 29, 33, 38tglineineq 26356 . . . . . . . . . . . . . . 15 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷 ≠ (𝐴𝐿𝑏)) → 𝐴 = (𝐴(midG‘𝐺)𝑏))
4039fveq2d 6667 . . . . . . . . . . . . . 14 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷 ≠ (𝐴𝐿𝑏)) → ((pInvG‘𝐺)‘𝐴) = ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝑏)))
4140fveq1d 6665 . . . . . . . . . . . . 13 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷 ≠ (𝐴𝐿𝑏)) → (((pInvG‘𝐺)‘𝐴)‘𝐴) = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝑏))‘𝐴))
42 eqid 2818 . . . . . . . . . . . . . 14 ((pInvG‘𝐺)‘𝐴) = ((pInvG‘𝐺)‘𝐴)
435, 6, 7, 19, 14, 20, 24, 42mircinv 26381 . . . . . . . . . . . . 13 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷 ≠ (𝐴𝐿𝑏)) → (((pInvG‘𝐺)‘𝐴)‘𝐴) = 𝐴)
4418, 41, 433eqtr2rd 2860 . . . . . . . . . . . 12 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷 ≠ (𝐴𝐿𝑏)) → 𝐴 = 𝑏)
453, 44mtand 812 . . . . . . . . . . 11 (((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) → ¬ 𝐷 ≠ (𝐴𝐿𝑏))
468ad5antr 730 . . . . . . . . . . . 12 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷(⟂G‘𝐺)(𝐴𝐿𝑏)) → 𝐺 ∈ TarskiG)
4721ad5antr 730 . . . . . . . . . . . 12 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷(⟂G‘𝐺)(𝐴𝐿𝑏)) → 𝐷 ∈ ran 𝐿)
48 nne 3017 . . . . . . . . . . . . . . 15 𝐷 ≠ (𝐴𝐿𝑏) ↔ 𝐷 = (𝐴𝐿𝑏))
4945, 48sylib 219 . . . . . . . . . . . . . 14 (((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) → 𝐷 = (𝐴𝐿𝑏))
5049adantr 481 . . . . . . . . . . . . 13 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷(⟂G‘𝐺)(𝐴𝐿𝑏)) → 𝐷 = (𝐴𝐿𝑏))
5150, 47eqeltrrd 2911 . . . . . . . . . . . 12 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷(⟂G‘𝐺)(𝐴𝐿𝑏)) → (𝐴𝐿𝑏) ∈ ran 𝐿)
52 simpr 485 . . . . . . . . . . . 12 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷(⟂G‘𝐺)(𝐴𝐿𝑏)) → 𝐷(⟂G‘𝐺)(𝐴𝐿𝑏))
535, 6, 7, 19, 46, 47, 51, 52perpneq 26427 . . . . . . . . . . 11 ((((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) ∧ 𝐷(⟂G‘𝐺)(𝐴𝐿𝑏)) → 𝐷 ≠ (𝐴𝐿𝑏))
5445, 53mtand 812 . . . . . . . . . 10 (((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) ∧ ¬ 𝐴 = 𝑏) → ¬ 𝐷(⟂G‘𝐺)(𝐴𝐿𝑏))
5554ex 413 . . . . . . . . 9 ((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) → (¬ 𝐴 = 𝑏 → ¬ 𝐷(⟂G‘𝐺)(𝐴𝐿𝑏)))
5655con4d 115 . . . . . . . 8 ((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) → (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) → 𝐴 = 𝑏))
57 idd 24 . . . . . . . 8 ((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) → (𝐴 = 𝑏𝐴 = 𝑏))
5856, 57jaod 853 . . . . . . 7 ((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ (𝐴(midG‘𝐺)𝑏) ∈ 𝐷) → ((𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏) → 𝐴 = 𝑏))
5958impr 455 . . . . . 6 ((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → 𝐴 = 𝑏)
6059eqcomd 2824 . . . . 5 ((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → 𝑏 = 𝐴)
61 simpr 485 . . . . . . . . 9 ((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = 𝐴) → 𝑏 = 𝐴)
6261oveq2d 7161 . . . . . . . 8 ((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = 𝐴) → (𝐴(midG‘𝐺)𝑏) = (𝐴(midG‘𝐺)𝐴))
635, 6, 7, 8, 10, 1, 1midid 26494 . . . . . . . . 9 (𝜑 → (𝐴(midG‘𝐺)𝐴) = 𝐴)
6463ad3antrrr 726 . . . . . . . 8 ((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = 𝐴) → (𝐴(midG‘𝐺)𝐴) = 𝐴)
6562, 64eqtrd 2853 . . . . . . 7 ((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = 𝐴) → (𝐴(midG‘𝐺)𝑏) = 𝐴)
66 simpllr 772 . . . . . . 7 ((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = 𝐴) → 𝐴𝐷)
6765, 66eqeltrd 2910 . . . . . 6 ((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = 𝐴) → (𝐴(midG‘𝐺)𝑏) ∈ 𝐷)
6861eqcomd 2824 . . . . . . 7 ((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = 𝐴) → 𝐴 = 𝑏)
6968olcd 870 . . . . . 6 ((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = 𝐴) → (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))
7067, 69jca 512 . . . . 5 ((((𝜑𝐴𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = 𝐴) → ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)))
7160, 70impbida 797 . . . 4 (((𝜑𝐴𝐷) ∧ 𝑏𝑃) → (((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)) ↔ 𝑏 = 𝐴))
7271ralrimiva 3179 . . 3 ((𝜑𝐴𝐷) → ∀𝑏𝑃 (((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)) ↔ 𝑏 = 𝐴))
73 reu6i 3716 . . 3 ((𝐴𝑃 ∧ ∀𝑏𝑃 (((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)) ↔ 𝑏 = 𝐴)) → ∃!𝑏𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)))
742, 72, 73syl2anc 584 . 2 ((𝜑𝐴𝐷) → ∃!𝑏𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)))
758adantr 481 . . . . . 6 ((𝜑 ∧ ¬ 𝐴𝐷) → 𝐺 ∈ TarskiG)
7675ad2antrr 722 . . . . 5 ((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) → 𝐺 ∈ TarskiG)
7721adantr 481 . . . . . . 7 ((𝜑 ∧ ¬ 𝐴𝐷) → 𝐷 ∈ ran 𝐿)
7877ad2antrr 722 . . . . . 6 ((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) → 𝐷 ∈ ran 𝐿)
79 simplr 765 . . . . . 6 ((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) → 𝑥𝐷)
805, 19, 7, 76, 78, 79tglnpt 26262 . . . . 5 ((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) → 𝑥𝑃)
81 eqid 2818 . . . . 5 ((pInvG‘𝐺)‘𝑥) = ((pInvG‘𝐺)‘𝑥)
821adantr 481 . . . . . 6 ((𝜑 ∧ ¬ 𝐴𝐷) → 𝐴𝑃)
8382ad2antrr 722 . . . . 5 ((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) → 𝐴𝑃)
845, 6, 7, 19, 14, 76, 80, 81, 83mircl 26374 . . . 4 ((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) → (((pInvG‘𝐺)‘𝑥)‘𝐴) ∈ 𝑃)
85 oveq2 7153 . . . . . . . . . 10 (𝑥 = (𝐴(midG‘𝐺)𝑏) → (𝐴𝐿𝑥) = (𝐴𝐿(𝐴(midG‘𝐺)𝑏)))
8685breq1d 5067 . . . . . . . . 9 (𝑥 = (𝐴(midG‘𝐺)𝑏) → ((𝐴𝐿𝑥)(⟂G‘𝐺)𝐷 ↔ (𝐴𝐿(𝐴(midG‘𝐺)𝑏))(⟂G‘𝐺)𝐷))
87 simprl 767 . . . . . . . . 9 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → (𝐴(midG‘𝐺)𝑏) ∈ 𝐷)
88 simpr 485 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐴𝐷) → ¬ 𝐴𝐷)
895, 6, 7, 19, 75, 77, 82, 88foot 26435 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝐴𝐷) → ∃!𝑥𝐷 (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷)
90 reurmo 3431 . . . . . . . . . . 11 (∃!𝑥𝐷 (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷 → ∃*𝑥𝐷 (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷)
9189, 90syl 17 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐴𝐷) → ∃*𝑥𝐷 (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷)
9291ad4antr 728 . . . . . . . . 9 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → ∃*𝑥𝐷 (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷)
9379ad2antrr 722 . . . . . . . . 9 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → 𝑥𝐷)
94 simpllr 772 . . . . . . . . 9 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷)
9576ad2antrr 722 . . . . . . . . . . 11 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → 𝐺 ∈ TarskiG)
9683ad2antrr 722 . . . . . . . . . . 11 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → 𝐴𝑃)
97 simplr 765 . . . . . . . . . . 11 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → 𝑏𝑃)
9810ad5antr 730 . . . . . . . . . . . . 13 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → 𝐺DimTarskiG≥2)
995, 6, 7, 95, 98, 96, 97midcl 26490 . . . . . . . . . . . 12 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → (𝐴(midG‘𝐺)𝑏) ∈ 𝑃)
1005, 6, 7, 95, 98, 96, 97midbtwn 26492 . . . . . . . . . . . 12 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → (𝐴(midG‘𝐺)𝑏) ∈ (𝐴𝐼𝑏))
10188ad4antr 728 . . . . . . . . . . . . 13 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → ¬ 𝐴𝐷)
102 nelne2 3112 . . . . . . . . . . . . 13 (((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ ¬ 𝐴𝐷) → (𝐴(midG‘𝐺)𝑏) ≠ 𝐴)
10387, 101, 102syl2anc 584 . . . . . . . . . . . 12 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → (𝐴(midG‘𝐺)𝑏) ≠ 𝐴)
1045, 6, 7, 95, 96, 99, 97, 100, 103tgbtwnne 26203 . . . . . . . . . . 11 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → 𝐴𝑏)
1055, 7, 19, 95, 96, 97, 99, 104, 100btwnlng1 26332 . . . . . . . . . . 11 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → (𝐴(midG‘𝐺)𝑏) ∈ (𝐴𝐿𝑏))
1065, 7, 19, 95, 96, 97, 104, 99, 103, 105tglineelsb2 26345 . . . . . . . . . 10 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → (𝐴𝐿𝑏) = (𝐴𝐿(𝐴(midG‘𝐺)𝑏)))
10778ad2antrr 722 . . . . . . . . . . 11 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → 𝐷 ∈ ran 𝐿)
1085, 7, 19, 95, 96, 97, 104tgelrnln 26343 . . . . . . . . . . 11 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → (𝐴𝐿𝑏) ∈ ran 𝐿)
109104neneqd 3018 . . . . . . . . . . . 12 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → ¬ 𝐴 = 𝑏)
110 simprr 769 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))
111110orcomd 865 . . . . . . . . . . . . 13 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → (𝐴 = 𝑏𝐷(⟂G‘𝐺)(𝐴𝐿𝑏)))
112111ord 858 . . . . . . . . . . . 12 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → (¬ 𝐴 = 𝑏𝐷(⟂G‘𝐺)(𝐴𝐿𝑏)))
113109, 112mpd 15 . . . . . . . . . . 11 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → 𝐷(⟂G‘𝐺)(𝐴𝐿𝑏))
1145, 6, 7, 19, 95, 107, 108, 113perpcom 26426 . . . . . . . . . 10 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → (𝐴𝐿𝑏)(⟂G‘𝐺)𝐷)
115106, 114eqbrtrrd 5081 . . . . . . . . 9 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → (𝐴𝐿(𝐴(midG‘𝐺)𝑏))(⟂G‘𝐺)𝐷)
11686, 87, 92, 93, 94, 115rmoi2 3874 . . . . . . . 8 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → 𝑥 = (𝐴(midG‘𝐺)𝑏))
117116eqcomd 2824 . . . . . . 7 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → (𝐴(midG‘𝐺)𝑏) = 𝑥)
11880ad2antrr 722 . . . . . . . 8 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → 𝑥𝑃)
1195, 6, 7, 95, 98, 96, 97, 14, 118ismidb 26491 . . . . . . 7 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → (𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴) ↔ (𝐴(midG‘𝐺)𝑏) = 𝑥))
120117, 119mpbird 258 . . . . . 6 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) → 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴))
121 simpr 485 . . . . . . . . 9 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) → 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴))
12276ad2antrr 722 . . . . . . . . . 10 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) → 𝐺 ∈ TarskiG)
12310ad5antr 730 . . . . . . . . . 10 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) → 𝐺DimTarskiG≥2)
12483ad2antrr 722 . . . . . . . . . 10 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) → 𝐴𝑃)
125 simplr 765 . . . . . . . . . 10 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) → 𝑏𝑃)
12680ad2antrr 722 . . . . . . . . . 10 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) → 𝑥𝑃)
1275, 6, 7, 122, 123, 124, 125, 14, 126ismidb 26491 . . . . . . . . 9 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) → (𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴) ↔ (𝐴(midG‘𝐺)𝑏) = 𝑥))
128121, 127mpbid 233 . . . . . . . 8 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) → (𝐴(midG‘𝐺)𝑏) = 𝑥)
12979ad2antrr 722 . . . . . . . 8 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) → 𝑥𝐷)
130128, 129eqeltrd 2910 . . . . . . 7 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) → (𝐴(midG‘𝐺)𝑏) ∈ 𝐷)
131122adantr 481 . . . . . . . . . . . 12 (((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) ∧ 𝐴𝑏) → 𝐺 ∈ TarskiG)
132 simp-4r 780 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) ∧ 𝐴𝑏) → (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷)
13319, 131, 132perpln1 26423 . . . . . . . . . . . 12 (((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) ∧ 𝐴𝑏) → (𝐴𝐿𝑥) ∈ ran 𝐿)
13478ad3antrrr 726 . . . . . . . . . . . 12 (((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) ∧ 𝐴𝑏) → 𝐷 ∈ ran 𝐿)
1355, 6, 7, 19, 131, 133, 134, 132perpcom 26426 . . . . . . . . . . 11 (((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) ∧ 𝐴𝑏) → 𝐷(⟂G‘𝐺)(𝐴𝐿𝑥))
136124adantr 481 . . . . . . . . . . . 12 (((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) ∧ 𝐴𝑏) → 𝐴𝑃)
137126adantr 481 . . . . . . . . . . . 12 (((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) ∧ 𝐴𝑏) → 𝑥𝑃)
1385, 7, 19, 131, 136, 137, 133tglnne 26341 . . . . . . . . . . . 12 (((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) ∧ 𝐴𝑏) → 𝐴𝑥)
139 simpllr 772 . . . . . . . . . . . 12 (((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) ∧ 𝐴𝑏) → 𝑏𝑃)
140 simpr 485 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) ∧ 𝐴𝑏) → 𝐴𝑏)
141140necomd 3068 . . . . . . . . . . . 12 (((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) ∧ 𝐴𝑏) → 𝑏𝐴)
1425, 6, 7, 19, 14, 131, 137, 81, 136mirbtwn 26371 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) ∧ 𝐴𝑏) → 𝑥 ∈ ((((pInvG‘𝐺)‘𝑥)‘𝐴)𝐼𝐴))
143 simplr 765 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) ∧ 𝐴𝑏) → 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴))
144143oveq1d 7160 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) ∧ 𝐴𝑏) → (𝑏𝐼𝐴) = ((((pInvG‘𝐺)‘𝑥)‘𝐴)𝐼𝐴))
145142, 144eleqtrrd 2913 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) ∧ 𝐴𝑏) → 𝑥 ∈ (𝑏𝐼𝐴))
1465, 7, 19, 131, 139, 136, 137, 141, 145btwnlng1 26332 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) ∧ 𝐴𝑏) → 𝑥 ∈ (𝑏𝐿𝐴))
1475, 7, 19, 131, 136, 137, 139, 138, 146, 141lnrot1 26336 . . . . . . . . . . . 12 (((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) ∧ 𝐴𝑏) → 𝑏 ∈ (𝐴𝐿𝑥))
1485, 7, 19, 131, 136, 137, 138, 139, 141, 147tglineelsb2 26345 . . . . . . . . . . 11 (((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) ∧ 𝐴𝑏) → (𝐴𝐿𝑥) = (𝐴𝐿𝑏))
149135, 148breqtrd 5083 . . . . . . . . . 10 (((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) ∧ 𝐴𝑏) → 𝐷(⟂G‘𝐺)(𝐴𝐿𝑏))
150149ex 413 . . . . . . . . 9 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) → (𝐴𝑏𝐷(⟂G‘𝐺)(𝐴𝐿𝑏)))
151150necon1bd 3031 . . . . . . . 8 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) → (¬ 𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) → 𝐴 = 𝑏))
152151orrd 857 . . . . . . 7 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) → (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))
153130, 152jca 512 . . . . . 6 ((((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) ∧ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)) → ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)))
154120, 153impbida 797 . . . . 5 (((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) ∧ 𝑏𝑃) → (((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)) ↔ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)))
155154ralrimiva 3179 . . . 4 ((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) → ∀𝑏𝑃 (((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)) ↔ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴)))
156 reu6i 3716 . . . 4 (((((pInvG‘𝐺)‘𝑥)‘𝐴) ∈ 𝑃 ∧ ∀𝑏𝑃 (((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)) ↔ 𝑏 = (((pInvG‘𝐺)‘𝑥)‘𝐴))) → ∃!𝑏𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)))
15784, 155, 156syl2anc 584 . . 3 ((((𝜑 ∧ ¬ 𝐴𝐷) ∧ 𝑥𝐷) ∧ (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷) → ∃!𝑏𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)))
1585, 6, 7, 19, 75, 77, 82, 88footex 26434 . . 3 ((𝜑 ∧ ¬ 𝐴𝐷) → ∃𝑥𝐷 (𝐴𝐿𝑥)(⟂G‘𝐺)𝐷)
159157, 158r19.29a 3286 . 2 ((𝜑 ∧ ¬ 𝐴𝐷) → ∃!𝑏𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)))
16074, 159pm2.61dan 809 1 (𝜑 → ∃!𝑏𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841   = wceq 1528  wcel 2105  wne 3013  wral 3135  ∃!wreu 3137  ∃*wrmo 3138   class class class wbr 5057  ran crn 5549  cfv 6348  (class class class)co 7145  2c2 11680  Basecbs 16471  distcds 16562  TarskiGcstrkg 26143  DimTarskiGcstrkgld 26147  Itvcitv 26149  LineGclng 26150  pInvGcmir 26365  ⟂Gcperpg 26408  midGcmid 26485
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-oadd 8095  df-er 8278  df-map 8397  df-pm 8398  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-dju 9318  df-card 9356  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-nn 11627  df-2 11688  df-3 11689  df-n0 11886  df-xnn0 11956  df-z 11970  df-uz 12232  df-fz 12881  df-fzo 13022  df-hash 13679  df-word 13850  df-concat 13911  df-s1 13938  df-s2 14198  df-s3 14199  df-trkgc 26161  df-trkgb 26162  df-trkgcb 26163  df-trkgld 26165  df-trkg 26166  df-cgrg 26224  df-leg 26296  df-mir 26366  df-rag 26407  df-perpg 26409  df-mid 26487
This theorem is referenced by:  lmif  26498  islmib  26500
  Copyright terms: Public domain W3C validator