mirhl

Description: If two points X and Y are on the same half-line from Z , the same applies to the mirror points. (Contributed by Thierry Arnoux, 21-Feb-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$
	mirhl.1	$⊢ φ \to X K (Z) Y$
Assertion	mirhl	$⊢ φ \to M (X) K (M (Z)) M (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		mirhl.1	$⊢ φ \to X K (Z) Y$
14	6	adantr	$⊢ (φ \land M (X) = M (Z)) \to G \in 𝒢_{Tarski}$
15	9	adantr	$⊢ (φ \land M (X) = M (Z)) \to A \in P$
16	10	adantr	$⊢ (φ \land M (X) = M (Z)) \to X \in P$
17	12	adantr	$⊢ (φ \land M (X) = M (Z)) \to Z \in P$
18		simpr	$⊢ (φ \land M (X) = M (Z)) \to M (X) = M (Z)$
19	1 2 3 4 5 14 15 7 16 17 18	mireq	$⊢ (φ \land M (X) = M (Z)) \to X = Z$
20	1 3 8 10 11 12 6	ishlg	$⊢ φ \to (X K (Z) Y \leftrightarrow (X \neq Z \land Y \neq Z \land (X \in (Z I Y) \lor Y \in (Z I X))))$
21	13 20	mpbid	$⊢ φ \to (X \neq Z \land Y \neq Z \land (X \in (Z I Y) \lor Y \in (Z I X)))$
22	21	simp1d	$⊢ φ \to X \neq Z$
23	22	adantr	$⊢ (φ \land M (X) = M (Z)) \to X \neq Z$
24	23	neneqd	$⊢ (φ \land M (X) = M (Z)) \to \neg X = Z$
25	19 24	pm2.65da	$⊢ φ \to \neg M (X) = M (Z)$
26	25	neqned	$⊢ φ \to M (X) \neq M (Z)$
27	6	adantr	$⊢ (φ \land M (Y) = M (Z)) \to G \in 𝒢_{Tarski}$
28	9	adantr	$⊢ (φ \land M (Y) = M (Z)) \to A \in P$
29	11	adantr	$⊢ (φ \land M (Y) = M (Z)) \to Y \in P$
30	12	adantr	$⊢ (φ \land M (Y) = M (Z)) \to Z \in P$
31		simpr	$⊢ (φ \land M (Y) = M (Z)) \to M (Y) = M (Z)$
32	1 2 3 4 5 27 28 7 29 30 31	mireq	$⊢ (φ \land M (Y) = M (Z)) \to Y = Z$
33	21	simp2d	$⊢ φ \to Y \neq Z$
34	33	adantr	$⊢ (φ \land M (Y) = M (Z)) \to Y \neq Z$
35	34	neneqd	$⊢ (φ \land M (Y) = M (Z)) \to \neg Y = Z$
36	32 35	pm2.65da	$⊢ φ \to \neg M (Y) = M (Z)$
37	36	neqned	$⊢ φ \to M (Y) \neq M (Z)$
38	21	simp3d	$⊢ φ \to (X \in (Z I Y) \lor Y \in (Z I X))$
39	6	adantr	$⊢ (φ \land X \in (Z I Y)) \to G \in 𝒢_{Tarski}$
40	9	adantr	$⊢ (φ \land X \in (Z I Y)) \to A \in P$
41	12	adantr	$⊢ (φ \land X \in (Z I Y)) \to Z \in P$
42	10	adantr	$⊢ (φ \land X \in (Z I Y)) \to X \in P$
43	11	adantr	$⊢ (φ \land X \in (Z I Y)) \to Y \in P$
44		simpr	$⊢ (φ \land X \in (Z I Y)) \to X \in (Z I Y)$
45	1 2 3 4 5 39 40 7 41 42 43 44	mirbtwni	$⊢ (φ \land X \in (Z I Y)) \to M (X) \in (M (Z) I M (Y))$
46	45	ex	$⊢ φ \to (X \in (Z I Y) \to M (X) \in (M (Z) I M (Y)))$
47	6	adantr	$⊢ (φ \land Y \in (Z I X)) \to G \in 𝒢_{Tarski}$
48	9	adantr	$⊢ (φ \land Y \in (Z I X)) \to A \in P$
49	12	adantr	$⊢ (φ \land Y \in (Z I X)) \to Z \in P$
50	11	adantr	$⊢ (φ \land Y \in (Z I X)) \to Y \in P$
51	10	adantr	$⊢ (φ \land Y \in (Z I X)) \to X \in P$
52		simpr	$⊢ (φ \land Y \in (Z I X)) \to Y \in (Z I X)$
53	1 2 3 4 5 47 48 7 49 50 51 52	mirbtwni	$⊢ (φ \land Y \in (Z I X)) \to M (Y) \in (M (Z) I M (X))$
54	53	ex	$⊢ φ \to (Y \in (Z I X) \to M (Y) \in (M (Z) I M (X)))$
55	46 54	orim12d	$⊢ φ \to ((X \in (Z I Y) \lor Y \in (Z I X)) \to (M (X) \in (M (Z) I M (Y)) \lor M (Y) \in (M (Z) I M (X))))$
56	38 55	mpd	$⊢ φ \to (M (X) \in (M (Z) I M (Y)) \lor M (Y) \in (M (Z) I M (X)))$
57	1 2 3 4 5 6 9 7 10	mircl	$⊢ φ \to M (X) \in P$
58	1 2 3 4 5 6 9 7 11	mircl	$⊢ φ \to M (Y) \in P$
59	1 2 3 4 5 6 9 7 12	mircl	$⊢ φ \to M (Z) \in P$
60	1 3 8 57 58 59 6	ishlg	$⊢ φ \to (M (X) K (M (Z)) M (Y) \leftrightarrow (M (X) \neq M (Z) \land M (Y) \neq M (Z) \land (M (X) \in (M (Z) I M (Y)) \lor M (Y) \in (M (Z) I M (X)))))$
61	26 37 56 60	mpbir3and	$⊢ φ \to M (X) K (M (Z)) M (Y)$

Metamath Proof Explorer

Theorem mirhl

Proof