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