Metamath Proof Explorer

Theorem mirval

Description: Value of the point inversion function S . 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 )
Assertion mirval 
|- ( ph -> ( S ` A ) = ( y e. P |-> ( iota_ z e. P ( ( A .- z ) = ( A .- y ) /\ A e. ( z I y ) ) ) ) )

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 df-mir 
 |-  pInvG = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( y e. ( Base ` g ) |-> ( iota_ z e. ( Base ` g ) ( ( x ( dist ` g ) z ) = ( x ( dist ` g ) y ) /\ x e. ( z ( Itv ` g ) y ) ) ) ) ) )
9 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
10 9 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = P )
11 fveq2 
 |-  ( g = G -> ( dist ` g ) = ( dist ` G ) )
12 11 2 eqtr4di 
 |-  ( g = G -> ( dist ` g ) = .- )
13 12 oveqd 
 |-  ( g = G -> ( x ( dist ` g ) z ) = ( x .- z ) )
14 12 oveqd 
 |-  ( g = G -> ( x ( dist ` g ) y ) = ( x .- y ) )
15 13 14 eqeq12d 
 |-  ( g = G -> ( ( x ( dist ` g ) z ) = ( x ( dist ` g ) y ) <-> ( x .- z ) = ( x .- y ) ) )
16 fveq2 
 |-  ( g = G -> ( Itv ` g ) = ( Itv ` G ) )
17 16 3 eqtr4di 
 |-  ( g = G -> ( Itv ` g ) = I )
18 17 oveqd 
 |-  ( g = G -> ( z ( Itv ` g ) y ) = ( z I y ) )
19 18 eleq2d 
 |-  ( g = G -> ( x e. ( z ( Itv ` g ) y ) <-> x e. ( z I y ) ) )
20 15 19 anbi12d 
 |-  ( g = G -> ( ( ( x ( dist ` g ) z ) = ( x ( dist ` g ) y ) /\ x e. ( z ( Itv ` g ) y ) ) <-> ( ( x .- z ) = ( x .- y ) /\ x e. ( z I y ) ) ) )
21 10 20 riotaeqbidv 
 |-  ( g = G -> ( iota_ z e. ( Base ` g ) ( ( x ( dist ` g ) z ) = ( x ( dist ` g ) y ) /\ x e. ( z ( Itv ` g ) y ) ) ) = ( iota_ z e. P ( ( x .- z ) = ( x .- y ) /\ x e. ( z I y ) ) ) )
22 10 21 mpteq12dv 
 |-  ( g = G -> ( y e. ( Base ` g ) |-> ( iota_ z e. ( Base ` g ) ( ( x ( dist ` g ) z ) = ( x ( dist ` g ) y ) /\ x e. ( z ( Itv ` g ) y ) ) ) ) = ( y e. P |-> ( iota_ z e. P ( ( x .- z ) = ( x .- y ) /\ x e. ( z I y ) ) ) ) )
23 10 22 mpteq12dv 
 |-  ( g = G -> ( x e. ( Base ` g ) |-> ( y e. ( Base ` g ) |-> ( iota_ z e. ( Base ` g ) ( ( x ( dist ` g ) z ) = ( x ( dist ` g ) y ) /\ x e. ( z ( Itv ` g ) y ) ) ) ) ) = ( x e. P |-> ( y e. P |-> ( iota_ z e. P ( ( x .- z ) = ( x .- y ) /\ x e. ( z I y ) ) ) ) ) )
24 6 elexd 
 |-  ( ph -> G e. _V )
25 1 fvexi 
 |-  P e. _V
26 25 mptex 
 |-  ( x e. P |-> ( y e. P |-> ( iota_ z e. P ( ( x .- z ) = ( x .- y ) /\ x e. ( z I y ) ) ) ) ) e. _V
27 26 a1i 
 |-  ( ph -> ( x e. P |-> ( y e. P |-> ( iota_ z e. P ( ( x .- z ) = ( x .- y ) /\ x e. ( z I y ) ) ) ) ) e. _V )
28 8 23 24 27 fvmptd3 
 |-  ( ph -> ( pInvG ` G ) = ( x e. P |-> ( y e. P |-> ( iota_ z e. P ( ( x .- z ) = ( x .- y ) /\ x e. ( z I y ) ) ) ) ) )
29 5 28 eqtrid 
 |-  ( ph -> S = ( x e. P |-> ( y e. P |-> ( iota_ z e. P ( ( x .- z ) = ( x .- y ) /\ x e. ( z I y ) ) ) ) ) )
30 simpll 
 |-  ( ( ( x = A /\ y e. P ) /\ z e. P ) -> x = A )
31 30 oveq1d 
 |-  ( ( ( x = A /\ y e. P ) /\ z e. P ) -> ( x .- z ) = ( A .- z ) )
32 30 oveq1d 
 |-  ( ( ( x = A /\ y e. P ) /\ z e. P ) -> ( x .- y ) = ( A .- y ) )
33 31 32 eqeq12d 
 |-  ( ( ( x = A /\ y e. P ) /\ z e. P ) -> ( ( x .- z ) = ( x .- y ) <-> ( A .- z ) = ( A .- y ) ) )
34 30 eleq1d 
 |-  ( ( ( x = A /\ y e. P ) /\ z e. P ) -> ( x e. ( z I y ) <-> A e. ( z I y ) ) )
35 33 34 anbi12d 
 |-  ( ( ( x = A /\ y e. P ) /\ z e. P ) -> ( ( ( x .- z ) = ( x .- y ) /\ x e. ( z I y ) ) <-> ( ( A .- z ) = ( A .- y ) /\ A e. ( z I y ) ) ) )
36 35 riotabidva 
 |-  ( ( x = A /\ y e. P ) -> ( iota_ z e. P ( ( x .- z ) = ( x .- y ) /\ x e. ( z I y ) ) ) = ( iota_ z e. P ( ( A .- z ) = ( A .- y ) /\ A e. ( z I y ) ) ) )
37 36 mpteq2dva 
 |-  ( x = A -> ( y e. P |-> ( iota_ z e. P ( ( x .- z ) = ( x .- y ) /\ x e. ( z I y ) ) ) ) = ( y e. P |-> ( iota_ z e. P ( ( A .- z ) = ( A .- y ) /\ A e. ( z I y ) ) ) ) )
38 37 adantl 
 |-  ( ( ph /\ x = A ) -> ( y e. P |-> ( iota_ z e. P ( ( x .- z ) = ( x .- y ) /\ x e. ( z I y ) ) ) ) = ( y e. P |-> ( iota_ z e. P ( ( A .- z ) = ( A .- y ) /\ A e. ( z I y ) ) ) ) )
39 25 mptex 
 |-  ( y e. P |-> ( iota_ z e. P ( ( A .- z ) = ( A .- y ) /\ A e. ( z I y ) ) ) ) e. _V
40 39 a1i 
 |-  ( ph -> ( y e. P |-> ( iota_ z e. P ( ( A .- z ) = ( A .- y ) /\ A e. ( z I y ) ) ) ) e. _V )
41 29 38 7 40 fvmptd 
 |-  ( ph -> ( S ` A ) = ( y e. P |-> ( iota_ z e. P ( ( A .- z ) = ( A .- y ) /\ A e. ( z I y ) ) ) ) )