Step |
Hyp |
Ref |
Expression |
1 |
|
ismot.p |
|- P = ( Base ` G ) |
2 |
|
ismot.m |
|- .- = ( dist ` G ) |
3 |
|
motgrp.1 |
|- ( ph -> G e. V ) |
4 |
|
motco.2 |
|- ( ph -> F e. ( G Ismt G ) ) |
5 |
|
motco.3 |
|- ( ph -> H e. ( G Ismt G ) ) |
6 |
1 2 3 4
|
motf1o |
|- ( ph -> F : P -1-1-onto-> P ) |
7 |
1 2 3 5
|
motf1o |
|- ( ph -> H : P -1-1-onto-> P ) |
8 |
|
f1oco |
|- ( ( F : P -1-1-onto-> P /\ H : P -1-1-onto-> P ) -> ( F o. H ) : P -1-1-onto-> P ) |
9 |
6 7 8
|
syl2anc |
|- ( ph -> ( F o. H ) : P -1-1-onto-> P ) |
10 |
|
f1of |
|- ( H : P -1-1-onto-> P -> H : P --> P ) |
11 |
7 10
|
syl |
|- ( ph -> H : P --> P ) |
12 |
11
|
adantr |
|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> H : P --> P ) |
13 |
|
simprl |
|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> a e. P ) |
14 |
|
fvco3 |
|- ( ( H : P --> P /\ a e. P ) -> ( ( F o. H ) ` a ) = ( F ` ( H ` a ) ) ) |
15 |
12 13 14
|
syl2anc |
|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( F o. H ) ` a ) = ( F ` ( H ` a ) ) ) |
16 |
|
simprr |
|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> b e. P ) |
17 |
|
fvco3 |
|- ( ( H : P --> P /\ b e. P ) -> ( ( F o. H ) ` b ) = ( F ` ( H ` b ) ) ) |
18 |
12 16 17
|
syl2anc |
|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( F o. H ) ` b ) = ( F ` ( H ` b ) ) ) |
19 |
15 18
|
oveq12d |
|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( ( F o. H ) ` a ) .- ( ( F o. H ) ` b ) ) = ( ( F ` ( H ` a ) ) .- ( F ` ( H ` b ) ) ) ) |
20 |
3
|
adantr |
|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> G e. V ) |
21 |
12 13
|
ffvelrnd |
|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( H ` a ) e. P ) |
22 |
12 16
|
ffvelrnd |
|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( H ` b ) e. P ) |
23 |
4
|
adantr |
|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> F e. ( G Ismt G ) ) |
24 |
1 2 20 21 22 23
|
motcgr |
|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( F ` ( H ` a ) ) .- ( F ` ( H ` b ) ) ) = ( ( H ` a ) .- ( H ` b ) ) ) |
25 |
5
|
adantr |
|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> H e. ( G Ismt G ) ) |
26 |
1 2 20 13 16 25
|
motcgr |
|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( H ` a ) .- ( H ` b ) ) = ( a .- b ) ) |
27 |
19 24 26
|
3eqtrd |
|- ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( ( F o. H ) ` a ) .- ( ( F o. H ) ` b ) ) = ( a .- b ) ) |
28 |
27
|
ralrimivva |
|- ( ph -> A. a e. P A. b e. P ( ( ( F o. H ) ` a ) .- ( ( F o. H ) ` b ) ) = ( a .- b ) ) |
29 |
1 2
|
ismot |
|- ( G e. V -> ( ( F o. H ) e. ( G Ismt G ) <-> ( ( F o. H ) : P -1-1-onto-> P /\ A. a e. P A. b e. P ( ( ( F o. H ) ` a ) .- ( ( F o. H ) ` b ) ) = ( a .- b ) ) ) ) |
30 |
3 29
|
syl |
|- ( ph -> ( ( F o. H ) e. ( G Ismt G ) <-> ( ( F o. H ) : P -1-1-onto-> P /\ A. a e. P A. b e. P ( ( ( F o. H ) ` a ) .- ( ( F o. H ) ` b ) ) = ( a .- b ) ) ) ) |
31 |
9 28 30
|
mpbir2and |
|- ( ph -> ( F o. H ) e. ( G Ismt G ) ) |