# Metamath Proof Explorer

## Theorem gsumle

Description: A finite sum in an ordered monoid is monotonic. This proof would be much easier in an ordered group, where an inverse element would be available. (Contributed by Thierry Arnoux, 13-Mar-2018)

Ref Expression
Hypotheses gsumle.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
gsumle.l
gsumle.m ${⊢}{\phi }\to {M}\in \mathrm{oMnd}$
gsumle.n ${⊢}{\phi }\to {M}\in \mathrm{CMnd}$
gsumle.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
gsumle.f ${⊢}{\phi }\to {F}:{A}⟶{B}$
gsumle.g ${⊢}{\phi }\to {G}:{A}⟶{B}$
gsumle.c
Assertion gsumle

### Proof

Step Hyp Ref Expression
1 gsumle.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
2 gsumle.l
3 gsumle.m ${⊢}{\phi }\to {M}\in \mathrm{oMnd}$
4 gsumle.n ${⊢}{\phi }\to {M}\in \mathrm{CMnd}$
5 gsumle.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
6 gsumle.f ${⊢}{\phi }\to {F}:{A}⟶{B}$
7 gsumle.g ${⊢}{\phi }\to {G}:{A}⟶{B}$
8 gsumle.c
9 ssid ${⊢}{A}\subseteq {A}$
10 sseq1 ${⊢}{a}=\varnothing \to \left({a}\subseteq {A}↔\varnothing \subseteq {A}\right)$
11 10 anbi2d ${⊢}{a}=\varnothing \to \left(\left({\phi }\wedge {a}\subseteq {A}\right)↔\left({\phi }\wedge \varnothing \subseteq {A}\right)\right)$
12 reseq2 ${⊢}{a}=\varnothing \to {{F}↾}_{{a}}={{F}↾}_{\varnothing }$
13 12 oveq2d ${⊢}{a}=\varnothing \to {\sum }_{{M}}\left({{F}↾}_{{a}}\right)={\sum }_{{M}}\left({{F}↾}_{\varnothing }\right)$
14 reseq2 ${⊢}{a}=\varnothing \to {{G}↾}_{{a}}={{G}↾}_{\varnothing }$
15 14 oveq2d ${⊢}{a}=\varnothing \to {\sum }_{{M}}\left({{G}↾}_{{a}}\right)={\sum }_{{M}}\left({{G}↾}_{\varnothing }\right)$
16 13 15 breq12d
17 11 16 imbi12d
18 sseq1 ${⊢}{a}={e}\to \left({a}\subseteq {A}↔{e}\subseteq {A}\right)$
19 18 anbi2d ${⊢}{a}={e}\to \left(\left({\phi }\wedge {a}\subseteq {A}\right)↔\left({\phi }\wedge {e}\subseteq {A}\right)\right)$
20 reseq2 ${⊢}{a}={e}\to {{F}↾}_{{a}}={{F}↾}_{{e}}$
21 20 oveq2d ${⊢}{a}={e}\to {\sum }_{{M}}\left({{F}↾}_{{a}}\right)={\sum }_{{M}}\left({{F}↾}_{{e}}\right)$
22 reseq2 ${⊢}{a}={e}\to {{G}↾}_{{a}}={{G}↾}_{{e}}$
23 22 oveq2d ${⊢}{a}={e}\to {\sum }_{{M}}\left({{G}↾}_{{a}}\right)={\sum }_{{M}}\left({{G}↾}_{{e}}\right)$
24 21 23 breq12d
25 19 24 imbi12d
26 sseq1 ${⊢}{a}={e}\cup \left\{{y}\right\}\to \left({a}\subseteq {A}↔{e}\cup \left\{{y}\right\}\subseteq {A}\right)$
27 26 anbi2d ${⊢}{a}={e}\cup \left\{{y}\right\}\to \left(\left({\phi }\wedge {a}\subseteq {A}\right)↔\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\right)$
28 reseq2 ${⊢}{a}={e}\cup \left\{{y}\right\}\to {{F}↾}_{{a}}={{F}↾}_{\left({e}\cup \left\{{y}\right\}\right)}$
29 28 oveq2d ${⊢}{a}={e}\cup \left\{{y}\right\}\to {\sum }_{{M}}\left({{F}↾}_{{a}}\right)={\sum }_{{M}}\left({{F}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)$
30 reseq2 ${⊢}{a}={e}\cup \left\{{y}\right\}\to {{G}↾}_{{a}}={{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}$
31 30 oveq2d ${⊢}{a}={e}\cup \left\{{y}\right\}\to {\sum }_{{M}}\left({{G}↾}_{{a}}\right)={\sum }_{{M}}\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)$
32 29 31 breq12d
33 27 32 imbi12d
34 sseq1 ${⊢}{a}={A}\to \left({a}\subseteq {A}↔{A}\subseteq {A}\right)$
35 34 anbi2d ${⊢}{a}={A}\to \left(\left({\phi }\wedge {a}\subseteq {A}\right)↔\left({\phi }\wedge {A}\subseteq {A}\right)\right)$
36 reseq2 ${⊢}{a}={A}\to {{F}↾}_{{a}}={{F}↾}_{{A}}$
37 36 oveq2d ${⊢}{a}={A}\to {\sum }_{{M}}\left({{F}↾}_{{a}}\right)={\sum }_{{M}}\left({{F}↾}_{{A}}\right)$
38 reseq2 ${⊢}{a}={A}\to {{G}↾}_{{a}}={{G}↾}_{{A}}$
39 38 oveq2d ${⊢}{a}={A}\to {\sum }_{{M}}\left({{G}↾}_{{a}}\right)={\sum }_{{M}}\left({{G}↾}_{{A}}\right)$
40 37 39 breq12d
41 35 40 imbi12d
42 omndtos ${⊢}{M}\in \mathrm{oMnd}\to {M}\in \mathrm{Toset}$
43 tospos ${⊢}{M}\in \mathrm{Toset}\to {M}\in \mathrm{Poset}$
44 3 42 43 3syl ${⊢}{\phi }\to {M}\in \mathrm{Poset}$
45 res0 ${⊢}{{F}↾}_{\varnothing }=\varnothing$
46 45 oveq2i ${⊢}{\sum }_{{M}}\left({{F}↾}_{\varnothing }\right)={\sum }_{{M}}\varnothing$
47 eqid ${⊢}{0}_{{M}}={0}_{{M}}$
48 47 gsum0 ${⊢}{\sum }_{{M}}\varnothing ={0}_{{M}}$
49 46 48 eqtri ${⊢}{\sum }_{{M}}\left({{F}↾}_{\varnothing }\right)={0}_{{M}}$
50 omndmnd ${⊢}{M}\in \mathrm{oMnd}\to {M}\in \mathrm{Mnd}$
51 1 47 mndidcl ${⊢}{M}\in \mathrm{Mnd}\to {0}_{{M}}\in {B}$
52 3 50 51 3syl ${⊢}{\phi }\to {0}_{{M}}\in {B}$
53 49 52 eqeltrid ${⊢}{\phi }\to {\sum }_{{M}}\left({{F}↾}_{\varnothing }\right)\in {B}$
54 1 2 posref
55 44 53 54 syl2anc
56 res0 ${⊢}{{G}↾}_{\varnothing }=\varnothing$
57 45 56 eqtr4i ${⊢}{{F}↾}_{\varnothing }={{G}↾}_{\varnothing }$
58 57 oveq2i ${⊢}{\sum }_{{M}}\left({{F}↾}_{\varnothing }\right)={\sum }_{{M}}\left({{G}↾}_{\varnothing }\right)$
59 55 58 breqtrdi
61 ssun1 ${⊢}{e}\subseteq {e}\cup \left\{{y}\right\}$
62 sstr2 ${⊢}{e}\subseteq {e}\cup \left\{{y}\right\}\to \left({e}\cup \left\{{y}\right\}\subseteq {A}\to {e}\subseteq {A}\right)$
63 61 62 ax-mp ${⊢}{e}\cup \left\{{y}\right\}\subseteq {A}\to {e}\subseteq {A}$
64 63 anim2i ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to \left({\phi }\wedge {e}\subseteq {A}\right)$
65 64 imim1i
66 simplr
67 simpllr
68 simpr
69 eqid ${⊢}{+}_{{M}}={+}_{{M}}$
71 7 ad2antrr ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {G}:{A}⟶{B}$
72 simplr ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {e}\cup \left\{{y}\right\}\subseteq {A}$
73 ssun2 ${⊢}\left\{{y}\right\}\subseteq {e}\cup \left\{{y}\right\}$
74 vex ${⊢}{y}\in \mathrm{V}$
75 74 snss ${⊢}{y}\in \left({e}\cup \left\{{y}\right\}\right)↔\left\{{y}\right\}\subseteq {e}\cup \left\{{y}\right\}$
76 73 75 mpbir ${⊢}{y}\in \left({e}\cup \left\{{y}\right\}\right)$
77 76 a1i ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {y}\in \left({e}\cup \left\{{y}\right\}\right)$
78 72 77 sseldd ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {y}\in {A}$
79 71 78 ffvelrnd ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {G}\left({y}\right)\in {B}$
81 4 ad2antrr ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {M}\in \mathrm{CMnd}$
82 vex ${⊢}{e}\in \mathrm{V}$
83 82 a1i ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {e}\in \mathrm{V}$
84 6 ad2antrr ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {F}:{A}⟶{B}$
85 61 72 sstrid ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {e}\subseteq {A}$
86 84 85 fssresd ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to \left({{F}↾}_{{e}}\right):{e}⟶{B}$
87 5 ad2antrr ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {A}\in \mathrm{Fin}$
88 fvexd ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {0}_{{M}}\in \mathrm{V}$
89 84 87 88 fdmfifsupp ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {finSupp}_{{0}_{{M}}}\left({F}\right)$
90 89 88 fsuppres ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {finSupp}_{{0}_{{M}}}\left(\left({{F}↾}_{{e}}\right)\right)$
91 1 47 81 83 86 90 gsumcl ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {\sum }_{{M}}\left({{F}↾}_{{e}}\right)\in {B}$
93 84 78 ffvelrnd ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {F}\left({y}\right)\in {B}$
95 71 85 fssresd ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to \left({{G}↾}_{{e}}\right):{e}⟶{B}$
96 ssfi ${⊢}\left({A}\in \mathrm{Fin}\wedge {e}\subseteq {A}\right)\to {e}\in \mathrm{Fin}$
97 87 85 96 syl2anc ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {e}\in \mathrm{Fin}$
98 95 97 88 fdmfifsupp ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {finSupp}_{{0}_{{M}}}\left(\left({{G}↾}_{{e}}\right)\right)$
99 1 47 81 83 95 98 gsumcl ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {\sum }_{{M}}\left({{G}↾}_{{e}}\right)\in {B}$
101 simpr
102 simpll ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {\phi }$
104 6 ffnd ${⊢}{\phi }\to {F}Fn{A}$
105 7 ffnd ${⊢}{\phi }\to {G}Fn{A}$
106 inidm ${⊢}{A}\cap {A}={A}$
107 eqidd ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {F}\left({y}\right)={F}\left({y}\right)$
108 eqidd ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {G}\left({y}\right)={G}\left({y}\right)$
109 104 105 5 5 106 107 108 ofrval
110 102 103 78 109 syl3anc
113 1 2 69 70 80 92 94 100 101 111 112 omndadd2d
115 6 ad2antrr ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge {z}\in {e}\right)\to {F}:{A}⟶{B}$
116 simplr ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge {z}\in {e}\right)\to {e}\cup \left\{{y}\right\}\subseteq {A}$
117 elun1 ${⊢}{z}\in {e}\to {z}\in \left({e}\cup \left\{{y}\right\}\right)$
118 117 adantl ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge {z}\in {e}\right)\to {z}\in \left({e}\cup \left\{{y}\right\}\right)$
119 116 118 sseldd ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge {z}\in {e}\right)\to {z}\in {A}$
120 115 119 ffvelrnd ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge {z}\in {e}\right)\to {F}\left({z}\right)\in {B}$
121 120 ex ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to \left({z}\in {e}\to {F}\left({z}\right)\in {B}\right)$
123 122 imp
124 74 a1i
125 simplr
126 fveq2 ${⊢}{z}={y}\to {F}\left({z}\right)={F}\left({y}\right)$
127 1 69 112 114 123 124 125 94 126 gsumunsn
128 84 72 feqresmpt ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {{F}↾}_{\left({e}\cup \left\{{y}\right\}\right)}=\left({z}\in \left({e}\cup \left\{{y}\right\}\right)⟼{F}\left({z}\right)\right)$
129 128 oveq2d ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {\sum }_{{M}}\left({{F}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)=\underset{{z}\in {e}\cup \left\{{y}\right\}}{{\sum }_{{M}}}{F}\left({z}\right)$
130 84 85 feqresmpt ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {{F}↾}_{{e}}=\left({z}\in {e}⟼{F}\left({z}\right)\right)$
131 130 oveq2d ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {\sum }_{{M}}\left({{F}↾}_{{e}}\right)=\underset{{z}\in {e}}{{\sum }_{{M}}}{F}\left({z}\right)$
132 131 oveq1d ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to \left({\sum }_{{M}},\left({{F}↾}_{{e}}\right)\right){+}_{{M}}{F}\left({y}\right)=\left(\underset{{z}\in {e}}{{\sum }_{{M}}},{F}\left({z}\right)\right){+}_{{M}}{F}\left({y}\right)$
133 129 132 eqeq12d ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to \left({\sum }_{{M}}\left({{F}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)=\left({\sum }_{{M}},\left({{F}↾}_{{e}}\right)\right){+}_{{M}}{F}\left({y}\right)↔\underset{{z}\in {e}\cup \left\{{y}\right\}}{{\sum }_{{M}}}{F}\left({z}\right)=\left(\underset{{z}\in {e}}{{\sum }_{{M}}},{F}\left({z}\right)\right){+}_{{M}}{F}\left({y}\right)\right)$
135 127 134 mpbird
136 7 adantr ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to {G}:{A}⟶{B}$
137 136 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\wedge {z}\in {e}\right)\to {G}:{A}⟶{B}$
138 119 adantlr ${⊢}\left(\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\wedge {z}\in {e}\right)\to {z}\in {A}$
139 137 138 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\wedge {z}\in {e}\right)\to {G}\left({z}\right)\in {B}$
140 74 a1i ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {y}\in \mathrm{V}$
141 simpr ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to ¬{y}\in {e}$
142 fveq2 ${⊢}{z}={y}\to {G}\left({z}\right)={G}\left({y}\right)$
143 1 69 81 97 139 140 141 79 142 gsumunsn ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to \underset{{z}\in {e}\cup \left\{{y}\right\}}{{\sum }_{{M}}}{G}\left({z}\right)=\left(\underset{{z}\in {e}}{{\sum }_{{M}}},{G}\left({z}\right)\right){+}_{{M}}{G}\left({y}\right)$
144 simpr ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to {e}\cup \left\{{y}\right\}\subseteq {A}$
145 136 144 feqresmpt ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to {{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}=\left({z}\in \left({e}\cup \left\{{y}\right\}\right)⟼{G}\left({z}\right)\right)$
146 145 oveq2d ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to {\sum }_{{M}}\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)=\underset{{z}\in {e}\cup \left\{{y}\right\}}{{\sum }_{{M}}}{G}\left({z}\right)$
147 resabs1 ${⊢}{e}\subseteq {e}\cup \left\{{y}\right\}\to {\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{{e}}={{G}↾}_{{e}}$
148 61 147 mp1i ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to {\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{{e}}={{G}↾}_{{e}}$
149 63 adantl ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to {e}\subseteq {A}$
150 136 149 feqresmpt ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to {{G}↾}_{{e}}=\left({z}\in {e}⟼{G}\left({z}\right)\right)$
151 148 150 eqtrd ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to {\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{{e}}=\left({z}\in {e}⟼{G}\left({z}\right)\right)$
152 151 oveq2d ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to {\sum }_{{M}}\left({\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{{e}}\right)=\underset{{z}\in {e}}{{\sum }_{{M}}}{G}\left({z}\right)$
153 resabs1 ${⊢}\left\{{y}\right\}\subseteq {e}\cup \left\{{y}\right\}\to {\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{\left\{{y}\right\}}={{G}↾}_{\left\{{y}\right\}}$
154 73 153 mp1i ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to {\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{\left\{{y}\right\}}={{G}↾}_{\left\{{y}\right\}}$
155 73 144 sstrid ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to \left\{{y}\right\}\subseteq {A}$
156 136 155 feqresmpt ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to {{G}↾}_{\left\{{y}\right\}}=\left({z}\in \left\{{y}\right\}⟼{G}\left({z}\right)\right)$
157 154 156 eqtrd ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to {\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{\left\{{y}\right\}}=\left({z}\in \left\{{y}\right\}⟼{G}\left({z}\right)\right)$
158 157 oveq2d ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to {\sum }_{{M}}\left({\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{\left\{{y}\right\}}\right)=\underset{{z}\in \left\{{y}\right\}}{{\sum }_{{M}}}{G}\left({z}\right)$
159 3 50 syl ${⊢}{\phi }\to {M}\in \mathrm{Mnd}$
160 159 adantr ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to {M}\in \mathrm{Mnd}$
161 74 a1i ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to {y}\in \mathrm{V}$
162 76 a1i ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to {y}\in \left({e}\cup \left\{{y}\right\}\right)$
163 144 162 sseldd ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to {y}\in {A}$
164 136 163 ffvelrnd ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to {G}\left({y}\right)\in {B}$
165 142 adantl ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge {z}={y}\right)\to {G}\left({z}\right)={G}\left({y}\right)$
166 1 160 161 164 165 gsumsnd ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to \underset{{z}\in \left\{{y}\right\}}{{\sum }_{{M}}}{G}\left({z}\right)={G}\left({y}\right)$
167 158 166 eqtrd ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to {\sum }_{{M}}\left({\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{\left\{{y}\right\}}\right)={G}\left({y}\right)$
168 152 167 oveq12d ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to \left({\sum }_{{M}},\left({\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{{e}}\right)\right){+}_{{M}}\left({\sum }_{{M}},\left({\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{\left\{{y}\right\}}\right)\right)=\left(\underset{{z}\in {e}}{{\sum }_{{M}}},{G}\left({z}\right)\right){+}_{{M}}{G}\left({y}\right)$
169 146 168 eqeq12d ${⊢}\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\to \left({\sum }_{{M}}\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)=\left({\sum }_{{M}},\left({\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{{e}}\right)\right){+}_{{M}}\left({\sum }_{{M}},\left({\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{\left\{{y}\right\}}\right)\right)↔\underset{{z}\in {e}\cup \left\{{y}\right\}}{{\sum }_{{M}}}{G}\left({z}\right)=\left(\underset{{z}\in {e}}{{\sum }_{{M}}},{G}\left({z}\right)\right){+}_{{M}}{G}\left({y}\right)\right)$
170 169 adantr ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to \left({\sum }_{{M}}\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)=\left({\sum }_{{M}},\left({\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{{e}}\right)\right){+}_{{M}}\left({\sum }_{{M}},\left({\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{\left\{{y}\right\}}\right)\right)↔\underset{{z}\in {e}\cup \left\{{y}\right\}}{{\sum }_{{M}}}{G}\left({z}\right)=\left(\underset{{z}\in {e}}{{\sum }_{{M}}},{G}\left({z}\right)\right){+}_{{M}}{G}\left({y}\right)\right)$
171 143 170 mpbird ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {\sum }_{{M}}\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)=\left({\sum }_{{M}},\left({\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{{e}}\right)\right){+}_{{M}}\left({\sum }_{{M}},\left({\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{\left\{{y}\right\}}\right)\right)$
172 61 147 ax-mp ${⊢}{\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{{e}}={{G}↾}_{{e}}$
173 172 oveq2i ${⊢}{\sum }_{{M}}\left({\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{{e}}\right)={\sum }_{{M}}\left({{G}↾}_{{e}}\right)$
174 73 153 ax-mp ${⊢}{\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{\left\{{y}\right\}}={{G}↾}_{\left\{{y}\right\}}$
175 174 oveq2i ${⊢}{\sum }_{{M}}\left({\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{\left\{{y}\right\}}\right)={\sum }_{{M}}\left({{G}↾}_{\left\{{y}\right\}}\right)$
176 173 175 oveq12i ${⊢}\left({\sum }_{{M}},\left({\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{{e}}\right)\right){+}_{{M}}\left({\sum }_{{M}},\left({\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)↾}_{\left\{{y}\right\}}\right)\right)=\left({\sum }_{{M}},\left({{G}↾}_{{e}}\right)\right){+}_{{M}}\left({\sum }_{{M}},\left({{G}↾}_{\left\{{y}\right\}}\right)\right)$
177 171 176 eqtrdi ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {\sum }_{{M}}\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)=\left({\sum }_{{M}},\left({{G}↾}_{{e}}\right)\right){+}_{{M}}\left({\sum }_{{M}},\left({{G}↾}_{\left\{{y}\right\}}\right)\right)$
178 73 72 sstrid ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to \left\{{y}\right\}\subseteq {A}$
179 71 178 feqresmpt ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {{G}↾}_{\left\{{y}\right\}}=\left({x}\in \left\{{y}\right\}⟼{G}\left({x}\right)\right)$
180 179 oveq2d ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {\sum }_{{M}}\left({{G}↾}_{\left\{{y}\right\}}\right)=\underset{{x}\in \left\{{y}\right\}}{{\sum }_{{M}}}{G}\left({x}\right)$
181 cmnmnd ${⊢}{M}\in \mathrm{CMnd}\to {M}\in \mathrm{Mnd}$
182 81 181 syl ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {M}\in \mathrm{Mnd}$
183 fveq2 ${⊢}{x}={y}\to {G}\left({x}\right)={G}\left({y}\right)$
184 1 183 gsumsn ${⊢}\left({M}\in \mathrm{Mnd}\wedge {y}\in \mathrm{V}\wedge {G}\left({y}\right)\in {B}\right)\to \underset{{x}\in \left\{{y}\right\}}{{\sum }_{{M}}}{G}\left({x}\right)={G}\left({y}\right)$
185 182 140 79 184 syl3anc ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to \underset{{x}\in \left\{{y}\right\}}{{\sum }_{{M}}}{G}\left({x}\right)={G}\left({y}\right)$
186 180 185 eqtrd ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {\sum }_{{M}}\left({{G}↾}_{\left\{{y}\right\}}\right)={G}\left({y}\right)$
187 186 oveq2d ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to \left({\sum }_{{M}},\left({{G}↾}_{{e}}\right)\right){+}_{{M}}\left({\sum }_{{M}},\left({{G}↾}_{\left\{{y}\right\}}\right)\right)=\left({\sum }_{{M}},\left({{G}↾}_{{e}}\right)\right){+}_{{M}}{G}\left({y}\right)$
188 177 187 eqtrd ${⊢}\left(\left({\phi }\wedge {e}\cup \left\{{y}\right\}\subseteq {A}\right)\wedge ¬{y}\in {e}\right)\to {\sum }_{{M}}\left({{G}↾}_{\left({e}\cup \left\{{y}\right\}\right)}\right)=\left({\sum }_{{M}},\left({{G}↾}_{{e}}\right)\right){+}_{{M}}{G}\left({y}\right)$
190 113 135 189 3brtr4d
191 66 67 68 190 syl21anc
192 191 exp31
193 192 a2d
194 65 193 syl5
195 17 25 33 41 60 194 findcard2s
196 195 imp
197 9 196 mpanr2
198 5 197 mpancom
199 fnresdm ${⊢}{F}Fn{A}\to {{F}↾}_{{A}}={F}$
200 104 199 syl ${⊢}{\phi }\to {{F}↾}_{{A}}={F}$
201 200 oveq2d ${⊢}{\phi }\to {\sum }_{{M}}\left({{F}↾}_{{A}}\right)={\sum }_{{M}}{F}$
202 fnresdm ${⊢}{G}Fn{A}\to {{G}↾}_{{A}}={G}$
203 105 202 syl ${⊢}{\phi }\to {{G}↾}_{{A}}={G}$
204 203 oveq2d ${⊢}{\phi }\to {\sum }_{{M}}\left({{G}↾}_{{A}}\right)={\sum }_{{M}}{G}$
205 198 201 204 3brtr3d