lmireu

Description: Any point has a unique antecedent through line mirroring. Theorem 10.6 of Schwabhauser p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019)

	Ref	Expression
Hypotheses	ismid.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	ismid.d	⊢ − = ( dist ‘ 𝐺 )
	ismid.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	ismid.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	ismid.1	⊢ ( 𝜑 → 𝐺 Dim_TarskiG≥ 2 )
	lmif.m	⊢ 𝑀 = ( ( lInvG ‘ 𝐺 ) ‘ 𝐷 )
	lmif.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	lmif.d	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
	lmicl.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
Assertion	lmireu	⊢ ( 𝜑 → ∃! 𝑏 ∈ 𝑃 ( 𝑀 ‘ 𝑏 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ismid.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		ismid.d	⊢ − = ( dist ‘ 𝐺 )
3		ismid.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		ismid.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		ismid.1	⊢ ( 𝜑 → 𝐺 Dim_TarskiG≥ 2 )
6		lmif.m	⊢ 𝑀 = ( ( lInvG ‘ 𝐺 ) ‘ 𝐷 )
7		lmif.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
8		lmif.d	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
9		lmicl.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
10	1 2 3 4 5 6 7 8 9	lmicl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ 𝑃 )
11	1 2 3 4 5 6 7 8 9	lmilmi	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = 𝐴 )
12	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑀 ‘ 𝑏 ) = 𝐴 ) → 𝐺 ∈ TarskiG )
13	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑀 ‘ 𝑏 ) = 𝐴 ) → 𝐺 Dim_TarskiG≥ 2 )
14	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑀 ‘ 𝑏 ) = 𝐴 ) → 𝐷 ∈ ran 𝐿 )
15		simplr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑀 ‘ 𝑏 ) = 𝐴 ) → 𝑏 ∈ 𝑃 )
16	1 2 3 12 13 6 7 14 15	lmilmi	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑀 ‘ 𝑏 ) = 𝐴 ) → ( 𝑀 ‘ ( 𝑀 ‘ 𝑏 ) ) = 𝑏 )
17		simpr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑀 ‘ 𝑏 ) = 𝐴 ) → ( 𝑀 ‘ 𝑏 ) = 𝐴 )
18	17	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑀 ‘ 𝑏 ) = 𝐴 ) → ( 𝑀 ‘ ( 𝑀 ‘ 𝑏 ) ) = ( 𝑀 ‘ 𝐴 ) )
19	16 18	eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑀 ‘ 𝑏 ) = 𝐴 ) → 𝑏 = ( 𝑀 ‘ 𝐴 ) )
20	19	ex	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑃 ) → ( ( 𝑀 ‘ 𝑏 ) = 𝐴 → 𝑏 = ( 𝑀 ‘ 𝐴 ) ) )
21	20	ralrimiva	⊢ ( 𝜑 → ∀ 𝑏 ∈ 𝑃 ( ( 𝑀 ‘ 𝑏 ) = 𝐴 → 𝑏 = ( 𝑀 ‘ 𝐴 ) ) )
22		fveqeq2	⊢ ( 𝑏 = ( 𝑀 ‘ 𝐴 ) → ( ( 𝑀 ‘ 𝑏 ) = 𝐴 ↔ ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = 𝐴 ) )
23	22	eqreu	⊢ ( ( ( 𝑀 ‘ 𝐴 ) ∈ 𝑃 ∧ ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = 𝐴 ∧ ∀ 𝑏 ∈ 𝑃 ( ( 𝑀 ‘ 𝑏 ) = 𝐴 → 𝑏 = ( 𝑀 ‘ 𝐴 ) ) ) → ∃! 𝑏 ∈ 𝑃 ( 𝑀 ‘ 𝑏 ) = 𝐴 )
24	10 11 21 23	syl3anc	⊢ ( 𝜑 → ∃! 𝑏 ∈ 𝑃 ( 𝑀 ‘ 𝑏 ) = 𝐴 )

Metamath Proof Explorer

Theorem lmireu

Proof