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

Theorem mirbtwn 26447
Description: Property of the image by the point inversion function. Definition 7.5 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 3-Jun-2019.)
Hypotheses
Ref Expression
mirval.p 𝑃 = (Base‘𝐺)
mirval.d = (dist‘𝐺)
mirval.i 𝐼 = (Itv‘𝐺)
mirval.l 𝐿 = (LineG‘𝐺)
mirval.s 𝑆 = (pInvG‘𝐺)
mirval.g (𝜑𝐺 ∈ TarskiG)
mirval.a (𝜑𝐴𝑃)
mirfv.m 𝑀 = (𝑆𝐴)
mirfv.b (𝜑𝐵𝑃)
Assertion
Ref Expression
mirbtwn (𝜑𝐴 ∈ ((𝑀𝐵)𝐼𝐵))

Proof of Theorem mirbtwn
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 mirval.p . . . . 5 𝑃 = (Base‘𝐺)
2 mirval.d . . . . 5 = (dist‘𝐺)
3 mirval.i . . . . 5 𝐼 = (Itv‘𝐺)
4 mirval.l . . . . 5 𝐿 = (LineG‘𝐺)
5 mirval.s . . . . 5 𝑆 = (pInvG‘𝐺)
6 mirval.g . . . . 5 (𝜑𝐺 ∈ TarskiG)
7 mirval.a . . . . 5 (𝜑𝐴𝑃)
8 mirfv.m . . . . 5 𝑀 = (𝑆𝐴)
9 mirfv.b . . . . 5 (𝜑𝐵𝑃)
101, 2, 3, 4, 5, 6, 7, 8, 9mirfv 26445 . . . 4 (𝜑 → (𝑀𝐵) = (𝑧𝑃 ((𝐴 𝑧) = (𝐴 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))))
111, 2, 3, 6, 9, 7mirreu3 26443 . . . . 5 (𝜑 → ∃!𝑧𝑃 ((𝐴 𝑧) = (𝐴 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵)))
12 riotacl2 7133 . . . . 5 (∃!𝑧𝑃 ((𝐴 𝑧) = (𝐴 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵)) → (𝑧𝑃 ((𝐴 𝑧) = (𝐴 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))) ∈ {𝑧𝑃 ∣ ((𝐴 𝑧) = (𝐴 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))})
1311, 12syl 17 . . . 4 (𝜑 → (𝑧𝑃 ((𝐴 𝑧) = (𝐴 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))) ∈ {𝑧𝑃 ∣ ((𝐴 𝑧) = (𝐴 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))})
1410, 13eqeltrd 2916 . . 3 (𝜑 → (𝑀𝐵) ∈ {𝑧𝑃 ∣ ((𝐴 𝑧) = (𝐴 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))})
15 oveq2 7167 . . . . . 6 (𝑧 = (𝑀𝐵) → (𝐴 𝑧) = (𝐴 (𝑀𝐵)))
1615eqeq1d 2826 . . . . 5 (𝑧 = (𝑀𝐵) → ((𝐴 𝑧) = (𝐴 𝐵) ↔ (𝐴 (𝑀𝐵)) = (𝐴 𝐵)))
17 oveq1 7166 . . . . . 6 (𝑧 = (𝑀𝐵) → (𝑧𝐼𝐵) = ((𝑀𝐵)𝐼𝐵))
1817eleq2d 2901 . . . . 5 (𝑧 = (𝑀𝐵) → (𝐴 ∈ (𝑧𝐼𝐵) ↔ 𝐴 ∈ ((𝑀𝐵)𝐼𝐵)))
1916, 18anbi12d 632 . . . 4 (𝑧 = (𝑀𝐵) → (((𝐴 𝑧) = (𝐴 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵)) ↔ ((𝐴 (𝑀𝐵)) = (𝐴 𝐵) ∧ 𝐴 ∈ ((𝑀𝐵)𝐼𝐵))))
2019elrab 3683 . . 3 ((𝑀𝐵) ∈ {𝑧𝑃 ∣ ((𝐴 𝑧) = (𝐴 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))} ↔ ((𝑀𝐵) ∈ 𝑃 ∧ ((𝐴 (𝑀𝐵)) = (𝐴 𝐵) ∧ 𝐴 ∈ ((𝑀𝐵)𝐼𝐵))))
2114, 20sylib 220 . 2 (𝜑 → ((𝑀𝐵) ∈ 𝑃 ∧ ((𝐴 (𝑀𝐵)) = (𝐴 𝐵) ∧ 𝐴 ∈ ((𝑀𝐵)𝐼𝐵))))
2221simprrd 772 1 (𝜑𝐴 ∈ ((𝑀𝐵)𝐼𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398   = wceq 1536  wcel 2113  ∃!wreu 3143  {crab 3145  cfv 6358  crio 7116  (class class class)co 7159  Basecbs 16486  distcds 16577  TarskiGcstrkg 26219  Itvcitv 26225  LineGclng 26226  pInvGcmir 26441
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pr 5333
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-reu 3148  df-rmo 3149  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-iun 4924  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-riota 7117  df-ov 7162  df-trkgc 26237  df-trkgb 26238  df-trkgcb 26239  df-trkg 26242  df-mir 26442
This theorem is referenced by:  mirmir  26451  mirinv  26455  miriso  26459  mirmir2  26463  mirln  26465  mirln2  26466  mirconn  26467  mirhl2  26470  mircgrextend  26471  mirtrcgr  26472  mirauto  26473  miduniq  26474  krippenlem  26479  ragflat  26493  ragcgr  26496  footexALT  26507  footexlem1  26508  footexlem2  26509  colperpexlem1  26519  colperpexlem3  26521  mideulem2  26523  opphllem  26524  opphllem1  26536  opphllem2  26537  opphllem4  26539  colhp  26559  midbtwn  26568  lmieu  26573  lmiisolem  26585
  Copyright terms: Public domain W3C validator