mirbtwnhl

Description: If the center of the point inversion A is between two points X and Y , then the half lines are mirrored. (Contributed by Thierry Arnoux, 3-Mar-2020)

	Ref	Expression
Hypotheses	mirval.p	$⊢ P = {Base}_{G}$
	mirval.d	$⊢ \underset{˙}{-} = dist (G)$
	mirval.i	$⊢ I = Itv (G)$
	mirval.l	$⊢ L = {Line}_{𝒢} (G)$
	mirval.s	$⊢ S = {pInv}_{𝒢} (G)$
	mirval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	mirhl.m	$⊢ M = S (A)$
	mirhl.k	$⊢ K = {hl}_{𝒢} (G)$
	mirhl.a	$⊢ φ \to A \in P$
	mirhl.x	$⊢ φ \to X \in P$
	mirhl.y	$⊢ φ \to Y \in P$
	mirhl.z	$⊢ φ \to Z \in P$
	mirbtwnhl.1	$⊢ φ \to X \neq A$
	mirbtwnhl.2	$⊢ φ \to Y \neq A$
	mirbtwnhl.3	$⊢ φ \to A \in (X I Y)$
Assertion	mirbtwnhl	$⊢ φ \to (Z K (A) X \leftrightarrow M (Z) K (A) Y)$

Proof

Step	Hyp	Ref	Expression
1		mirval.p	$⊢ P = {Base}_{G}$
2		mirval.d	$⊢ \underset{˙}{-} = dist (G)$
3		mirval.i	$⊢ I = Itv (G)$
4		mirval.l	$⊢ L = {Line}_{𝒢} (G)$
5		mirval.s	$⊢ S = {pInv}_{𝒢} (G)$
6		mirval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		mirhl.m	$⊢ M = S (A)$
8		mirhl.k	$⊢ K = {hl}_{𝒢} (G)$
9		mirhl.a	$⊢ φ \to A \in P$
10		mirhl.x	$⊢ φ \to X \in P$
11		mirhl.y	$⊢ φ \to Y \in P$
12		mirhl.z	$⊢ φ \to Z \in P$
13		mirbtwnhl.1	$⊢ φ \to X \neq A$
14		mirbtwnhl.2	$⊢ φ \to Y \neq A$
15		mirbtwnhl.3	$⊢ φ \to A \in (X I Y)$
16		simpr	$⊢ (φ \land Z = A) \to Z = A$
17	1 3 8 9 10 9 6	hleqnid	$⊢ φ \to \neg A K (A) X$
18	17	adantr	$⊢ (φ \land Z = A) \to \neg A K (A) X$
19	16 18	eqnbrtrd	$⊢ (φ \land Z = A) \to \neg Z K (A) X$
20	16	fveq2d	$⊢ (φ \land Z = A) \to M (Z) = M (A)$
21	1 2 3 4 5 6 9 7	mircinv	$⊢ φ \to M (A) = A$
22	21	adantr	$⊢ (φ \land Z = A) \to M (A) = A$
23	20 22	eqtrd	$⊢ (φ \land Z = A) \to M (Z) = A$
24	1 3 8 9 11 9 6	hleqnid	$⊢ φ \to \neg A K (A) Y$
25	24	adantr	$⊢ (φ \land Z = A) \to \neg A K (A) Y$
26	23 25	eqnbrtrd	$⊢ (φ \land Z = A) \to \neg M (Z) K (A) Y$
27	19 26	2falsed	$⊢ (φ \land Z = A) \to (Z K (A) X \leftrightarrow M (Z) K (A) Y)$
28		simplr	$⊢ ((φ \land Z \neq A) \land Z K (A) X) \to Z \neq A$
29	28	neneqd	$⊢ ((φ \land Z \neq A) \land Z K (A) X) \to \neg Z = A$
30	6	ad3antrrr	$⊢ (((φ \land Z \neq A) \land Z K (A) X) \land M (Z) = A) \to G \in 𝒢_{Tarski}$
31	9	ad3antrrr	$⊢ (((φ \land Z \neq A) \land Z K (A) X) \land M (Z) = A) \to A \in P$
32	12	ad3antrrr	$⊢ (((φ \land Z \neq A) \land Z K (A) X) \land M (Z) = A) \to Z \in P$
33		simpr	$⊢ (((φ \land Z \neq A) \land Z K (A) X) \land M (Z) = A) \to M (Z) = A$
34	21	ad3antrrr	$⊢ (((φ \land Z \neq A) \land Z K (A) X) \land M (Z) = A) \to M (A) = A$
35	33 34	eqtr4d	$⊢ (((φ \land Z \neq A) \land Z K (A) X) \land M (Z) = A) \to M (Z) = M (A)$
36	1 2 3 4 5 30 31 7 32 31 35	mireq	$⊢ (((φ \land Z \neq A) \land Z K (A) X) \land M (Z) = A) \to Z = A$
37	29 36	mtand	$⊢ ((φ \land Z \neq A) \land Z K (A) X) \to \neg M (Z) = A$
38	37	neqned	$⊢ ((φ \land Z \neq A) \land Z K (A) X) \to M (Z) \neq A$
39	14	ad2antrr	$⊢ ((φ \land Z \neq A) \land Z K (A) X) \to Y \neq A$
40	6	ad2antrr	$⊢ ((φ \land Z \neq A) \land Z K (A) X) \to G \in 𝒢_{Tarski}$
41	10	ad2antrr	$⊢ ((φ \land Z \neq A) \land Z K (A) X) \to X \in P$
42	9	ad2antrr	$⊢ ((φ \land Z \neq A) \land Z K (A) X) \to A \in P$
43	1 2 3 4 5 6 9 7 12	mircl	$⊢ φ \to M (Z) \in P$
44	43	ad2antrr	$⊢ ((φ \land Z \neq A) \land Z K (A) X) \to M (Z) \in P$
45	11	ad2antrr	$⊢ ((φ \land Z \neq A) \land Z K (A) X) \to Y \in P$
46	13	ad2antrr	$⊢ ((φ \land Z \neq A) \land Z K (A) X) \to X \neq A$
47	12	ad2antrr	$⊢ ((φ \land Z \neq A) \land Z K (A) X) \to Z \in P$
48	1 3 8 12 10 9 6	ishlg	$⊢ φ \to (Z K (A) X \leftrightarrow (Z \neq A \land X \neq A \land (Z \in (A I X) \lor X \in (A I Z))))$
49	48	adantr	$⊢ (φ \land Z \neq A) \to (Z K (A) X \leftrightarrow (Z \neq A \land X \neq A \land (Z \in (A I X) \lor X \in (A I Z))))$
50	49	biimpa	$⊢ ((φ \land Z \neq A) \land Z K (A) X) \to (Z \neq A \land X \neq A \land (Z \in (A I X) \lor X \in (A I Z)))$
51	50	simp3d	$⊢ ((φ \land Z \neq A) \land Z K (A) X) \to (Z \in (A I X) \lor X \in (A I Z))$
52	51	orcomd	$⊢ ((φ \land Z \neq A) \land Z K (A) X) \to (X \in (A I Z) \lor Z \in (A I X))$
53	1 2 3 4 5 40 7 42 41 47 52	mirconn	$⊢ ((φ \land Z \neq A) \land Z K (A) X) \to A \in (X I M (Z))$
54	15	ad2antrr	$⊢ ((φ \land Z \neq A) \land Z K (A) X) \to A \in (X I Y)$
55	1 3 40 41 42 44 45 46 53 54	tgbtwnconn2	$⊢ ((φ \land Z \neq A) \land Z K (A) X) \to (M (Z) \in (A I Y) \lor Y \in (A I M (Z)))$
56	1 3 8 43 11 9 6	ishlg	$⊢ φ \to (M (Z) K (A) Y \leftrightarrow (M (Z) \neq A \land Y \neq A \land (M (Z) \in (A I Y) \lor Y \in (A I M (Z)))))$
57	56	adantr	$⊢ (φ \land Z \neq A) \to (M (Z) K (A) Y \leftrightarrow (M (Z) \neq A \land Y \neq A \land (M (Z) \in (A I Y) \lor Y \in (A I M (Z)))))$
58	57	adantr	$⊢ ((φ \land Z \neq A) \land Z K (A) X) \to (M (Z) K (A) Y \leftrightarrow (M (Z) \neq A \land Y \neq A \land (M (Z) \in (A I Y) \lor Y \in (A I M (Z)))))$
59	38 39 55 58	mpbir3and	$⊢ ((φ \land Z \neq A) \land Z K (A) X) \to M (Z) K (A) Y$
60		simplr	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to Z \neq A$
61	13	ad2antrr	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to X \neq A$
62	6	ad2antrr	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to G \in 𝒢_{Tarski}$
63	11	ad2antrr	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to Y \in P$
64	9	ad2antrr	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to A \in P$
65	12	ad2antrr	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to Z \in P$
66	10	ad2antrr	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to X \in P$
67	14	ad2antrr	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to Y \neq A$
68	21	ad2antrr	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to M (A) = A$
69	43	ad2antrr	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to M (Z) \in P$
70	1 2 3 4 5 62 64 7 63	mircl	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to M (Y) \in P$
71	57	biimpa	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to (M (Z) \neq A \land Y \neq A \land (M (Z) \in (A I Y) \lor Y \in (A I M (Z))))$
72	71	simp3d	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to (M (Z) \in (A I Y) \lor Y \in (A I M (Z)))$
73	1 2 3 4 5 62 7 64 69 63 72	mirconn	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to A \in (M (Z) I M (Y))$
74	1 2 3 62 69 64 70 73	tgbtwncom	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to A \in (M (Y) I M (Z))$
75	68 74	eqeltrd	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to M (A) \in (M (Y) I M (Z))$
76	1 2 3 4 5 62 64 7 63 64 65	mirbtwnb	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to (A \in (Y I Z) \leftrightarrow M (A) \in (M (Y) I M (Z)))$
77	75 76	mpbird	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to A \in (Y I Z)$
78	1 2 3 6 10 9 11 15	tgbtwncom	$⊢ φ \to A \in (Y I X)$
79	78	ad2antrr	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to A \in (Y I X)$
80	1 3 62 63 64 65 66 67 77 79	tgbtwnconn2	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to (Z \in (A I X) \lor X \in (A I Z))$
81	49	adantr	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to (Z K (A) X \leftrightarrow (Z \neq A \land X \neq A \land (Z \in (A I X) \lor X \in (A I Z))))$
82	60 61 80 81	mpbir3and	$⊢ ((φ \land Z \neq A) \land M (Z) K (A) Y) \to Z K (A) X$
83	59 82	impbida	$⊢ (φ \land Z \neq A) \to (Z K (A) X \leftrightarrow M (Z) K (A) Y)$
84	27 83	pm2.61dane	$⊢ φ \to (Z K (A) X \leftrightarrow M (Z) K (A) Y)$

Metamath Proof Explorer

Theorem mirbtwnhl

Proof