mirlni

Description: The mirror of a point X on a line ( Y L Z ) is on the mirrored line ( ( MY ) L ( MZ ) ) . (Contributed by Thierry Arnoux, 13-Jul-2026)

	Ref	Expression
Hypotheses	mirlni.p	$⊢ P = {Base}_{G}$
	mirlni.l	$⊢ L = {Line}_{𝒢} (G)$
	mirlni.s	$⊢ S = {pInv}_{𝒢} (G)$
	mirlni.m	$⊢ M = S (A)$
	mirlni.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	mirlni.a	$⊢ φ \to A \in P$
	mirlni.x	$⊢ φ \to X \in P$
	mirlni.y	$⊢ φ \to Y \in P$
	mirlni.z	$⊢ φ \to Z \in P$
	mirlni.1	$⊢ φ \to Z \neq Y$
	mirlni.2	$⊢ φ \to X \in (Y L Z)$
Assertion	mirlni	$⊢ φ \to M (X) \in (M (Y) L M (Z))$

Proof

Step	Hyp	Ref	Expression
1		mirlni.p	$⊢ P = {Base}_{G}$
2		mirlni.l	$⊢ L = {Line}_{𝒢} (G)$
3		mirlni.s	$⊢ S = {pInv}_{𝒢} (G)$
4		mirlni.m	$⊢ M = S (A)$
5		mirlni.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		mirlni.a	$⊢ φ \to A \in P$
7		mirlni.x	$⊢ φ \to X \in P$
8		mirlni.y	$⊢ φ \to Y \in P$
9		mirlni.z	$⊢ φ \to Z \in P$
10		mirlni.1	$⊢ φ \to Z \neq Y$
11		mirlni.2	$⊢ φ \to X \in (Y L Z)$
12		eqid	$⊢ Itv (G) = Itv (G)$
13	10	necomd	$⊢ φ \to Y \neq Z$
14	1 2 12 5 8 9 13 7	tgellng	$⊢ φ \to (X \in (Y L Z) \leftrightarrow (X \in (Y Itv (G) Z) \lor Y \in (X Itv (G) Z) \lor Z \in (Y Itv (G) X)))$
15	11 14	mpbid	$⊢ φ \to (X \in (Y Itv (G) Z) \lor Y \in (X Itv (G) Z) \lor Z \in (Y Itv (G) X))$
16		eqid	$⊢ dist (G) = dist (G)$
17	5	adantr	$⊢ (φ \land X \in (Y Itv (G) Z)) \to G \in 𝒢_{Tarski}$
18	6	adantr	$⊢ (φ \land X \in (Y Itv (G) Z)) \to A \in P$
19	8	adantr	$⊢ (φ \land X \in (Y Itv (G) Z)) \to Y \in P$
20	7	adantr	$⊢ (φ \land X \in (Y Itv (G) Z)) \to X \in P$
21	9	adantr	$⊢ (φ \land X \in (Y Itv (G) Z)) \to Z \in P$
22		simpr	$⊢ (φ \land X \in (Y Itv (G) Z)) \to X \in (Y Itv (G) Z)$
23	1 16 12 2 3 17 18 4 19 20 21 22	mirbtwni	$⊢ (φ \land X \in (Y Itv (G) Z)) \to M (X) \in (M (Y) Itv (G) M (Z))$
24	5	adantr	$⊢ (φ \land Y \in (X Itv (G) Z)) \to G \in 𝒢_{Tarski}$
25	6	adantr	$⊢ (φ \land Y \in (X Itv (G) Z)) \to A \in P$
26	7	adantr	$⊢ (φ \land Y \in (X Itv (G) Z)) \to X \in P$
27	8	adantr	$⊢ (φ \land Y \in (X Itv (G) Z)) \to Y \in P$
28	9	adantr	$⊢ (φ \land Y \in (X Itv (G) Z)) \to Z \in P$
29		simpr	$⊢ (φ \land Y \in (X Itv (G) Z)) \to Y \in (X Itv (G) Z)$
30	1 16 12 2 3 24 25 4 26 27 28 29	mirbtwni	$⊢ (φ \land Y \in (X Itv (G) Z)) \to M (Y) \in (M (X) Itv (G) M (Z))$
31	5	adantr	$⊢ (φ \land Z \in (Y Itv (G) X)) \to G \in 𝒢_{Tarski}$
32	6	adantr	$⊢ (φ \land Z \in (Y Itv (G) X)) \to A \in P$
33	8	adantr	$⊢ (φ \land Z \in (Y Itv (G) X)) \to Y \in P$
34	9	adantr	$⊢ (φ \land Z \in (Y Itv (G) X)) \to Z \in P$
35	7	adantr	$⊢ (φ \land Z \in (Y Itv (G) X)) \to X \in P$
36		simpr	$⊢ (φ \land Z \in (Y Itv (G) X)) \to Z \in (Y Itv (G) X)$
37	1 16 12 2 3 31 32 4 33 34 35 36	mirbtwni	$⊢ (φ \land Z \in (Y Itv (G) X)) \to M (Z) \in (M (Y) Itv (G) M (X))$
38	15 23 30 37	3orim123da	$⊢ φ \to (M (X) \in (M (Y) Itv (G) M (Z)) \lor M (Y) \in (M (X) Itv (G) M (Z)) \lor M (Z) \in (M (Y) Itv (G) M (X)))$
39	1 16 12 2 3 5 6 4 8	mircl	$⊢ φ \to M (Y) \in P$
40	1 16 12 2 3 5 6 4 9	mircl	$⊢ φ \to M (Z) \in P$
41	1 3 4 5 6 8 9	mirleqb	$⊢ φ \to (Y = Z \leftrightarrow M (Y) = M (Z))$
42	41	necon3bid	$⊢ φ \to (Y \neq Z \leftrightarrow M (Y) \neq M (Z))$
43	13 42	mpbid	$⊢ φ \to M (Y) \neq M (Z)$
44	1 16 12 2 3 5 6 4 7	mircl	$⊢ φ \to M (X) \in P$
45	1 2 12 5 39 40 43 44	tgellng	$⊢ φ \to (M (X) \in (M (Y) L M (Z)) \leftrightarrow (M (X) \in (M (Y) Itv (G) M (Z)) \lor M (Y) \in (M (X) Itv (G) M (Z)) \lor M (Z) \in (M (Y) Itv (G) M (X))))$
46	38 45	mpbird	$⊢ φ \to M (X) \in (M (Y) L M (Z))$

Metamath Proof Explorer

Theorem mirlni

Proof