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 ) |
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 ) |