Theorem 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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	mirval.d	⊢ − = ( dist ‘ 𝐺 )
	mirval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	mirval.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	mirval.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
	mirval.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	mirhl.m	⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
	mirhl.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	mirhl.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	mirhl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	mirhl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	mirhl.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
	mirhl.1	⊢ ( 𝜑 → 𝑋 ( 𝐾 ‘ 𝑍 ) 𝑌 )
Assertion	mirhl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑍 ) ) ( 𝑀 ‘ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		mirval.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		mirval.d	⊢ − = ( dist ‘ 𝐺 )
3		mirval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		mirval.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		mirval.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
6		mirval.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7		mirhl.m	⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
8		mirhl.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
9		mirhl.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
10		mirhl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
11		mirhl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
12		mirhl.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
13		mirhl.1	⊢ ( 𝜑 → 𝑋 ( 𝐾 ‘ 𝑍 ) 𝑌 )
14	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑍 ) ) → 𝐺 ∈ TarskiG )
15	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑍 ) ) → 𝐴 ∈ 𝑃 )
16	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑍 ) ) → 𝑋 ∈ 𝑃 )
17	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑍 ) ) → 𝑍 ∈ 𝑃 )
18		simpr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑍 ) ) → ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑍 ) )
19	1 2 3 4 5 14 15 7 16 17 18	mireq	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑍 ) ) → 𝑋 = 𝑍 )
20	1 3 8 10 11 12 6	ishlg	⊢ ( 𝜑 → ( 𝑋 ( 𝐾 ‘ 𝑍 ) 𝑌 ↔ ( 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ∧ ( 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ) ) )
21	13 20	mpbid	⊢ ( 𝜑 → ( 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ∧ ( 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ) )
22	21	simp1d	⊢ ( 𝜑 → 𝑋 ≠ 𝑍 )
23	22	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑍 ) ) → 𝑋 ≠ 𝑍 )
24	23	neneqd	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑍 ) ) → ¬ 𝑋 = 𝑍 )
25	19 24	pm2.65da	⊢ ( 𝜑 → ¬ ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑍 ) )
26	25	neqned	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ≠ ( 𝑀 ‘ 𝑍 ) )
27	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) = ( 𝑀 ‘ 𝑍 ) ) → 𝐺 ∈ TarskiG )
28	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) = ( 𝑀 ‘ 𝑍 ) ) → 𝐴 ∈ 𝑃 )
29	11	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) = ( 𝑀 ‘ 𝑍 ) ) → 𝑌 ∈ 𝑃 )
30	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) = ( 𝑀 ‘ 𝑍 ) ) → 𝑍 ∈ 𝑃 )
31		simpr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) = ( 𝑀 ‘ 𝑍 ) ) → ( 𝑀 ‘ 𝑌 ) = ( 𝑀 ‘ 𝑍 ) )
32	1 2 3 4 5 27 28 7 29 30 31	mireq	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) = ( 𝑀 ‘ 𝑍 ) ) → 𝑌 = 𝑍 )
33	21	simp2d	⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
34	33	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) = ( 𝑀 ‘ 𝑍 ) ) → 𝑌 ≠ 𝑍 )
35	34	neneqd	⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) = ( 𝑀 ‘ 𝑍 ) ) → ¬ 𝑌 = 𝑍 )
36	32 35	pm2.65da	⊢ ( 𝜑 → ¬ ( 𝑀 ‘ 𝑌 ) = ( 𝑀 ‘ 𝑍 ) )
37	36	neqned	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ≠ ( 𝑀 ‘ 𝑍 ) )
38	21	simp3d	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) )
39	6	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ) → 𝐺 ∈ TarskiG )
40	9	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ) → 𝐴 ∈ 𝑃 )
41	12	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ) → 𝑍 ∈ 𝑃 )
42	10	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ) → 𝑋 ∈ 𝑃 )
43	11	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ) → 𝑌 ∈ 𝑃 )
44		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ) → 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) )
45	1 2 3 4 5 39 40 7 41 42 43 44	mirbtwni	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ) → ( 𝑀 ‘ 𝑋 ) ∈ ( ( 𝑀 ‘ 𝑍 ) 𝐼 ( 𝑀 ‘ 𝑌 ) ) )
46	45	ex	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) → ( 𝑀 ‘ 𝑋 ) ∈ ( ( 𝑀 ‘ 𝑍 ) 𝐼 ( 𝑀 ‘ 𝑌 ) ) ) )
47	6	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) → 𝐺 ∈ TarskiG )
48	9	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) → 𝐴 ∈ 𝑃 )
49	12	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) → 𝑍 ∈ 𝑃 )
50	11	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) → 𝑌 ∈ 𝑃 )
51	10	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) → 𝑋 ∈ 𝑃 )
52		simpr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) → 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) )
53	1 2 3 4 5 47 48 7 49 50 51 52	mirbtwni	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) → ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑍 ) 𝐼 ( 𝑀 ‘ 𝑋 ) ) )
54	53	ex	⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) → ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑍 ) 𝐼 ( 𝑀 ‘ 𝑋 ) ) ) )
55	46 54	orim12d	⊢ ( 𝜑 → ( ( 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) → ( ( 𝑀 ‘ 𝑋 ) ∈ ( ( 𝑀 ‘ 𝑍 ) 𝐼 ( 𝑀 ‘ 𝑌 ) ) ∨ ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑍 ) 𝐼 ( 𝑀 ‘ 𝑋 ) ) ) ) )
56	38 55	mpd	⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ∈ ( ( 𝑀 ‘ 𝑍 ) 𝐼 ( 𝑀 ‘ 𝑌 ) ) ∨ ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑍 ) 𝐼 ( 𝑀 ‘ 𝑋 ) ) ) )
57	1 2 3 4 5 6 9 7 10	mircl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ∈ 𝑃 )
58	1 2 3 4 5 6 9 7 11	mircl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ∈ 𝑃 )
59	1 2 3 4 5 6 9 7 12	mircl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑍 ) ∈ 𝑃 )
60	1 3 8 57 58 59 6	ishlg	⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑍 ) ) ( 𝑀 ‘ 𝑌 ) ↔ ( ( 𝑀 ‘ 𝑋 ) ≠ ( 𝑀 ‘ 𝑍 ) ∧ ( 𝑀 ‘ 𝑌 ) ≠ ( 𝑀 ‘ 𝑍 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ ( ( 𝑀 ‘ 𝑍 ) 𝐼 ( 𝑀 ‘ 𝑌 ) ) ∨ ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑍 ) 𝐼 ( 𝑀 ‘ 𝑋 ) ) ) ) ) )
61	26 37 56 60	mpbir3and	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑍 ) ) ( 𝑀 ‘ 𝑌 ) )