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 fex 
 |-  ( ( F : A --> B /\ A e. V ) -> F e. _V )
26 7 6 25 syl2anc 
 |-  ( ph -> F e. _V )
27 ovex 
 |-  ( 1 ... M ) e. _V
28 fex 
 |-  ( ( H : ( 1 ... M ) --> A /\ ( 1 ... M ) e. _V ) -> H e. _V )
29 16 27 28 sylancl 
 |-  ( H : ( 1 ... M ) -1-1-> A -> H e. _V )
30 10 29 syl 
 |-  ( ph -> H e. _V )
31 f1fun 
 |-  ( H : ( 1 ... M ) -1-1-> A -> Fun H )
32 10 31 syl 
 |-  ( ph -> Fun H )
33 32 11 jca 
 |-  ( ph -> ( Fun H /\ ( F supp .0. ) C_ ran H ) )
34 26 30 33 jca31 
 |-  ( ph -> ( ( F e. _V /\ H e. _V ) /\ ( Fun H /\ ( F supp .0. ) C_ ran H ) ) )
35 34 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 ) ) )
36 imacosupp 
 |-  ( ( F e. _V /\ H e. _V ) -> ( ( Fun H /\ ( F supp .0. ) C_ ran H ) -> ( H " ( ( F o. H ) supp .0. ) ) = ( F supp .0. ) ) )
37 36 imp 
 |-  ( ( ( F e. _V /\ H e. _V ) /\ ( Fun H /\ ( F supp .0. ) C_ ran H ) ) -> ( H " ( ( F o. H ) supp .0. ) ) = ( F supp .0. ) )
38 35 37 syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H " ( ( F o. H ) supp .0. ) ) = ( F supp .0. ) )
39 24 38 syl5eq 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H " W ) = ( F supp .0. ) )
40 39 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. ) ) )
41 23 40 mpbid 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H |` W ) : W -1-1-onto-> ( F supp .0. ) )
42 isof1o 
 |-  ( f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) -> f : ( 1 ... ( # ` W ) ) -1-1-onto-> W )
43 42 ad2antll 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> f : ( 1 ... ( # ` W ) ) -1-1-onto-> W )
44 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. ) )
45 41 43 44 syl2anc 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( ( H |` W ) o. f ) : ( 1 ... ( # ` W ) ) -1-1-onto-> ( F supp .0. ) )
46 f1of 
 |-  ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> f : ( 1 ... ( # ` W ) ) --> W )
47 frn 
 |-  ( f : ( 1 ... ( # ` W ) ) --> W -> ran f C_ W )
48 43 46 47 3syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ran f C_ W )
49 cores 
 |-  ( ran f C_ W -> ( ( H |` W ) o. f ) = ( H o. f ) )
50 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. ) ) )
51 48 49 50 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. ) ) )
52 45 51 mpbid 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H o. f ) : ( 1 ... ( # ` W ) ) -1-1-onto-> ( F supp .0. ) )
53 fzfi 
 |-  ( 1 ... M ) e. Fin
54 ssfi 
 |-  ( ( ( 1 ... M ) e. Fin /\ W C_ ( 1 ... M ) ) -> W e. Fin )
55 53 20 54 sylancr 
 |-  ( ph -> W e. Fin )
56 55 ad2antrr 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> W e. Fin )
57 12 a1i 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> W = ( ( F o. H ) supp .0. ) )
58 57 imaeq2d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H " W ) = ( H " ( ( F o. H ) supp .0. ) ) )
59 53 a1i 
 |-  ( ph -> ( 1 ... M ) e. Fin )
60 fex2 
 |-  ( ( H : ( 1 ... M ) --> A /\ ( 1 ... M ) e. Fin /\ A e. V ) -> H e. _V )
61 17 59 6 60 syl3anc 
 |-  ( ph -> H e. _V )
62 26 61 33 jca31 
 |-  ( ph -> ( ( F e. _V /\ H e. _V ) /\ ( Fun H /\ ( F supp .0. ) C_ ran H ) ) )
63 62 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 ) ) )
64 63 37 syl 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H " ( ( F o. H ) supp .0. ) ) = ( F supp .0. ) )
65 58 64 eqtrd 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H " W ) = ( F supp .0. ) )
66 65 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. ) ) )
67 23 66 mpbid 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H |` W ) : W -1-1-onto-> ( F supp .0. ) )
68 56 67 hasheqf1od 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( # ` W ) = ( # ` ( F supp .0. ) ) )
69 68 oveq2d 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( 1 ... ( # ` W ) ) = ( 1 ... ( # ` ( F supp .0. ) ) ) )
70 69 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. ) ) )
71 52 70 mpbid 
 |-  ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( H o. f ) : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) )