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

Theorem mirreu3 27638
Description: Existential uniqueness of the mirror point. Theorem 7.8 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 30-May-2019.)
Hypotheses
Ref Expression
mirreu.p 𝑃 = (Baseβ€˜πΊ)
mirreu.d βˆ’ = (distβ€˜πΊ)
mirreu.i 𝐼 = (Itvβ€˜πΊ)
mirreu.g (πœ‘ β†’ 𝐺 ∈ TarskiG)
mirreu.a (πœ‘ β†’ 𝐴 ∈ 𝑃)
mirreu.m (πœ‘ β†’ 𝑀 ∈ 𝑃)
Assertion
Ref Expression
mirreu3 (πœ‘ β†’ βˆƒ!𝑏 ∈ 𝑃 ((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)))
Distinct variable groups:   βˆ’ ,𝑏   𝐴,𝑏   𝐼,𝑏   𝑀,𝑏   𝑃,𝑏   πœ‘,𝑏
Allowed substitution hint:   𝐺(𝑏)

Proof of Theorem mirreu3
Dummy variable 𝑐 is distinct from all other variables.
StepHypRef Expression
1 mirreu.a . . . . . 6 (πœ‘ β†’ 𝐴 ∈ 𝑃)
21adantr 482 . . . . 5 ((πœ‘ ∧ 𝐴 = 𝑀) β†’ 𝐴 ∈ 𝑃)
3 eqidd 2734 . . . . 5 ((πœ‘ ∧ 𝐴 = 𝑀) β†’ (𝑀 βˆ’ 𝐴) = (𝑀 βˆ’ 𝐴))
4 simpr 486 . . . . . 6 ((πœ‘ ∧ 𝐴 = 𝑀) β†’ 𝐴 = 𝑀)
5 mirreu.p . . . . . . 7 𝑃 = (Baseβ€˜πΊ)
6 mirreu.d . . . . . . 7 βˆ’ = (distβ€˜πΊ)
7 mirreu.i . . . . . . 7 𝐼 = (Itvβ€˜πΊ)
8 mirreu.g . . . . . . . 8 (πœ‘ β†’ 𝐺 ∈ TarskiG)
98adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝐴 = 𝑀) β†’ 𝐺 ∈ TarskiG)
105, 6, 7, 9, 2, 2tgbtwntriv2 27471 . . . . . 6 ((πœ‘ ∧ 𝐴 = 𝑀) β†’ 𝐴 ∈ (𝐴𝐼𝐴))
114, 10eqeltrrd 2835 . . . . 5 ((πœ‘ ∧ 𝐴 = 𝑀) β†’ 𝑀 ∈ (𝐴𝐼𝐴))
12 oveq2 7366 . . . . . . . 8 (𝑏 = 𝐴 β†’ (𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴))
1312eqeq1d 2735 . . . . . . 7 (𝑏 = 𝐴 β†’ ((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ↔ (𝑀 βˆ’ 𝐴) = (𝑀 βˆ’ 𝐴)))
14 oveq1 7365 . . . . . . . 8 (𝑏 = 𝐴 β†’ (𝑏𝐼𝐴) = (𝐴𝐼𝐴))
1514eleq2d 2820 . . . . . . 7 (𝑏 = 𝐴 β†’ (𝑀 ∈ (𝑏𝐼𝐴) ↔ 𝑀 ∈ (𝐴𝐼𝐴)))
1613, 15anbi12d 632 . . . . . 6 (𝑏 = 𝐴 β†’ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ↔ ((𝑀 βˆ’ 𝐴) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝐴𝐼𝐴))))
1716rspcev 3580 . . . . 5 ((𝐴 ∈ 𝑃 ∧ ((𝑀 βˆ’ 𝐴) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝐴𝐼𝐴))) β†’ βˆƒπ‘ ∈ 𝑃 ((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)))
182, 3, 11, 17syl12anc 836 . . . 4 ((πœ‘ ∧ 𝐴 = 𝑀) β†’ βˆƒπ‘ ∈ 𝑃 ((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)))
198ad3antrrr 729 . . . . . . . 8 ((((πœ‘ ∧ 𝐴 = 𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ 𝐺 ∈ TarskiG)
20 mirreu.m . . . . . . . . 9 (πœ‘ β†’ 𝑀 ∈ 𝑃)
2120ad3antrrr 729 . . . . . . . 8 ((((πœ‘ ∧ 𝐴 = 𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ 𝑀 ∈ 𝑃)
22 simplrl 776 . . . . . . . 8 ((((πœ‘ ∧ 𝐴 = 𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ 𝑏 ∈ 𝑃)
23 simprll 778 . . . . . . . . 9 ((((πœ‘ ∧ 𝐴 = 𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ (𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴))
24 simpllr 775 . . . . . . . . . 10 ((((πœ‘ ∧ 𝐴 = 𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ 𝐴 = 𝑀)
2524oveq2d 7374 . . . . . . . . 9 ((((πœ‘ ∧ 𝐴 = 𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ (𝑀 βˆ’ 𝐴) = (𝑀 βˆ’ 𝑀))
2623, 25eqtrd 2773 . . . . . . . 8 ((((πœ‘ ∧ 𝐴 = 𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ (𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝑀))
275, 6, 7, 19, 21, 22, 21, 26axtgcgrid 27447 . . . . . . 7 ((((πœ‘ ∧ 𝐴 = 𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ 𝑀 = 𝑏)
28 simplrr 777 . . . . . . . 8 ((((πœ‘ ∧ 𝐴 = 𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ 𝑐 ∈ 𝑃)
29 simprrl 780 . . . . . . . . 9 ((((πœ‘ ∧ 𝐴 = 𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ (𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴))
3029, 25eqtrd 2773 . . . . . . . 8 ((((πœ‘ ∧ 𝐴 = 𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ (𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝑀))
315, 6, 7, 19, 21, 28, 21, 30axtgcgrid 27447 . . . . . . 7 ((((πœ‘ ∧ 𝐴 = 𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ 𝑀 = 𝑐)
3227, 31eqtr3d 2775 . . . . . 6 ((((πœ‘ ∧ 𝐴 = 𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ 𝑏 = 𝑐)
3332ex 414 . . . . 5 (((πœ‘ ∧ 𝐴 = 𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) β†’ ((((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴))) β†’ 𝑏 = 𝑐))
3433ralrimivva 3194 . . . 4 ((πœ‘ ∧ 𝐴 = 𝑀) β†’ βˆ€π‘ ∈ 𝑃 βˆ€π‘ ∈ 𝑃 ((((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴))) β†’ 𝑏 = 𝑐))
3518, 34jca 513 . . 3 ((πœ‘ ∧ 𝐴 = 𝑀) β†’ (βˆƒπ‘ ∈ 𝑃 ((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ βˆ€π‘ ∈ 𝑃 βˆ€π‘ ∈ 𝑃 ((((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴))) β†’ 𝑏 = 𝑐)))
368adantr 482 . . . . . 6 ((πœ‘ ∧ 𝐴 β‰  𝑀) β†’ 𝐺 ∈ TarskiG)
371adantr 482 . . . . . 6 ((πœ‘ ∧ 𝐴 β‰  𝑀) β†’ 𝐴 ∈ 𝑃)
3820adantr 482 . . . . . 6 ((πœ‘ ∧ 𝐴 β‰  𝑀) β†’ 𝑀 ∈ 𝑃)
395, 6, 7, 36, 37, 38, 38, 37axtgsegcon 27448 . . . . 5 ((πœ‘ ∧ 𝐴 β‰  𝑀) β†’ βˆƒπ‘ ∈ 𝑃 (𝑀 ∈ (𝐴𝐼𝑏) ∧ (𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴)))
40 ancom 462 . . . . . . . 8 ((𝑀 ∈ (𝐴𝐼𝑏) ∧ (𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴)) ↔ ((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝐴𝐼𝑏)))
418adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑏 ∈ 𝑃) β†’ 𝐺 ∈ TarskiG)
421adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑏 ∈ 𝑃) β†’ 𝐴 ∈ 𝑃)
4320adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑏 ∈ 𝑃) β†’ 𝑀 ∈ 𝑃)
44 simpr 486 . . . . . . . . . 10 ((πœ‘ ∧ 𝑏 ∈ 𝑃) β†’ 𝑏 ∈ 𝑃)
455, 6, 7, 41, 42, 43, 44tgbtwncomb 27473 . . . . . . . . 9 ((πœ‘ ∧ 𝑏 ∈ 𝑃) β†’ (𝑀 ∈ (𝐴𝐼𝑏) ↔ 𝑀 ∈ (𝑏𝐼𝐴)))
4645anbi2d 630 . . . . . . . 8 ((πœ‘ ∧ 𝑏 ∈ 𝑃) β†’ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝐴𝐼𝑏)) ↔ ((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴))))
4740, 46bitrid 283 . . . . . . 7 ((πœ‘ ∧ 𝑏 ∈ 𝑃) β†’ ((𝑀 ∈ (𝐴𝐼𝑏) ∧ (𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴)) ↔ ((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴))))
4847rexbidva 3170 . . . . . 6 (πœ‘ β†’ (βˆƒπ‘ ∈ 𝑃 (𝑀 ∈ (𝐴𝐼𝑏) ∧ (𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴)) ↔ βˆƒπ‘ ∈ 𝑃 ((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴))))
4948adantr 482 . . . . 5 ((πœ‘ ∧ 𝐴 β‰  𝑀) β†’ (βˆƒπ‘ ∈ 𝑃 (𝑀 ∈ (𝐴𝐼𝑏) ∧ (𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴)) ↔ βˆƒπ‘ ∈ 𝑃 ((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴))))
5039, 49mpbid 231 . . . 4 ((πœ‘ ∧ 𝐴 β‰  𝑀) β†’ βˆƒπ‘ ∈ 𝑃 ((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)))
518ad3antrrr 729 . . . . . . 7 ((((πœ‘ ∧ 𝐴 β‰  𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ 𝐺 ∈ TarskiG)
5220ad3antrrr 729 . . . . . . 7 ((((πœ‘ ∧ 𝐴 β‰  𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ 𝑀 ∈ 𝑃)
531ad3antrrr 729 . . . . . . 7 ((((πœ‘ ∧ 𝐴 β‰  𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ 𝐴 ∈ 𝑃)
54 simplrl 776 . . . . . . 7 ((((πœ‘ ∧ 𝐴 β‰  𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ 𝑏 ∈ 𝑃)
55 simplrr 777 . . . . . . 7 ((((πœ‘ ∧ 𝐴 β‰  𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ 𝑐 ∈ 𝑃)
56 simpllr 775 . . . . . . 7 ((((πœ‘ ∧ 𝐴 β‰  𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ 𝐴 β‰  𝑀)
57 simprlr 779 . . . . . . . 8 ((((πœ‘ ∧ 𝐴 β‰  𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ 𝑀 ∈ (𝑏𝐼𝐴))
585, 6, 7, 51, 54, 52, 53, 57tgbtwncom 27472 . . . . . . 7 ((((πœ‘ ∧ 𝐴 β‰  𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ 𝑀 ∈ (𝐴𝐼𝑏))
59 simprrr 781 . . . . . . . 8 ((((πœ‘ ∧ 𝐴 β‰  𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ 𝑀 ∈ (𝑐𝐼𝐴))
605, 6, 7, 51, 55, 52, 53, 59tgbtwncom 27472 . . . . . . 7 ((((πœ‘ ∧ 𝐴 β‰  𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ 𝑀 ∈ (𝐴𝐼𝑐))
61 simprll 778 . . . . . . 7 ((((πœ‘ ∧ 𝐴 β‰  𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ (𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴))
62 simprrl 780 . . . . . . 7 ((((πœ‘ ∧ 𝐴 β‰  𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ (𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴))
635, 6, 7, 51, 52, 52, 53, 53, 54, 55, 56, 58, 60, 61, 62tgsegconeq 27470 . . . . . 6 ((((πœ‘ ∧ 𝐴 β‰  𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴)))) β†’ 𝑏 = 𝑐)
6463ex 414 . . . . 5 (((πœ‘ ∧ 𝐴 β‰  𝑀) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) β†’ ((((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴))) β†’ 𝑏 = 𝑐))
6564ralrimivva 3194 . . . 4 ((πœ‘ ∧ 𝐴 β‰  𝑀) β†’ βˆ€π‘ ∈ 𝑃 βˆ€π‘ ∈ 𝑃 ((((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴))) β†’ 𝑏 = 𝑐))
6650, 65jca 513 . . 3 ((πœ‘ ∧ 𝐴 β‰  𝑀) β†’ (βˆƒπ‘ ∈ 𝑃 ((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ βˆ€π‘ ∈ 𝑃 βˆ€π‘ ∈ 𝑃 ((((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴))) β†’ 𝑏 = 𝑐)))
6735, 66pm2.61dane 3029 . 2 (πœ‘ β†’ (βˆƒπ‘ ∈ 𝑃 ((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ βˆ€π‘ ∈ 𝑃 βˆ€π‘ ∈ 𝑃 ((((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴))) β†’ 𝑏 = 𝑐)))
68 oveq2 7366 . . . . 5 (𝑏 = 𝑐 β†’ (𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝑐))
6968eqeq1d 2735 . . . 4 (𝑏 = 𝑐 β†’ ((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ↔ (𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴)))
70 oveq1 7365 . . . . 5 (𝑏 = 𝑐 β†’ (𝑏𝐼𝐴) = (𝑐𝐼𝐴))
7170eleq2d 2820 . . . 4 (𝑏 = 𝑐 β†’ (𝑀 ∈ (𝑏𝐼𝐴) ↔ 𝑀 ∈ (𝑐𝐼𝐴)))
7269, 71anbi12d 632 . . 3 (𝑏 = 𝑐 β†’ (((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ↔ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴))))
7372reu4 3690 . 2 (βˆƒ!𝑏 ∈ 𝑃 ((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ↔ (βˆƒπ‘ ∈ 𝑃 ((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ βˆ€π‘ ∈ 𝑃 βˆ€π‘ ∈ 𝑃 ((((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)) ∧ ((𝑀 βˆ’ 𝑐) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑐𝐼𝐴))) β†’ 𝑏 = 𝑐)))
7467, 73sylibr 233 1 (πœ‘ β†’ βˆƒ!𝑏 ∈ 𝑃 ((𝑀 βˆ’ 𝑏) = (𝑀 βˆ’ 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  βˆƒ!wreu 3350  β€˜cfv 6497  (class class class)co 7358  Basecbs 17088  distcds 17147  TarskiGcstrkg 27411  Itvcitv 27417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5264
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361  df-trkgc 27432  df-trkgb 27433  df-trkgcb 27434  df-trkg 27437
This theorem is referenced by:  mircgr  27641  mirbtwn  27642  ismir  27643  mirf  27644  mireq  27649
  Copyright terms: Public domain W3C validator