Metamath Proof Explorer

Theorem lmiinv

Description: The invariants of the line mirroring lie on the mirror line. Theorem 10.8 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$
	Assertion	lmiinv	$⊢ φ \to (M (A) = A \leftrightarrow A \in D)$

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	1 2 3 4 5 6 7 8 9 9	islmib	$⊢ φ \to (A = M (A) \leftrightarrow (A {mid}_{𝒢} (G) A \in D \land (D ⟂_{𝒢} (G) (A L A) \lor A = A)))$
11		eqcom	$⊢ A = M (A) \leftrightarrow M (A) = A$
12	11	a1i	$⊢ φ \to (A = M (A) \leftrightarrow M (A) = A)$
13		eqidd	$⊢ φ \to A = A$
14	13	olcd	$⊢ φ \to (D ⟂_{𝒢} (G) (A L A) \lor A = A)$
15	14	biantrud	$⊢ φ \to (A {mid}_{𝒢} (G) A \in D \leftrightarrow (A {mid}_{𝒢} (G) A \in D \land (D ⟂_{𝒢} (G) (A L A) \lor A = A)))$
16	1 2 3 4 5 9 9	midid	$⊢ φ \to A {mid}_{𝒢} (G) A = A$
17	16	eleq1d	$⊢ φ \to (A {mid}_{𝒢} (G) A \in D \leftrightarrow A \in D)$
18	15 17	bitr3d	$⊢ φ \to ((A {mid}_{𝒢} (G) A \in D \land (D ⟂_{𝒢} (G) (A L A) \lor A = A)) \leftrightarrow A \in D)$
19	10 12 18	3bitr3d	$⊢ φ \to (M (A) = A \leftrightarrow A \in D)$