Step |
Hyp |
Ref |
Expression |
1 |
|
gsumval3.b |
|- B = ( Base ` G ) |
2 |
|
gsumval3.0 |
|- .0. = ( 0g ` G ) |
3 |
|
gsumval3.p |
|- .+ = ( +g ` G ) |
4 |
|
gsumval3.z |
|- Z = ( Cntz ` G ) |
5 |
|
gsumval3.g |
|- ( ph -> G e. Mnd ) |
6 |
|
gsumval3.a |
|- ( ph -> A e. V ) |
7 |
|
gsumval3.f |
|- ( ph -> F : A --> B ) |
8 |
|
gsumval3.c |
|- ( ph -> ran F C_ ( Z ` ran F ) ) |
9 |
|
gsumval3.m |
|- ( ph -> M e. NN ) |
10 |
|
gsumval3.h |
|- ( ph -> H : ( 1 ... M ) -1-1-> A ) |
11 |
|
gsumval3.n |
|- ( ph -> ( F supp .0. ) C_ ran H ) |
12 |
|
gsumval3.w |
|- W = ( ( F o. H ) supp .0. ) |
13 |
10
|
ad2antrr |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> H : ( 1 ... M ) -1-1-> A ) |
14 |
|
suppssdm |
|- ( ( F o. H ) supp .0. ) C_ dom ( F o. H ) |
15 |
12 14
|
eqsstri |
|- W C_ dom ( F o. H ) |
16 |
|
f1f |
|- ( H : ( 1 ... M ) -1-1-> A -> H : ( 1 ... M ) --> A ) |
17 |
10 16
|
syl |
|- ( ph -> H : ( 1 ... M ) --> A ) |
18 |
|
fco |
|- ( ( F : A --> B /\ H : ( 1 ... M ) --> A ) -> ( F o. H ) : ( 1 ... M ) --> B ) |
19 |
7 17 18
|
syl2anc |
|- ( ph -> ( F o. H ) : ( 1 ... M ) --> B ) |
20 |
15 19
|
fssdm |
|- ( ph -> W C_ ( 1 ... M ) ) |
21 |
20
|
ad2antrr |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> W C_ ( 1 ... M ) ) |
22 |
|
f1ores |
|- ( ( H : ( 1 ... M ) -1-1-> A /\ W C_ ( 1 ... M ) ) -> ( H |` W ) : W -1-1-onto-> ( H " W ) ) |
23 |
13 21 22
|
syl2anc |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H |` W ) : W -1-1-onto-> ( H " W ) ) |
24 |
12
|
imaeq2i |
|- ( H " W ) = ( H " ( ( F o. H ) supp .0. ) ) |
25 |
7 6
|
fexd |
|- ( ph -> F e. _V ) |
26 |
|
ovex |
|- ( 1 ... M ) e. _V |
27 |
|
fex |
|- ( ( H : ( 1 ... M ) --> A /\ ( 1 ... M ) e. _V ) -> H e. _V ) |
28 |
16 26 27
|
sylancl |
|- ( H : ( 1 ... M ) -1-1-> A -> H e. _V ) |
29 |
10 28
|
syl |
|- ( ph -> H e. _V ) |
30 |
|
f1fun |
|- ( H : ( 1 ... M ) -1-1-> A -> Fun H ) |
31 |
10 30
|
syl |
|- ( ph -> Fun H ) |
32 |
31 11
|
jca |
|- ( ph -> ( Fun H /\ ( F supp .0. ) C_ ran H ) ) |
33 |
25 29 32
|
jca31 |
|- ( ph -> ( ( F e. _V /\ H e. _V ) /\ ( Fun H /\ ( F supp .0. ) C_ ran H ) ) ) |
34 |
33
|
ad2antrr |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( ( F e. _V /\ H e. _V ) /\ ( Fun H /\ ( F supp .0. ) C_ ran H ) ) ) |
35 |
|
imacosupp |
|- ( ( F e. _V /\ H e. _V ) -> ( ( Fun H /\ ( F supp .0. ) C_ ran H ) -> ( H " ( ( F o. H ) supp .0. ) ) = ( F supp .0. ) ) ) |
36 |
35
|
imp |
|- ( ( ( F e. _V /\ H e. _V ) /\ ( Fun H /\ ( F supp .0. ) C_ ran H ) ) -> ( H " ( ( F o. H ) supp .0. ) ) = ( F supp .0. ) ) |
37 |
34 36
|
syl |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H " ( ( F o. H ) supp .0. ) ) = ( F supp .0. ) ) |
38 |
24 37
|
syl5eq |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H " W ) = ( F supp .0. ) ) |
39 |
38
|
f1oeq3d |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( ( H |` W ) : W -1-1-onto-> ( H " W ) <-> ( H |` W ) : W -1-1-onto-> ( F supp .0. ) ) ) |
40 |
23 39
|
mpbid |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H |` W ) : W -1-1-onto-> ( F supp .0. ) ) |
41 |
|
isof1o |
|- ( f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) -> f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) |
42 |
41
|
ad2antll |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) |
43 |
|
f1oco |
|- ( ( ( H |` W ) : W -1-1-onto-> ( F supp .0. ) /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) -> ( ( H |` W ) o. f ) : ( 1 ... ( # ` W ) ) -1-1-onto-> ( F supp .0. ) ) |
44 |
40 42 43
|
syl2anc |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( ( H |` W ) o. f ) : ( 1 ... ( # ` W ) ) -1-1-onto-> ( F supp .0. ) ) |
45 |
|
f1of |
|- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> f : ( 1 ... ( # ` W ) ) --> W ) |
46 |
|
frn |
|- ( f : ( 1 ... ( # ` W ) ) --> W -> ran f C_ W ) |
47 |
42 45 46
|
3syl |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ran f C_ W ) |
48 |
|
cores |
|- ( ran f C_ W -> ( ( H |` W ) o. f ) = ( H o. f ) ) |
49 |
|
f1oeq1 |
|- ( ( ( H |` W ) o. f ) = ( H o. f ) -> ( ( ( H |` W ) o. f ) : ( 1 ... ( # ` W ) ) -1-1-onto-> ( F supp .0. ) <-> ( H o. f ) : ( 1 ... ( # ` W ) ) -1-1-onto-> ( F supp .0. ) ) ) |
50 |
47 48 49
|
3syl |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( ( ( H |` W ) o. f ) : ( 1 ... ( # ` W ) ) -1-1-onto-> ( F supp .0. ) <-> ( H o. f ) : ( 1 ... ( # ` W ) ) -1-1-onto-> ( F supp .0. ) ) ) |
51 |
44 50
|
mpbid |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H o. f ) : ( 1 ... ( # ` W ) ) -1-1-onto-> ( F supp .0. ) ) |
52 |
|
fzfi |
|- ( 1 ... M ) e. Fin |
53 |
|
ssfi |
|- ( ( ( 1 ... M ) e. Fin /\ W C_ ( 1 ... M ) ) -> W e. Fin ) |
54 |
52 20 53
|
sylancr |
|- ( ph -> W e. Fin ) |
55 |
54
|
ad2antrr |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> W e. Fin ) |
56 |
12
|
a1i |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> W = ( ( F o. H ) supp .0. ) ) |
57 |
56
|
imaeq2d |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H " W ) = ( H " ( ( F o. H ) supp .0. ) ) ) |
58 |
52
|
a1i |
|- ( ph -> ( 1 ... M ) e. Fin ) |
59 |
17 58
|
fexd |
|- ( ph -> H e. _V ) |
60 |
25 59 32
|
jca31 |
|- ( ph -> ( ( F e. _V /\ H e. _V ) /\ ( Fun H /\ ( F supp .0. ) C_ ran H ) ) ) |
61 |
60
|
ad2antrr |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( ( F e. _V /\ H e. _V ) /\ ( Fun H /\ ( F supp .0. ) C_ ran H ) ) ) |
62 |
61 36
|
syl |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H " ( ( F o. H ) supp .0. ) ) = ( F supp .0. ) ) |
63 |
57 62
|
eqtrd |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H " W ) = ( F supp .0. ) ) |
64 |
63
|
f1oeq3d |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( ( H |` W ) : W -1-1-onto-> ( H " W ) <-> ( H |` W ) : W -1-1-onto-> ( F supp .0. ) ) ) |
65 |
23 64
|
mpbid |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H |` W ) : W -1-1-onto-> ( F supp .0. ) ) |
66 |
55 65
|
hasheqf1od |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( # ` W ) = ( # ` ( F supp .0. ) ) ) |
67 |
66
|
oveq2d |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( 1 ... ( # ` W ) ) = ( 1 ... ( # ` ( F supp .0. ) ) ) ) |
68 |
67
|
f1oeq2d |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( ( H o. f ) : ( 1 ... ( # ` W ) ) -1-1-onto-> ( F supp .0. ) <-> ( H o. f ) : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) |
69 |
51 68
|
mpbid |
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H o. f ) : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) |