Theorem lmiopp

Description: Line mirroring produces points on the opposite side of the mirroring line. Theorem 10.14 of Schwabhauser p. 92. (Contributed by Thierry Arnoux, 2-Aug-2020)

	Ref	Expression
Hypotheses	lmiopp.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	lmiopp.m	⊢ − = ( dist ‘ 𝐺 )
	lmiopp.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	lmiopp.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	lmiopp.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	lmiopp.h	⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
	lmiopp.d	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
	lmiopp.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
	lmiopp.n	⊢ 𝑀 = ( ( lInvG ‘ 𝐺 ) ‘ 𝐷 )
	lmiopp.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	lmiopp.1	⊢ ( 𝜑 → ¬ 𝐴 ∈ 𝐷 )
Assertion	lmiopp	⊢ ( 𝜑 → 𝐴 𝑂 ( 𝑀 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		lmiopp.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		lmiopp.m	⊢ − = ( dist ‘ 𝐺 )
3		lmiopp.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		lmiopp.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		lmiopp.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6		lmiopp.h	⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
7		lmiopp.d	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
8		lmiopp.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
9		lmiopp.n	⊢ 𝑀 = ( ( lInvG ‘ 𝐺 ) ‘ 𝐷 )
10		lmiopp.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
11		lmiopp.1	⊢ ( 𝜑 → ¬ 𝐴 ∈ 𝐷 )
12	1 2 3 5 6 9 4 7 10	lmicl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ 𝑃 )
13		eqidd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = ( 𝑀 ‘ 𝐴 ) )
14	1 2 3 5 6 9 4 7 10 12	islmib	⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) = ( 𝑀 ‘ 𝐴 ) ↔ ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 ( 𝑀 ‘ 𝐴 ) ) ∨ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) ) ) )
15	13 14	mpbid	⊢ ( 𝜑 → ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 ( 𝑀 ‘ 𝐴 ) ) ∨ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) ) )
16	15	simpld	⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ∈ 𝐷 )
17	1 2 3 5 6 9 4 7 10	lmilmi	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = 𝐴 )
18	17	eqeq1d	⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝑀 ‘ 𝐴 ) ↔ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) )
19	1 2 3 5 6 9 4 7 12	lmiinv	⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝑀 ‘ 𝐴 ) ↔ ( 𝑀 ‘ 𝐴 ) ∈ 𝐷 ) )
20		eqcom	⊢ ( 𝐴 = ( 𝑀 ‘ 𝐴 ) ↔ ( 𝑀 ‘ 𝐴 ) = 𝐴 )
21	20	a1i	⊢ ( 𝜑 → ( 𝐴 = ( 𝑀 ‘ 𝐴 ) ↔ ( 𝑀 ‘ 𝐴 ) = 𝐴 ) )
22	18 19 21	3bitr3d	⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) ∈ 𝐷 ↔ ( 𝑀 ‘ 𝐴 ) = 𝐴 ) )
23	1 2 3 5 6 9 4 7 10	lmiinv	⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) = 𝐴 ↔ 𝐴 ∈ 𝐷 ) )
24	22 23	bitrd	⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) ∈ 𝐷 ↔ 𝐴 ∈ 𝐷 ) )
25	11 24	mtbird	⊢ ( 𝜑 → ¬ ( 𝑀 ‘ 𝐴 ) ∈ 𝐷 )
26	1 2 3 5 6 10 12	midbtwn	⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ∈ ( 𝐴 𝐼 ( 𝑀 ‘ 𝐴 ) ) )
27	1 2 3 8 10 12 16 11 25 26	islnoppd	⊢ ( 𝜑 → 𝐴 𝑂 ( 𝑀 ‘ 𝐴 ) )