mirreu3

Description: Existential uniqueness of the mirror point. Theorem 7.8 of Schwabhauser p. 49. (Contributed by Thierry Arnoux, 30-May-2019)

	Ref	Expression
Hypotheses	mirreu.p	$⊢ P = {Base}_{G}$
	mirreu.d	$⊢ \underset{˙}{-} = dist (G)$
	mirreu.i	$⊢ I = Itv (G)$
	mirreu.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	mirreu.a	$⊢ φ \to A \in P$
	mirreu.m	$⊢ φ \to M \in P$
Assertion	mirreu3	$⊢ φ \to \exists! b \in P (M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A))$

Proof

Step	Hyp	Ref	Expression
1		mirreu.p	$⊢ P = {Base}_{G}$
2		mirreu.d	$⊢ \underset{˙}{-} = dist (G)$
3		mirreu.i	$⊢ I = Itv (G)$
4		mirreu.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		mirreu.a	$⊢ φ \to A \in P$
6		mirreu.m	$⊢ φ \to M \in P$
7	5	adantr	$⊢ (φ \land A = M) \to A \in P$
8		eqidd	$⊢ (φ \land A = M) \to M \underset{˙}{-} A = M \underset{˙}{-} A$
9		simpr	$⊢ (φ \land A = M) \to A = M$
10	4	adantr	$⊢ (φ \land A = M) \to G \in 𝒢_{Tarski}$
11	1 2 3 10 7 7	tgbtwntriv2	$⊢ (φ \land A = M) \to A \in (A I A)$
12	9 11	eqeltrrd	$⊢ (φ \land A = M) \to M \in (A I A)$
13		oveq2	$⊢ b = A \to M \underset{˙}{-} b = M \underset{˙}{-} A$
14	13	eqeq1d	$⊢ b = A \to (M \underset{˙}{-} b = M \underset{˙}{-} A \leftrightarrow M \underset{˙}{-} A = M \underset{˙}{-} A)$
15		oveq1	$⊢ b = A \to b I A = A I A$
16	15	eleq2d	$⊢ b = A \to (M \in (b I A) \leftrightarrow M \in (A I A))$
17	14 16	anbi12d	$⊢ b = A \to ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \leftrightarrow (M \underset{˙}{-} A = M \underset{˙}{-} A \land M \in (A I A)))$
18	17	rspcev	$⊢ (A \in P \land (M \underset{˙}{-} A = M \underset{˙}{-} A \land M \in (A I A))) \to \exists b \in P (M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A))$
19	7 8 12 18	syl12anc	$⊢ (φ \land A = M) \to \exists b \in P (M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A))$
20	4	ad3antrrr	$⊢ (((φ \land A = M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to G \in 𝒢_{Tarski}$
21	6	ad3antrrr	$⊢ (((φ \land A = M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to M \in P$
22		simplrl	$⊢ (((φ \land A = M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to b \in P$
23		simprll	$⊢ (((φ \land A = M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to M \underset{˙}{-} b = M \underset{˙}{-} A$
24		simpllr	$⊢ (((φ \land A = M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to A = M$
25	24	oveq2d	$⊢ (((φ \land A = M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to M \underset{˙}{-} A = M \underset{˙}{-} M$
26	23 25	eqtrd	$⊢ (((φ \land A = M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to M \underset{˙}{-} b = M \underset{˙}{-} M$
27	1 2 3 20 21 22 21 26	axtgcgrid	$⊢ (((φ \land A = M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to M = b$
28		simplrr	$⊢ (((φ \land A = M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to c \in P$
29		simprrl	$⊢ (((φ \land A = M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to M \underset{˙}{-} c = M \underset{˙}{-} A$
30	29 25	eqtrd	$⊢ (((φ \land A = M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to M \underset{˙}{-} c = M \underset{˙}{-} M$
31	1 2 3 20 21 28 21 30	axtgcgrid	$⊢ (((φ \land A = M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to M = c$
32	27 31	eqtr3d	$⊢ (((φ \land A = M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to b = c$
33	32	ex	$⊢ ((φ \land A = M) \land (b \in P \land c \in P)) \to (((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A))) \to b = c)$
34	33	ralrimivva	$⊢ (φ \land A = M) \to \forall b \in P \forall c \in P (((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A))) \to b = c)$
35	19 34	jca	$⊢ (φ \land A = M) \to (\exists b \in P (M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land \forall b \in P \forall c \in P (((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A))) \to b = c))$
36	4	adantr	$⊢ (φ \land A \neq M) \to G \in 𝒢_{Tarski}$
37	5	adantr	$⊢ (φ \land A \neq M) \to A \in P$
38	6	adantr	$⊢ (φ \land A \neq M) \to M \in P$
39	1 2 3 36 37 38 38 37	axtgsegcon	$⊢ (φ \land A \neq M) \to \exists b \in P (M \in (A I b) \land M \underset{˙}{-} b = M \underset{˙}{-} A)$
40		ancom	$⊢ (M \in (A I b) \land M \underset{˙}{-} b = M \underset{˙}{-} A) \leftrightarrow (M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (A I b))$
41	4	adantr	$⊢ (φ \land b \in P) \to G \in 𝒢_{Tarski}$
42	5	adantr	$⊢ (φ \land b \in P) \to A \in P$
43	6	adantr	$⊢ (φ \land b \in P) \to M \in P$
44		simpr	$⊢ (φ \land b \in P) \to b \in P$
45	1 2 3 41 42 43 44	tgbtwncomb	$⊢ (φ \land b \in P) \to (M \in (A I b) \leftrightarrow M \in (b I A))$
46	45	anbi2d	$⊢ (φ \land b \in P) \to ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (A I b)) \leftrightarrow (M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)))$
47	40 46	syl5bb	$⊢ (φ \land b \in P) \to ((M \in (A I b) \land M \underset{˙}{-} b = M \underset{˙}{-} A) \leftrightarrow (M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)))$
48	47	rexbidva	$⊢ φ \to (\exists b \in P (M \in (A I b) \land M \underset{˙}{-} b = M \underset{˙}{-} A) \leftrightarrow \exists b \in P (M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)))$
49	48	adantr	$⊢ (φ \land A \neq M) \to (\exists b \in P (M \in (A I b) \land M \underset{˙}{-} b = M \underset{˙}{-} A) \leftrightarrow \exists b \in P (M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)))$
50	39 49	mpbid	$⊢ (φ \land A \neq M) \to \exists b \in P (M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A))$
51	4	ad3antrrr	$⊢ (((φ \land A \neq M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to G \in 𝒢_{Tarski}$
52	6	ad3antrrr	$⊢ (((φ \land A \neq M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to M \in P$
53	5	ad3antrrr	$⊢ (((φ \land A \neq M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to A \in P$
54		simplrl	$⊢ (((φ \land A \neq M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to b \in P$
55		simplrr	$⊢ (((φ \land A \neq M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to c \in P$
56		simpllr	$⊢ (((φ \land A \neq M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to A \neq M$
57		simprlr	$⊢ (((φ \land A \neq M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to M \in (b I A)$
58	1 2 3 51 54 52 53 57	tgbtwncom	$⊢ (((φ \land A \neq M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to M \in (A I b)$
59		simprrr	$⊢ (((φ \land A \neq M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to M \in (c I A)$
60	1 2 3 51 55 52 53 59	tgbtwncom	$⊢ (((φ \land A \neq M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to M \in (A I c)$
61		simprll	$⊢ (((φ \land A \neq M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to M \underset{˙}{-} b = M \underset{˙}{-} A$
62		simprrl	$⊢ (((φ \land A \neq M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to M \underset{˙}{-} c = M \underset{˙}{-} A$
63	1 2 3 51 52 52 53 53 54 55 56 58 60 61 62	tgsegconeq	$⊢ (((φ \land A \neq M) \land (b \in P \land c \in P)) \land ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))) \to b = c$
64	63	ex	$⊢ ((φ \land A \neq M) \land (b \in P \land c \in P)) \to (((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A))) \to b = c)$
65	64	ralrimivva	$⊢ (φ \land A \neq M) \to \forall b \in P \forall c \in P (((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A))) \to b = c)$
66	50 65	jca	$⊢ (φ \land A \neq M) \to (\exists b \in P (M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land \forall b \in P \forall c \in P (((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A))) \to b = c))$
67	35 66	pm2.61dane	$⊢ φ \to (\exists b \in P (M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land \forall b \in P \forall c \in P (((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A))) \to b = c))$
68		oveq2	$⊢ b = c \to M \underset{˙}{-} b = M \underset{˙}{-} c$
69	68	eqeq1d	$⊢ b = c \to (M \underset{˙}{-} b = M \underset{˙}{-} A \leftrightarrow M \underset{˙}{-} c = M \underset{˙}{-} A)$
70		oveq1	$⊢ b = c \to b I A = c I A$
71	70	eleq2d	$⊢ b = c \to (M \in (b I A) \leftrightarrow M \in (c I A))$
72	69 71	anbi12d	$⊢ b = c \to ((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \leftrightarrow (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A)))$
73	72	reu4	$⊢ \exists! b \in P (M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \leftrightarrow (\exists b \in P (M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land \forall b \in P \forall c \in P (((M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A)) \land (M \underset{˙}{-} c = M \underset{˙}{-} A \land M \in (c I A))) \to b = c))$
74	67 73	sylibr	$⊢ φ \to \exists! b \in P (M \underset{˙}{-} b = M \underset{˙}{-} A \land M \in (b I A))$

Metamath Proof Explorer

Theorem mirreu3

Proof