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