# Metamath Proof Explorer

## Theorem gsumval3lem2

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

Ref Expression
Hypotheses gsumval3.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
gsumval3.0
gsumval3.p
gsumval3.z ${⊢}{Z}=\mathrm{Cntz}\left({G}\right)$
gsumval3.g ${⊢}{\phi }\to {G}\in \mathrm{Mnd}$
gsumval3.a ${⊢}{\phi }\to {A}\in {V}$
gsumval3.f ${⊢}{\phi }\to {F}:{A}⟶{B}$
gsumval3.c ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq {Z}\left(\mathrm{ran}{F}\right)$
gsumval3.m ${⊢}{\phi }\to {M}\in ℕ$
gsumval3.h ${⊢}{\phi }\to {H}:\left(1\dots {M}\right)\underset{1-1}{⟶}{A}$
gsumval3.n
gsumval3.w
Assertion gsumval3lem2

### Proof

Step Hyp Ref Expression
1 gsumval3.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 gsumval3.0
3 gsumval3.p
4 gsumval3.z ${⊢}{Z}=\mathrm{Cntz}\left({G}\right)$
5 gsumval3.g ${⊢}{\phi }\to {G}\in \mathrm{Mnd}$
6 gsumval3.a ${⊢}{\phi }\to {A}\in {V}$
7 gsumval3.f ${⊢}{\phi }\to {F}:{A}⟶{B}$
8 gsumval3.c ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq {Z}\left(\mathrm{ran}{F}\right)$
9 gsumval3.m ${⊢}{\phi }\to {M}\in ℕ$
10 gsumval3.h ${⊢}{\phi }\to {H}:\left(1\dots {M}\right)\underset{1-1}{⟶}{A}$
11 gsumval3.n
12 gsumval3.w
13 f1f ${⊢}{H}:\left(1\dots {M}\right)\underset{1-1}{⟶}{A}\to {H}:\left(1\dots {M}\right)⟶{A}$
14 10 13 syl ${⊢}{\phi }\to {H}:\left(1\dots {M}\right)⟶{A}$
15 fzfid ${⊢}{\phi }\to \left(1\dots {M}\right)\in \mathrm{Fin}$
16 fex2 ${⊢}\left({H}:\left(1\dots {M}\right)⟶{A}\wedge \left(1\dots {M}\right)\in \mathrm{Fin}\wedge {A}\in {V}\right)\to {H}\in \mathrm{V}$
17 14 15 6 16 syl3anc ${⊢}{\phi }\to {H}\in \mathrm{V}$
18 vex ${⊢}{f}\in \mathrm{V}$
19 coexg ${⊢}\left({H}\in \mathrm{V}\wedge {f}\in \mathrm{V}\right)\to {H}\circ {f}\in \mathrm{V}$
20 17 18 19 sylancl ${⊢}{\phi }\to {H}\circ {f}\in \mathrm{V}$
21 20 ad2antrr ${⊢}\left(\left({\phi }\wedge {W}\ne \varnothing \right)\wedge \left(¬{A}\in \mathrm{ran}\dots \wedge {f}{Isom}_{<,<}\left(\left(1\dots \left|{W}\right|\right),{W}\right)\right)\right)\to {H}\circ {f}\in \mathrm{V}$
22 1 2 3 4 5 6 7 8 9 10 11 12 gsumval3lem1
23 fzfi ${⊢}\left(1\dots {M}\right)\in \mathrm{Fin}$
24 suppssdm
25 12 24 eqsstri ${⊢}{W}\subseteq \mathrm{dom}\left({F}\circ {H}\right)$
26 fco ${⊢}\left({F}:{A}⟶{B}\wedge {H}:\left(1\dots {M}\right)⟶{A}\right)\to \left({F}\circ {H}\right):\left(1\dots {M}\right)⟶{B}$
27 7 14 26 syl2anc ${⊢}{\phi }\to \left({F}\circ {H}\right):\left(1\dots {M}\right)⟶{B}$
28 25 27 fssdm ${⊢}{\phi }\to {W}\subseteq \left(1\dots {M}\right)$
29 ssfi ${⊢}\left(\left(1\dots {M}\right)\in \mathrm{Fin}\wedge {W}\subseteq \left(1\dots {M}\right)\right)\to {W}\in \mathrm{Fin}$
30 23 28 29 sylancr ${⊢}{\phi }\to {W}\in \mathrm{Fin}$
31 30 ad2antrr ${⊢}\left(\left({\phi }\wedge {W}\ne \varnothing \right)\wedge \left(¬{A}\in \mathrm{ran}\dots \wedge {f}{Isom}_{<,<}\left(\left(1\dots \left|{W}\right|\right),{W}\right)\right)\right)\to {W}\in \mathrm{Fin}$
32 10 ad2antrr ${⊢}\left(\left({\phi }\wedge {W}\ne \varnothing \right)\wedge \left(¬{A}\in \mathrm{ran}\dots \wedge {f}{Isom}_{<,<}\left(\left(1\dots \left|{W}\right|\right),{W}\right)\right)\right)\to {H}:\left(1\dots {M}\right)\underset{1-1}{⟶}{A}$
33 28 ad2antrr ${⊢}\left(\left({\phi }\wedge {W}\ne \varnothing \right)\wedge \left(¬{A}\in \mathrm{ran}\dots \wedge {f}{Isom}_{<,<}\left(\left(1\dots \left|{W}\right|\right),{W}\right)\right)\right)\to {W}\subseteq \left(1\dots {M}\right)$
34 f1ores ${⊢}\left({H}:\left(1\dots {M}\right)\underset{1-1}{⟶}{A}\wedge {W}\subseteq \left(1\dots {M}\right)\right)\to \left({{H}↾}_{{W}}\right):{W}\underset{1-1 onto}{⟶}{H}\left[{W}\right]$
35 32 33 34 syl2anc ${⊢}\left(\left({\phi }\wedge {W}\ne \varnothing \right)\wedge \left(¬{A}\in \mathrm{ran}\dots \wedge {f}{Isom}_{<,<}\left(\left(1\dots \left|{W}\right|\right),{W}\right)\right)\right)\to \left({{H}↾}_{{W}}\right):{W}\underset{1-1 onto}{⟶}{H}\left[{W}\right]$
36 12 imaeq2i
37 fex ${⊢}\left({F}:{A}⟶{B}\wedge {A}\in {V}\right)\to {F}\in \mathrm{V}$
38 7 6 37 syl2anc ${⊢}{\phi }\to {F}\in \mathrm{V}$
39 ovex ${⊢}\left(1\dots {M}\right)\in \mathrm{V}$
40 fex ${⊢}\left({H}:\left(1\dots {M}\right)⟶{A}\wedge \left(1\dots {M}\right)\in \mathrm{V}\right)\to {H}\in \mathrm{V}$
41 14 39 40 sylancl ${⊢}{\phi }\to {H}\in \mathrm{V}$
42 38 41 jca ${⊢}{\phi }\to \left({F}\in \mathrm{V}\wedge {H}\in \mathrm{V}\right)$
43 f1fun ${⊢}{H}:\left(1\dots {M}\right)\underset{1-1}{⟶}{A}\to \mathrm{Fun}{H}$
44 10 43 syl ${⊢}{\phi }\to \mathrm{Fun}{H}$
45 44 11 jca
46 imacosupp
47 42 45 46 sylc
49 36 48 syl5eq
51 50 f1oeq3d
52 35 51 mpbid
53 31 52 hasheqf1od
54 53 fveq2d
55 22 54 jca
56 f1oeq1
57 coeq2 ${⊢}{g}={H}\circ {f}\to {F}\circ {g}={F}\circ \left({H}\circ {f}\right)$
58 57 seqeq3d
59 58 fveq1d
60 59 eqeq2d
61 56 60 anbi12d
62 21 55 61 spcedv
63 5 ad2antrr ${⊢}\left(\left({\phi }\wedge {W}\ne \varnothing \right)\wedge \left(¬{A}\in \mathrm{ran}\dots \wedge {f}{Isom}_{<,<}\left(\left(1\dots \left|{W}\right|\right),{W}\right)\right)\right)\to {G}\in \mathrm{Mnd}$
64 6 ad2antrr ${⊢}\left(\left({\phi }\wedge {W}\ne \varnothing \right)\wedge \left(¬{A}\in \mathrm{ran}\dots \wedge {f}{Isom}_{<,<}\left(\left(1\dots \left|{W}\right|\right),{W}\right)\right)\right)\to {A}\in {V}$
65 7 ad2antrr ${⊢}\left(\left({\phi }\wedge {W}\ne \varnothing \right)\wedge \left(¬{A}\in \mathrm{ran}\dots \wedge {f}{Isom}_{<,<}\left(\left(1\dots \left|{W}\right|\right),{W}\right)\right)\right)\to {F}:{A}⟶{B}$
66 8 ad2antrr ${⊢}\left(\left({\phi }\wedge {W}\ne \varnothing \right)\wedge \left(¬{A}\in \mathrm{ran}\dots \wedge {f}{Isom}_{<,<}\left(\left(1\dots \left|{W}\right|\right),{W}\right)\right)\right)\to \mathrm{ran}{F}\subseteq {Z}\left(\mathrm{ran}{F}\right)$
67 f1f1orn ${⊢}{H}:\left(1\dots {M}\right)\underset{1-1}{⟶}{A}\to {H}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\mathrm{ran}{H}$
68 10 67 syl ${⊢}{\phi }\to {H}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\mathrm{ran}{H}$
69 f1oen3g ${⊢}\left({H}\in \mathrm{V}\wedge {H}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\mathrm{ran}{H}\right)\to \left(1\dots {M}\right)\approx \mathrm{ran}{H}$
70 17 68 69 syl2anc ${⊢}{\phi }\to \left(1\dots {M}\right)\approx \mathrm{ran}{H}$
71 enfi ${⊢}\left(1\dots {M}\right)\approx \mathrm{ran}{H}\to \left(\left(1\dots {M}\right)\in \mathrm{Fin}↔\mathrm{ran}{H}\in \mathrm{Fin}\right)$
72 70 71 syl ${⊢}{\phi }\to \left(\left(1\dots {M}\right)\in \mathrm{Fin}↔\mathrm{ran}{H}\in \mathrm{Fin}\right)$
73 23 72 mpbii ${⊢}{\phi }\to \mathrm{ran}{H}\in \mathrm{Fin}$
74 73 11 ssfid
76 12 neeq1i
77 supp0cosupp0
78 77 necon3d
79 38 41 78 syl2anc
80 76 79 syl5bi
81 80 imp
84 14 frnd ${⊢}{\phi }\to \mathrm{ran}{H}\subseteq {A}$
85 84 ad2antrr ${⊢}\left(\left({\phi }\wedge {W}\ne \varnothing \right)\wedge \left(¬{A}\in \mathrm{ran}\dots \wedge {f}{Isom}_{<,<}\left(\left(1\dots \left|{W}\right|\right),{W}\right)\right)\right)\to \mathrm{ran}{H}\subseteq {A}$
86 83 85 sstrd
87 1 2 3 4 63 64 65 66 75 82 86 gsumval3eu
88 iota1
89 87 88 syl
90 eqid
91 simprl ${⊢}\left(\left({\phi }\wedge {W}\ne \varnothing \right)\wedge \left(¬{A}\in \mathrm{ran}\dots \wedge {f}{Isom}_{<,<}\left(\left(1\dots \left|{W}\right|\right),{W}\right)\right)\right)\to ¬{A}\in \mathrm{ran}\dots$
92 1 2 3 4 63 64 65 66 75 82 90 91 gsumval3a
93 92 eqeq1d
94 89 93 bitr4d
95 94 alrimiv
96 fvex
97 eqeq1
98 97 anbi2d
99 98 exbidv
100 eqeq2
101 99 100 bibi12d
102 96 101 spcv
103 95 102 syl
104 62 103 mpbid