Metamath Proof Explorer

Theorem mirfv

Description: Value of the point inversion function M . Definition 7.5 of Schwabhauser p. 49. (Contributed by Thierry Arnoux, 30-May-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 )
mirfv.b 
|- ( ph -> B e. P )
Assertion mirfv 
|- ( ph -> ( M ` B ) = ( iota_ z e. P ( ( A .- z ) = ( A .- B ) /\ A e. ( z I 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 mirfv.b 
 |-  ( ph -> B e. P )
10 1 2 3 4 5 6 7 mirval 
 |-  ( ph -> ( S ` A ) = ( y e. P |-> ( iota_ z e. P ( ( A .- z ) = ( A .- y ) /\ A e. ( z I y ) ) ) ) )
11 8 10 syl5eq 
 |-  ( ph -> M = ( y e. P |-> ( iota_ z e. P ( ( A .- z ) = ( A .- y ) /\ A e. ( z I y ) ) ) ) )
12 simplr 
 |-  ( ( ( ph /\ y = B ) /\ z e. P ) -> y = B )
13 12 oveq2d 
 |-  ( ( ( ph /\ y = B ) /\ z e. P ) -> ( A .- y ) = ( A .- B ) )
14 13 eqeq2d 
 |-  ( ( ( ph /\ y = B ) /\ z e. P ) -> ( ( A .- z ) = ( A .- y ) <-> ( A .- z ) = ( A .- B ) ) )
15 12 oveq2d 
 |-  ( ( ( ph /\ y = B ) /\ z e. P ) -> ( z I y ) = ( z I B ) )
16 15 eleq2d 
 |-  ( ( ( ph /\ y = B ) /\ z e. P ) -> ( A e. ( z I y ) <-> A e. ( z I B ) ) )
17 14 16 anbi12d 
 |-  ( ( ( ph /\ y = B ) /\ z e. P ) -> ( ( ( A .- z ) = ( A .- y ) /\ A e. ( z I y ) ) <-> ( ( A .- z ) = ( A .- B ) /\ A e. ( z I B ) ) ) )
18 17 riotabidva 
 |-  ( ( ph /\ y = B ) -> ( iota_ z e. P ( ( A .- z ) = ( A .- y ) /\ A e. ( z I y ) ) ) = ( iota_ z e. P ( ( A .- z ) = ( A .- B ) /\ A e. ( z I B ) ) ) )
19 riotaex 
 |-  ( iota_ z e. P ( ( A .- z ) = ( A .- B ) /\ A e. ( z I B ) ) ) e. _V
20 19 a1i 
 |-  ( ph -> ( iota_ z e. P ( ( A .- z ) = ( A .- B ) /\ A e. ( z I B ) ) ) e. _V )
21 11 18 9 20 fvmptd 
 |-  ( ph -> ( M ` B ) = ( iota_ z e. P ( ( A .- z ) = ( A .- B ) /\ A e. ( z I B ) ) ) )