lmimid

Description: If we have a right angle, then the mirror point is the point inversion. (Contributed by Thierry Arnoux, 15-Dec-2019)

	Ref	Expression
Hypotheses	ismid.p	$⊢ P = {Base}_{G}$
	ismid.d	$⊢ \underset{˙}{-} = dist (G)$
	ismid.i	$⊢ I = Itv (G)$
	ismid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	ismid.1	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
	lmif.m	$⊢ M = {lInv}_{𝒢} (G) (D)$
	lmif.l	$⊢ L = {Line}_{𝒢} (G)$
	lmif.d	$⊢ φ \to D \in ran L$
	lmicl.1	$⊢ φ \to A \in P$
	lmimid.s	$⊢ S = {pInv}_{𝒢} (G) (B)$
	lmimid.r	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
	lmimid.a	$⊢ φ \to A \in D$
	lmimid.b	$⊢ φ \to B \in D$
	lmimid.c	$⊢ φ \to C \in P$
	lmimid.d	$⊢ φ \to A \neq B$
Assertion	lmimid	$⊢ φ \to M (C) = S (C)$

Proof

Step	Hyp	Ref	Expression
1		ismid.p	$⊢ P = {Base}_{G}$
2		ismid.d	$⊢ \underset{˙}{-} = dist (G)$
3		ismid.i	$⊢ I = Itv (G)$
4		ismid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		ismid.1	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
6		lmif.m	$⊢ M = {lInv}_{𝒢} (G) (D)$
7		lmif.l	$⊢ L = {Line}_{𝒢} (G)$
8		lmif.d	$⊢ φ \to D \in ran L$
9		lmicl.1	$⊢ φ \to A \in P$
10		lmimid.s	$⊢ S = {pInv}_{𝒢} (G) (B)$
11		lmimid.r	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
12		lmimid.a	$⊢ φ \to A \in D$
13		lmimid.b	$⊢ φ \to B \in D$
14		lmimid.c	$⊢ φ \to C \in P$
15		lmimid.d	$⊢ φ \to A \neq B$
16	10	a1i	$⊢ φ \to S = {pInv}_{𝒢} (G) (B)$
17	16	fveq1d	$⊢ φ \to S (C) = {pInv}_{𝒢} (G) (B) (C)$
18		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
19	1 7 3 4 8 13	tglnpt	$⊢ φ \to B \in P$
20	1 2 3 7 18 4 19 10 14	mircl	$⊢ φ \to S (C) \in P$
21	1 2 3 4 5 14 20 18 19	ismidb	$⊢ φ \to (S (C) = {pInv}_{𝒢} (G) (B) (C) \leftrightarrow C {mid}_{𝒢} (G) S (C) = B)$
22	17 21	mpbid	$⊢ φ \to C {mid}_{𝒢} (G) S (C) = B$
23	22 13	eqeltrd	$⊢ φ \to C {mid}_{𝒢} (G) S (C) \in D$
24		df-ne	$⊢ C \neq S (C) \leftrightarrow \neg C = S (C)$
25	4	adantr	$⊢ (φ \land C \neq S (C)) \to G \in 𝒢_{Tarski}$
26	8	adantr	$⊢ (φ \land C \neq S (C)) \to D \in ran L$
27	14	adantr	$⊢ (φ \land C \neq S (C)) \to C \in P$
28	20	adantr	$⊢ (φ \land C \neq S (C)) \to S (C) \in P$
29		simpr	$⊢ (φ \land C \neq S (C)) \to C \neq S (C)$
30	1 3 7 25 27 28 29	tgelrnln	$⊢ (φ \land C \neq S (C)) \to C L S (C) \in ran L$
31	13	adantr	$⊢ (φ \land C \neq S (C)) \to B \in D$
32	19	adantr	$⊢ (φ \land C \neq S (C)) \to B \in P$
33	1 2 3 4 5 14 20	midbtwn	$⊢ φ \to C {mid}_{𝒢} (G) S (C) \in (C I S (C))$
34	22 33	eqeltrrd	$⊢ φ \to B \in (C I S (C))$
35	34	adantr	$⊢ (φ \land C \neq S (C)) \to B \in (C I S (C))$
36	1 3 7 25 27 28 32 29 35	btwnlng1	$⊢ (φ \land C \neq S (C)) \to B \in (C L S (C))$
37	31 36	elind	$⊢ (φ \land C \neq S (C)) \to B \in (D \cap (C L S (C)))$
38	12	adantr	$⊢ (φ \land C \neq S (C)) \to A \in D$
39	1 3 7 25 27 28 29	tglinerflx1	$⊢ (φ \land C \neq S (C)) \to C \in (C L S (C))$
40	15	adantr	$⊢ (φ \land C \neq S (C)) \to A \neq B$
41	1 2 3 7 18 4 19 10 14	mirinv	$⊢ φ \to (S (C) = C \leftrightarrow B = C)$
42		eqcom	$⊢ B = C \leftrightarrow C = B$
43	41 42	bitrdi	$⊢ φ \to (S (C) = C \leftrightarrow C = B)$
44	43	biimpar	$⊢ (φ \land C = B) \to S (C) = C$
45	44	eqcomd	$⊢ (φ \land C = B) \to C = S (C)$
46	45	ex	$⊢ φ \to (C = B \to C = S (C))$
47	46	necon3d	$⊢ φ \to (C \neq S (C) \to C \neq B)$
48	47	imp	$⊢ (φ \land C \neq S (C)) \to C \neq B$
49	11	adantr	$⊢ (φ \land C \neq S (C)) \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
50	1 2 3 7 25 26 30 37 38 39 40 48 49	ragperp	$⊢ (φ \land C \neq S (C)) \to D ⟂_{𝒢} (G) (C L S (C))$
51	50	ex	$⊢ φ \to (C \neq S (C) \to D ⟂_{𝒢} (G) (C L S (C)))$
52	24 51	syl5bir	$⊢ φ \to (\neg C = S (C) \to D ⟂_{𝒢} (G) (C L S (C)))$
53	52	orrd	$⊢ φ \to (C = S (C) \lor D ⟂_{𝒢} (G) (C L S (C)))$
54	53	orcomd	$⊢ φ \to (D ⟂_{𝒢} (G) (C L S (C)) \lor C = S (C))$
55	1 2 3 4 5 6 7 8 14 20	islmib	$⊢ φ \to (S (C) = M (C) \leftrightarrow (C {mid}_{𝒢} (G) S (C) \in D \land (D ⟂_{𝒢} (G) (C L S (C)) \lor C = S (C))))$
56	23 54 55	mpbir2and	$⊢ φ \to S (C) = M (C)$
57	56	eqcomd	$⊢ φ \to M (C) = S (C)$

Metamath Proof Explorer

Theorem lmimid

Proof