Metamath Proof Explorer


Theorem mircom

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

Ref Expression
Hypotheses mirval.p
|- P = ( Base ` G )
mirval.d
|- .- = ( dist ` G )
mirval.i
|- I = ( Itv ` G )
mirval.l
|- L = ( LineG ` G )
mirval.s
|- S = ( pInvG ` G )
mirval.g
|- ( ph -> G e. TarskiG )
mirval.a
|- ( ph -> A e. P )
mirfv.m
|- M = ( S ` A )
mirmir.b
|- ( ph -> B e. P )
mircom.1
|- ( ph -> ( M ` B ) = C )
Assertion mircom
|- ( ph -> ( M ` C ) = B )

Proof

Step Hyp Ref Expression
1 mirval.p
 |-  P = ( Base ` G )
2 mirval.d
 |-  .- = ( dist ` G )
3 mirval.i
 |-  I = ( Itv ` G )
4 mirval.l
 |-  L = ( LineG ` G )
5 mirval.s
 |-  S = ( pInvG ` G )
6 mirval.g
 |-  ( ph -> G e. TarskiG )
7 mirval.a
 |-  ( ph -> A e. P )
8 mirfv.m
 |-  M = ( S ` A )
9 mirmir.b
 |-  ( ph -> B e. P )
10 mircom.1
 |-  ( ph -> ( M ` B ) = C )
11 10 fveq2d
 |-  ( ph -> ( M ` ( M ` B ) ) = ( M ` C ) )
12 1 2 3 4 5 6 7 8 9 mirmir
 |-  ( ph -> ( M ` ( M ` B ) ) = B )
13 11 12 eqtr3d
 |-  ( ph -> ( M ` C ) = B )