lmicom

Description: The line mirroring function is an involution. Theorem 10.4 of Schwabhauser p. 89. (Contributed by Thierry Arnoux, 11-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$
	islmib.b	$⊢ φ \to B \in P$
	lmicom.1	$⊢ φ \to M (A) = B$
Assertion	lmicom	$⊢ φ \to M (B) = A$

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		islmib.b	$⊢ φ \to B \in P$
11		lmicom.1	$⊢ φ \to M (A) = B$
12	1 2 3 4 5 9 10	midcom	$⊢ φ \to A {mid}_{𝒢} (G) B = B {mid}_{𝒢} (G) A$
13	11	eqcomd	$⊢ φ \to B = M (A)$
14	1 2 3 4 5 6 7 8 9 10	islmib	$⊢ φ \to (B = M (A) \leftrightarrow (A {mid}_{𝒢} (G) B \in D \land (D ⟂_{𝒢} (G) (A L B) \lor A = B)))$
15	13 14	mpbid	$⊢ φ \to (A {mid}_{𝒢} (G) B \in D \land (D ⟂_{𝒢} (G) (A L B) \lor A = B))$
16	15	simpld	$⊢ φ \to A {mid}_{𝒢} (G) B \in D$
17	12 16	eqeltrrd	$⊢ φ \to B {mid}_{𝒢} (G) A \in D$
18	15	simprd	$⊢ φ \to (D ⟂_{𝒢} (G) (A L B) \lor A = B)$
19	18	orcomd	$⊢ φ \to (A = B \lor D ⟂_{𝒢} (G) (A L B))$
20	19	ord	$⊢ φ \to (\neg A = B \to D ⟂_{𝒢} (G) (A L B))$
21	4	adantr	$⊢ (φ \land \neg A = B) \to G \in 𝒢_{Tarski}$
22	9	adantr	$⊢ (φ \land \neg A = B) \to A \in P$
23	10	adantr	$⊢ (φ \land \neg A = B) \to B \in P$
24		simpr	$⊢ (φ \land \neg A = B) \to \neg A = B$
25	24	neqned	$⊢ (φ \land \neg A = B) \to A \neq B$
26	1 3 7 21 22 23 25	tglinecom	$⊢ (φ \land \neg A = B) \to A L B = B L A$
27	26	breq2d	$⊢ (φ \land \neg A = B) \to (D ⟂_{𝒢} (G) (A L B) \leftrightarrow D ⟂_{𝒢} (G) (B L A))$
28	27	pm5.74da	$⊢ φ \to ((\neg A = B \to D ⟂_{𝒢} (G) (A L B)) \leftrightarrow (\neg A = B \to D ⟂_{𝒢} (G) (B L A)))$
29	20 28	mpbid	$⊢ φ \to (\neg A = B \to D ⟂_{𝒢} (G) (B L A))$
30	29	orrd	$⊢ φ \to (A = B \lor D ⟂_{𝒢} (G) (B L A))$
31	30	orcomd	$⊢ φ \to (D ⟂_{𝒢} (G) (B L A) \lor A = B)$
32		eqcom	$⊢ A = B \leftrightarrow B = A$
33	32	orbi2i	$⊢ (D ⟂_{𝒢} (G) (B L A) \lor A = B) \leftrightarrow (D ⟂_{𝒢} (G) (B L A) \lor B = A)$
34	31 33	sylib	$⊢ φ \to (D ⟂_{𝒢} (G) (B L A) \lor B = A)$
35	1 2 3 4 5 6 7 8 10 9	islmib	$⊢ φ \to (A = M (B) \leftrightarrow (B {mid}_{𝒢} (G) A \in D \land (D ⟂_{𝒢} (G) (B L A) \lor B = A)))$
36	17 34 35	mpbir2and	$⊢ φ \to A = M (B)$
37	36	eqcomd	$⊢ φ \to M (B) = A$

Metamath Proof Explorer

Theorem lmicom

Proof