Metamath Proof Explorer


Theorem lmieq

Description: Equality deduction for line mirroring. Theorem 10.7 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 ( 𝜑𝐺 DimTarskiG≥ 2 )
lmif.m 𝑀 = ( ( lInvG ‘ 𝐺 ) ‘ 𝐷 )
lmif.l 𝐿 = ( LineG ‘ 𝐺 )
lmif.d ( 𝜑𝐷 ∈ ran 𝐿 )
lmicl.1 ( 𝜑𝐴𝑃 )
lmieq.c ( 𝜑𝐵𝑃 )
lmieq.d ( 𝜑 → ( 𝑀𝐴 ) = ( 𝑀𝐵 ) )
Assertion lmieq ( 𝜑𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 ismid.p 𝑃 = ( Base ‘ 𝐺 )
2 ismid.d = ( dist ‘ 𝐺 )
3 ismid.i 𝐼 = ( Itv ‘ 𝐺 )
4 ismid.g ( 𝜑𝐺 ∈ TarskiG )
5 ismid.1 ( 𝜑𝐺 DimTarskiG≥ 2 )
6 lmif.m 𝑀 = ( ( lInvG ‘ 𝐺 ) ‘ 𝐷 )
7 lmif.l 𝐿 = ( LineG ‘ 𝐺 )
8 lmif.d ( 𝜑𝐷 ∈ ran 𝐿 )
9 lmicl.1 ( 𝜑𝐴𝑃 )
10 lmieq.c ( 𝜑𝐵𝑃 )
11 lmieq.d ( 𝜑 → ( 𝑀𝐴 ) = ( 𝑀𝐵 ) )
12 fveqeq2 ( 𝑏 = 𝐴 → ( ( 𝑀𝑏 ) = ( 𝑀𝐵 ) ↔ ( 𝑀𝐴 ) = ( 𝑀𝐵 ) ) )
13 fveqeq2 ( 𝑏 = 𝐵 → ( ( 𝑀𝑏 ) = ( 𝑀𝐵 ) ↔ ( 𝑀𝐵 ) = ( 𝑀𝐵 ) ) )
14 1 2 3 4 5 6 7 8 10 lmicl ( 𝜑 → ( 𝑀𝐵 ) ∈ 𝑃 )
15 1 2 3 4 5 6 7 8 14 lmireu ( 𝜑 → ∃! 𝑏𝑃 ( 𝑀𝑏 ) = ( 𝑀𝐵 ) )
16 eqidd ( 𝜑 → ( 𝑀𝐵 ) = ( 𝑀𝐵 ) )
17 12 13 15 9 10 11 16 reu2eqd ( 𝜑𝐴 = 𝐵 )