Theorem mirreu3 23907

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	|- P = ( Base ` G )
mirreu.d	|- .- = ( dist ` G )
mirreu.i	|- I = (Itv ` G )
mirreu.g	|- ( ph -> G e. TarskiG )
mirreu.a	|- ( ph -> A e. P )
mirreu.m	|- ( ph -> M e. P )

Assertion

Ref	Expression
mirreu3	|- ( ph -> E! b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) )

Distinct variable groups:   .- , b   A, b   I, b   M, b   P, b   ph, b

Allowed substitution hint:   G( b)

Proof of Theorem mirreu3

Dummy variable c is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mirreu.a	. . . . . 6 |- ( ph -> A e. P )
2	1	adantr 465	. . . . 5 |- ( ( ph /\ A = M ) -> A e. P )
3		eqidd 2444	. . . . 5 |- ( ( ph /\ A = M ) -> ( M .- A ) = ( M .- A ) )
4		simpr 461	. . . . . 6 |- ( ( ph /\ A = M ) -> A = M )
5		mirreu.p	. . . . . . 7 |- P = ( Base ` G )
6		mirreu.d	. . . . . . 7 |- .- = ( dist ` G )
7		mirreu.i	. . . . . . 7 |- I = (Itv ` G )
8		mirreu.g	. . . . . . . 8 |- ( ph -> G e. TarskiG )
9	8	adantr 465	. . . . . . 7 |- ( ( ph /\ A = M ) -> G e. TarskiG )
10	5, 6, 7, 9, 2, 2	tgbtwntriv2 23750	. . . . . 6 |- ( ( ph /\ A = M ) -> A e. ( A I A ) )
11	4, 10	eqeltrrd 2532	. . . . 5 |- ( ( ph /\ A = M ) -> M e. ( A I A ) )
12		oveq2 6289	. . . . . . . 8 |- ( b = A -> ( M .- b ) = ( M .- A ) )
13	12	eqeq1d 2445	. . . . . . 7 |- ( b = A -> ( ( M .- b ) = ( M .- A ) <-> ( M .- A ) = ( M .- A ) ) )
14		oveq1 6288	. . . . . . . 8 |- ( b = A -> ( b I A ) = ( A I A ) )
15	14	eleq2d 2513	. . . . . . 7 |- ( b = A -> ( M e. ( b I A ) <-> M e. ( A I A ) ) )
16	13, 15	anbi12d 710	. . . . . 6 |- ( b = A -> ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) <-> ( ( M .- A ) = ( M .- A ) /\ M e. ( A I A ) ) ) )
17	16	rspcev 3196	. . . . 5 |- ( ( A e. P /\ ( ( M .- A ) = ( M .- A ) /\ M e. ( A I A ) ) ) -> E. b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) )
18	2, 3, 11, 17	syl12anc 1227	. . . 4 |- ( ( ph /\ A = M ) -> E. b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) )
19	8	ad3antrrr 729	. . . . . . . 8 |- ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> G e. TarskiG )
20		mirreu.m	. . . . . . . . 9 |- ( ph -> M e. P )
21	20	ad3antrrr 729	. . . . . . . 8 |- ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> M e. P )
22		simplrl 761	. . . . . . . 8 |- ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> b e. P )
23		simprll 763	. . . . . . . . 9 |- ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> ( M .- b ) = ( M .- A ) )
24		simpllr 760	. . . . . . . . . 10 |- ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> A = M )
25	24	oveq2d 6297	. . . . . . . . 9 |- ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> ( M .- A ) = ( M .- M ) )
26	23, 25	eqtrd 2484	. . . . . . . 8 |- ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> ( M .- b ) = ( M .- M ) )
27	5, 6, 7, 19, 21, 22, 21, 26	axtgcgrid 23732	. . . . . . 7 |- ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> M = b )
28		simplrr 762	. . . . . . . 8 |- ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> c e. P )
29		simprrl 765	. . . . . . . . 9 |- ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> ( M .- c ) = ( M .- A ) )
30	29, 25	eqtrd 2484	. . . . . . . 8 |- ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> ( M .- c ) = ( M .- M ) )
31	5, 6, 7, 19, 21, 28, 21, 30	axtgcgrid 23732	. . . . . . 7 |- ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> M = c )
32	27, 31	eqtr3d 2486	. . . . . 6 |- ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> b = c )
33	32	ex 434	. . . . 5 |- ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) -> ( ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) -> b = c ) )
34	33	ralrimivva 2864	. . . 4 |- ( ( ph /\ A = M ) -> A. b e. P A. c e. P ( ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) -> b = c ) )
35	18, 34	jca 532	. . 3 |- ( ( ph /\ A = M ) -> ( E. b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ A. b e. P A. c e. P ( ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) -> b = c ) ) )
36	8	adantr 465	. . . . . 6 |- ( ( ph /\ A =/= M ) -> G e. TarskiG )
37	1	adantr 465	. . . . . 6 |- ( ( ph /\ A =/= M ) -> A e. P )
38	20	adantr 465	. . . . . 6 |- ( ( ph /\ A =/= M ) -> M e. P )
39	5, 6, 7, 36, 37, 38, 38, 37	axtgsegcon 23733	. . . . 5 |- ( ( ph /\ A =/= M ) -> E. b e. P ( M e. ( A I b ) /\ ( M .- b ) = ( M .- A ) ) )
40		ancom 450	. . . . . . . 8 |- ( ( M e. ( A I b ) /\ ( M .- b ) = ( M .- A ) ) <-> ( ( M .- b ) = ( M .- A ) /\ M e. ( A I b ) ) )
41	8	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ b e. P ) -> G e. TarskiG )
42	1	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ b e. P ) -> A e. P )
43	20	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ b e. P ) -> M e. P )
44		simpr 461	. . . . . . . . . 10 |- ( ( ph /\ b e. P ) -> b e. P )
45	5, 6, 7, 41, 42, 43, 44	tgbtwncomb 23752	. . . . . . . . 9 |- ( ( ph /\ b e. P ) -> ( M e. ( A I b ) <-> M e. ( b I A ) ) )
46	45	anbi2d 703	. . . . . . . 8 |- ( ( ph /\ b e. P ) -> ( ( ( M .- b ) = ( M .- A ) /\ M e. ( A I b ) ) <-> ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) ) )
47	40, 46	syl5bb 257	. . . . . . 7 |- ( ( ph /\ b e. P ) -> ( ( M e. ( A I b ) /\ ( M .- b ) = ( M .- A ) ) <-> ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) ) )
48	47	rexbidva 2951	. . . . . 6 |- ( ph -> ( E. b e. P ( M e. ( A I b ) /\ ( M .- b ) = ( M .- A ) ) <-> E. b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) ) )
49	48	adantr 465	. . . . 5 |- ( ( ph /\ A =/= M ) -> ( E. b e. P ( M e. ( A I b ) /\ ( M .- b ) = ( M .- A ) ) <-> E. b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) ) )
50	39, 49	mpbid 210	. . . 4 |- ( ( ph /\ A =/= M ) -> E. b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) )
51	8	ad3antrrr 729	. . . . . . 7 |- ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> G e. TarskiG )
52	20	ad3antrrr 729	. . . . . . 7 |- ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> M e. P )
53	1	ad3antrrr 729	. . . . . . 7 |- ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> A e. P )
54		simplrl 761	. . . . . . 7 |- ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> b e. P )
55		simplrr 762	. . . . . . 7 |- ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> c e. P )
56		simpllr 760	. . . . . . 7 |- ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> A =/= M )
57		simprlr 764	. . . . . . . 8 |- ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> M e. ( b I A ) )
58	5, 6, 7, 51, 54, 52, 53, 57	tgbtwncom 23751	. . . . . . 7 |- ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> M e. ( A I b ) )
59		simprrr 766	. . . . . . . 8 |- ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> M e. ( c I A ) )
60	5, 6, 7, 51, 55, 52, 53, 59	tgbtwncom 23751	. . . . . . 7 |- ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> M e. ( A I c ) )
61		simprll 763	. . . . . . 7 |- ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> ( M .- b ) = ( M .- A ) )
62		simprrl 765	. . . . . . 7 |- ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> ( M .- c ) = ( M .- A ) )
63	5, 6, 7, 51, 52, 52, 53, 53, 54, 55, 56, 58, 60, 61, 62	tgsegconeq 23749	. . . . . 6 |- ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> b = c )
64	63	ex 434	. . . . 5 |- ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) -> ( ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) -> b = c ) )
65	64	ralrimivva 2864	. . . 4 |- ( ( ph /\ A =/= M ) -> A. b e. P A. c e. P ( ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) -> b = c ) )
66	50, 65	jca 532	. . 3 |- ( ( ph /\ A =/= M ) -> ( E. b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ A. b e. P A. c e. P ( ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) -> b = c ) ) )
67	35, 66	pm2.61dane 2761	. 2 |- ( ph -> ( E. b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ A. b e. P A. c e. P ( ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) -> b = c ) ) )
68		oveq2 6289	. . . . 5 |- ( b = c -> ( M .- b ) = ( M .- c ) )
69	68	eqeq1d 2445	. . . 4 |- ( b = c -> ( ( M .- b ) = ( M .- A ) <-> ( M .- c ) = ( M .- A ) ) )
70		oveq1 6288	. . . . 5 |- ( b = c -> ( b I A ) = ( c I A ) )
71	70	eleq2d 2513	. . . 4 |- ( b = c -> ( M e. ( b I A ) <-> M e. ( c I A ) ) )
72	69, 71	anbi12d 710	. . 3 |- ( b = c -> ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) <-> ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) )
73	72	reu4 3279	. 2 |- ( E! b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) <-> ( E. b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ A. b e. P A. c e. P ( ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) -> b = c ) ) )
74	67, 73	sylibr 212	1 |- ( ph -> E! b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1383   e. wcel 1804   =/= wne 2638   A.wral 2793   E.wrex 2794   E!wreu 2795   ` cfv 5578  (class class class)co 6281   Basecbs 14509   distcds 14583  TarskiGcstrkg 23697  Itvcitv 23704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-nul 4566

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-reu 2800  df-rmo 2801  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-ov 6284  df-trkgc 23716  df-trkgb 23717  df-trkgcb 23718  df-trkg 23722

This theorem is referenced by:  mircgr  23910  mirbtwn  23911  ismir  23912  mirf  23913  mireq  23918