Metamath Proof Explorer


Theorem gsumval3lem1

Description: Lemma 1 for gsumval3 . (Contributed by AV, 31-May-2019)

Ref Expression
Hypotheses gsumval3.b
|- B = ( Base ` G )
gsumval3.0
|- .0. = ( 0g ` G )
gsumval3.p
|- .+ = ( +g ` G )
gsumval3.z
|- Z = ( Cntz ` G )
gsumval3.g
|- ( ph -> G e. Mnd )
gsumval3.a
|- ( ph -> A e. V )
gsumval3.f
|- ( ph -> F : A --> B )
gsumval3.c
|- ( ph -> ran F C_ ( Z ` ran F ) )
gsumval3.m
|- ( ph -> M e. NN )
gsumval3.h
|- ( ph -> H : ( 1 ... M ) -1-1-> A )
gsumval3.n
|- ( ph -> ( F supp .0. ) C_ ran H )
gsumval3.w
|- W = ( ( F o. H ) supp .0. )
Assertion gsumval3lem1
|- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H o. f ) : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) )

Proof

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. ) )