Metamath Proof Explorer


Theorem mircom

Description: Variation on mirmir . (Contributed by Thierry Arnoux, 10-Nov-2019)

Ref Expression
Hypotheses mirval.p 𝑃 = ( Base ‘ 𝐺 )
mirval.d = ( dist ‘ 𝐺 )
mirval.i 𝐼 = ( Itv ‘ 𝐺 )
mirval.l 𝐿 = ( LineG ‘ 𝐺 )
mirval.s 𝑆 = ( pInvG ‘ 𝐺 )
mirval.g ( 𝜑𝐺 ∈ TarskiG )
mirval.a ( 𝜑𝐴𝑃 )
mirfv.m 𝑀 = ( 𝑆𝐴 )
mirmir.b ( 𝜑𝐵𝑃 )
mircom.1 ( 𝜑 → ( 𝑀𝐵 ) = 𝐶 )
Assertion mircom ( 𝜑 → ( 𝑀𝐶 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 mirval.p 𝑃 = ( Base ‘ 𝐺 )
2 mirval.d = ( dist ‘ 𝐺 )
3 mirval.i 𝐼 = ( Itv ‘ 𝐺 )
4 mirval.l 𝐿 = ( LineG ‘ 𝐺 )
5 mirval.s 𝑆 = ( pInvG ‘ 𝐺 )
6 mirval.g ( 𝜑𝐺 ∈ TarskiG )
7 mirval.a ( 𝜑𝐴𝑃 )
8 mirfv.m 𝑀 = ( 𝑆𝐴 )
9 mirmir.b ( 𝜑𝐵𝑃 )
10 mircom.1 ( 𝜑 → ( 𝑀𝐵 ) = 𝐶 )
11 10 fveq2d ( 𝜑 → ( 𝑀 ‘ ( 𝑀𝐵 ) ) = ( 𝑀𝐶 ) )
12 1 2 3 4 5 6 7 8 9 mirmir ( 𝜑 → ( 𝑀 ‘ ( 𝑀𝐵 ) ) = 𝐵 )
13 11 12 eqtr3d ( 𝜑 → ( 𝑀𝐶 ) = 𝐵 )