Metamath Proof Explorer


Theorem psrass1lemOLD

Description: Obsolete version of psrass1lem as of 7-Aug-2024. (Contributed by Mario Carneiro, 5-Jan-2015) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses psrbag.d D = f 0 I | f -1 Fin
psrbagconf1o.s S = y D | y f F
gsumbagdiagOLD.i φ I V
gsumbagdiagOLD.f φ F D
gsumbagdiagOLD.b B = Base G
gsumbagdiagOLD.g φ G CMnd
gsumbagdiagOLD.x φ j S k x D | x f F f j X B
psrass1lemOLD.y k = n f j X = Y
Assertion psrass1lemOLD φ G n S G j x D | x f n Y = G j S G k x D | x f F f j X

Proof

Step Hyp Ref Expression
1 psrbag.d D = f 0 I | f -1 Fin
2 psrbagconf1o.s S = y D | y f F
3 gsumbagdiagOLD.i φ I V
4 gsumbagdiagOLD.f φ F D
5 gsumbagdiagOLD.b B = Base G
6 gsumbagdiagOLD.g φ G CMnd
7 gsumbagdiagOLD.x φ j S k x D | x f F f j X B
8 psrass1lemOLD.y k = n f j X = Y
9 1 2 3 4 gsumbagdiaglemOLD φ m S j x D | x f F f m j S m x D | x f F f j
10 7 anassrs φ j S k x D | x f F f j X B
11 10 fmpttd φ j S k x D | x f F f j X : x D | x f F f j B
12 3 adantr φ j S I V
13 2 ssrab3 S D
14 4 adantr φ j S F D
15 simpr φ j S j S
16 1 2 psrbagconclOLD I V F D j S F f j S
17 12 14 15 16 syl3anc φ j S F f j S
18 13 17 sselid φ j S F f j D
19 eqid x D | x f F f j = x D | x f F f j
20 1 19 psrbagconf1oOLD I V F f j D m x D | x f F f j F f j f m : x D | x f F f j 1-1 onto x D | x f F f j
21 12 18 20 syl2anc φ j S m x D | x f F f j F f j f m : x D | x f F f j 1-1 onto x D | x f F f j
22 f1of m x D | x f F f j F f j f m : x D | x f F f j 1-1 onto x D | x f F f j m x D | x f F f j F f j f m : x D | x f F f j x D | x f F f j
23 21 22 syl φ j S m x D | x f F f j F f j f m : x D | x f F f j x D | x f F f j
24 fco k x D | x f F f j X : x D | x f F f j B m x D | x f F f j F f j f m : x D | x f F f j x D | x f F f j k x D | x f F f j X m x D | x f F f j F f j f m : x D | x f F f j B
25 11 23 24 syl2anc φ j S k x D | x f F f j X m x D | x f F f j F f j f m : x D | x f F f j B
26 12 adantr φ j S m x D | x f F f j I V
27 14 adantr φ j S m x D | x f F f j F D
28 1 psrbagfOLD I V F D F : I 0
29 26 27 28 syl2anc φ j S m x D | x f F f j F : I 0
30 29 ffvelrnda φ j S m x D | x f F f j z I F z 0
31 15 adantr φ j S m x D | x f F f j j S
32 13 31 sselid φ j S m x D | x f F f j j D
33 1 psrbagfOLD I V j D j : I 0
34 26 32 33 syl2anc φ j S m x D | x f F f j j : I 0
35 34 ffvelrnda φ j S m x D | x f F f j z I j z 0
36 ssrab2 x D | x f F f j D
37 simpr φ j S m x D | x f F f j m x D | x f F f j
38 36 37 sselid φ j S m x D | x f F f j m D
39 1 psrbagfOLD I V m D m : I 0
40 26 38 39 syl2anc φ j S m x D | x f F f j m : I 0
41 40 ffvelrnda φ j S m x D | x f F f j z I m z 0
42 nn0cn F z 0 F z
43 nn0cn j z 0 j z
44 nn0cn m z 0 m z
45 sub32 F z j z m z F z - j z - m z = F z - m z - j z
46 42 43 44 45 syl3an F z 0 j z 0 m z 0 F z - j z - m z = F z - m z - j z
47 30 35 41 46 syl3anc φ j S m x D | x f F f j z I F z - j z - m z = F z - m z - j z
48 47 mpteq2dva φ j S m x D | x f F f j z I F z - j z - m z = z I F z - m z - j z
49 ovexd φ j S m x D | x f F f j z I F z j z V
50 29 feqmptd φ j S m x D | x f F f j F = z I F z
51 34 feqmptd φ j S m x D | x f F f j j = z I j z
52 26 30 35 50 51 offval2 φ j S m x D | x f F f j F f j = z I F z j z
53 40 feqmptd φ j S m x D | x f F f j m = z I m z
54 26 49 41 52 53 offval2 φ j S m x D | x f F f j F f j f m = z I F z - j z - m z
55 ovexd φ j S m x D | x f F f j z I F z m z V
56 26 30 41 50 53 offval2 φ j S m x D | x f F f j F f m = z I F z m z
57 26 55 35 56 51 offval2 φ j S m x D | x f F f j F f m f j = z I F z - m z - j z
58 48 54 57 3eqtr4d φ j S m x D | x f F f j F f j f m = F f m f j
59 18 adantr φ j S m x D | x f F f j F f j D
60 1 19 psrbagconclOLD I V F f j D m x D | x f F f j F f j f m x D | x f F f j
61 26 59 37 60 syl3anc φ j S m x D | x f F f j F f j f m x D | x f F f j
62 58 61 eqeltrrd φ j S m x D | x f F f j F f m f j x D | x f F f j
63 58 mpteq2dva φ j S m x D | x f F f j F f j f m = m x D | x f F f j F f m f j
64 nfcv _ n X
65 nfcsb1v _ k n / k X
66 csbeq1a k = n X = n / k X
67 64 65 66 cbvmpt k x D | x f F f j X = n x D | x f F f j n / k X
68 67 a1i φ j S k x D | x f F f j X = n x D | x f F f j n / k X
69 csbeq1 n = F f m f j n / k X = F f m f j / k X
70 62 63 68 69 fmptco φ j S k x D | x f F f j X m x D | x f F f j F f j f m = m x D | x f F f j F f m f j / k X
71 70 feq1d φ j S k x D | x f F f j X m x D | x f F f j F f j f m : x D | x f F f j B m x D | x f F f j F f m f j / k X : x D | x f F f j B
72 25 71 mpbid φ j S m x D | x f F f j F f m f j / k X : x D | x f F f j B
73 72 fvmptelrn φ j S m x D | x f F f j F f m f j / k X B
74 73 anasss φ j S m x D | x f F f j F f m f j / k X B
75 9 74 syldan φ m S j x D | x f F f m F f m f j / k X B
76 1 2 3 4 5 6 75 gsumbagdiagOLD φ G m S , j x D | x f F f m F f m f j / k X = G j S , m x D | x f F f j F f m f j / k X
77 eqid 0 G = 0 G
78 1 psrbaglefiOLD I V F D y D | y f F Fin
79 3 4 78 syl2anc φ y D | y f F Fin
80 2 79 eqeltrid φ S Fin
81 3 adantr φ m S I V
82 4 adantr φ m S F D
83 simpr φ m S m S
84 1 2 psrbagconclOLD I V F D m S F f m S
85 81 82 83 84 syl3anc φ m S F f m S
86 13 85 sselid φ m S F f m D
87 1 psrbaglefiOLD I V F f m D x D | x f F f m Fin
88 81 86 87 syl2anc φ m S x D | x f F f m Fin
89 xpfi S Fin S Fin S × S Fin
90 80 80 89 syl2anc φ S × S Fin
91 simprl φ m S j x D | x f F f m m S
92 9 simpld φ m S j x D | x f F f m j S
93 brxp m S × S j m S j S
94 91 92 93 sylanbrc φ m S j x D | x f F f m m S × S j
95 94 pm2.24d φ m S j x D | x f F f m ¬ m S × S j F f m f j / k X = 0 G
96 95 impr φ m S j x D | x f F f m ¬ m S × S j F f m f j / k X = 0 G
97 5 77 6 80 88 75 90 96 gsum2d2 φ G m S , j x D | x f F f m F f m f j / k X = G m S G j x D | x f F f m F f m f j / k X
98 1 psrbaglefiOLD I V F f j D x D | x f F f j Fin
99 12 18 98 syl2anc φ j S x D | x f F f j Fin
100 simprl φ j S m x D | x f F f j j S
101 1 2 3 4 gsumbagdiaglemOLD φ j S m x D | x f F f j m S j x D | x f F f m
102 101 simpld φ j S m x D | x f F f j m S
103 brxp j S × S m j S m S
104 100 102 103 sylanbrc φ j S m x D | x f F f j j S × S m
105 104 pm2.24d φ j S m x D | x f F f j ¬ j S × S m F f m f j / k X = 0 G
106 105 impr φ j S m x D | x f F f j ¬ j S × S m F f m f j / k X = 0 G
107 5 77 6 80 99 74 90 106 gsum2d2 φ G j S , m x D | x f F f j F f m f j / k X = G j S G m x D | x f F f j F f m f j / k X
108 76 97 107 3eqtr3d φ G m S G j x D | x f F f m F f m f j / k X = G j S G m x D | x f F f j F f m f j / k X
109 6 adantr φ m S G CMnd
110 75 anassrs φ m S j x D | x f F f m F f m f j / k X B
111 110 fmpttd φ m S j x D | x f F f m F f m f j / k X : x D | x f F f m B
112 ovex 0 I V
113 1 112 rabex2 D V
114 113 a1i φ m S D V
115 rabexg D V x D | x f F f m V
116 mptexg x D | x f F f m V j x D | x f F f m F f m f j / k X V
117 114 115 116 3syl φ m S j x D | x f F f m F f m f j / k X V
118 funmpt Fun j x D | x f F f m F f m f j / k X
119 118 a1i φ m S Fun j x D | x f F f m F f m f j / k X
120 fvexd φ m S 0 G V
121 suppssdm j x D | x f F f m F f m f j / k X supp 0 G dom j x D | x f F f m F f m f j / k X
122 eqid j x D | x f F f m F f m f j / k X = j x D | x f F f m F f m f j / k X
123 122 dmmptss dom j x D | x f F f m F f m f j / k X x D | x f F f m
124 121 123 sstri j x D | x f F f m F f m f j / k X supp 0 G x D | x f F f m
125 124 a1i φ m S j x D | x f F f m F f m f j / k X supp 0 G x D | x f F f m
126 suppssfifsupp j x D | x f F f m F f m f j / k X V Fun j x D | x f F f m F f m f j / k X 0 G V x D | x f F f m Fin j x D | x f F f m F f m f j / k X supp 0 G x D | x f F f m finSupp 0 G j x D | x f F f m F f m f j / k X
127 117 119 120 88 125 126 syl32anc φ m S finSupp 0 G j x D | x f F f m F f m f j / k X
128 5 77 109 88 111 127 gsumcl φ m S G j x D | x f F f m F f m f j / k X B
129 128 fmpttd φ m S G j x D | x f F f m F f m f j / k X : S B
130 1 2 psrbagconf1oOLD I V F D m S F f m : S 1-1 onto S
131 3 4 130 syl2anc φ m S F f m : S 1-1 onto S
132 f1ocnv m S F f m : S 1-1 onto S m S F f m -1 : S 1-1 onto S
133 f1of m S F f m -1 : S 1-1 onto S m S F f m -1 : S S
134 131 132 133 3syl φ m S F f m -1 : S S
135 fco m S G j x D | x f F f m F f m f j / k X : S B m S F f m -1 : S S m S G j x D | x f F f m F f m f j / k X m S F f m -1 : S B
136 129 134 135 syl2anc φ m S G j x D | x f F f m F f m f j / k X m S F f m -1 : S B
137 coass n S G j x D | x f n Y m S F f m m S F f m -1 = n S G j x D | x f n Y m S F f m m S F f m -1
138 f1ococnv2 m S F f m : S 1-1 onto S m S F f m m S F f m -1 = I S
139 131 138 syl φ m S F f m m S F f m -1 = I S
140 139 coeq2d φ n S G j x D | x f n Y m S F f m m S F f m -1 = n S G j x D | x f n Y I S
141 137 140 syl5eq φ n S G j x D | x f n Y m S F f m m S F f m -1 = n S G j x D | x f n Y I S
142 eqidd φ m S F f m = m S F f m
143 eqidd φ n S G j x D | x f n Y = n S G j x D | x f n Y
144 breq2 n = F f m x f n x f F f m
145 144 rabbidv n = F f m x D | x f n = x D | x f F f m
146 ovex n f j V
147 146 8 csbie n f j / k X = Y
148 oveq1 n = F f m n f j = F f m f j
149 148 csbeq1d n = F f m n f j / k X = F f m f j / k X
150 147 149 eqtr3id n = F f m Y = F f m f j / k X
151 145 150 mpteq12dv n = F f m j x D | x f n Y = j x D | x f F f m F f m f j / k X
152 151 oveq2d n = F f m G j x D | x f n Y = G j x D | x f F f m F f m f j / k X
153 85 142 143 152 fmptco φ n S G j x D | x f n Y m S F f m = m S G j x D | x f F f m F f m f j / k X
154 153 coeq1d φ n S G j x D | x f n Y m S F f m m S F f m -1 = m S G j x D | x f F f m F f m f j / k X m S F f m -1
155 coires1 n S G j x D | x f n Y I S = n S G j x D | x f n Y S
156 ssid S S
157 resmpt S S n S G j x D | x f n Y S = n S G j x D | x f n Y
158 156 157 ax-mp n S G j x D | x f n Y S = n S G j x D | x f n Y
159 155 158 eqtri n S G j x D | x f n Y I S = n S G j x D | x f n Y
160 159 a1i φ n S G j x D | x f n Y I S = n S G j x D | x f n Y
161 141 154 160 3eqtr3d φ m S G j x D | x f F f m F f m f j / k X m S F f m -1 = n S G j x D | x f n Y
162 161 feq1d φ m S G j x D | x f F f m F f m f j / k X m S F f m -1 : S B n S G j x D | x f n Y : S B
163 136 162 mpbid φ n S G j x D | x f n Y : S B
164 rabexg D V y D | y f F V
165 113 164 mp1i φ y D | y f F V
166 2 165 eqeltrid φ S V
167 166 mptexd φ n S G j x D | x f n Y V
168 funmpt Fun n S G j x D | x f n Y
169 168 a1i φ Fun n S G j x D | x f n Y
170 fvexd φ 0 G V
171 suppssdm n S G j x D | x f n Y supp 0 G dom n S G j x D | x f n Y
172 eqid n S G j x D | x f n Y = n S G j x D | x f n Y
173 172 dmmptss dom n S G j x D | x f n Y S
174 171 173 sstri n S G j x D | x f n Y supp 0 G S
175 174 a1i φ n S G j x D | x f n Y supp 0 G S
176 suppssfifsupp n S G j x D | x f n Y V Fun n S G j x D | x f n Y 0 G V S Fin n S G j x D | x f n Y supp 0 G S finSupp 0 G n S G j x D | x f n Y
177 167 169 170 80 175 176 syl32anc φ finSupp 0 G n S G j x D | x f n Y
178 5 77 6 80 163 177 131 gsumf1o φ G n S G j x D | x f n Y = G n S G j x D | x f n Y m S F f m
179 153 oveq2d φ G n S G j x D | x f n Y m S F f m = G m S G j x D | x f F f m F f m f j / k X
180 178 179 eqtrd φ G n S G j x D | x f n Y = G m S G j x D | x f F f m F f m f j / k X
181 6 adantr φ j S G CMnd
182 113 a1i φ j S D V
183 rabexg D V x D | x f F f j V
184 mptexg x D | x f F f j V k x D | x f F f j X V
185 182 183 184 3syl φ j S k x D | x f F f j X V
186 funmpt Fun k x D | x f F f j X
187 186 a1i φ j S Fun k x D | x f F f j X
188 fvexd φ j S 0 G V
189 suppssdm k x D | x f F f j X supp 0 G dom k x D | x f F f j X
190 eqid k x D | x f F f j X = k x D | x f F f j X
191 190 dmmptss dom k x D | x f F f j X x D | x f F f j
192 189 191 sstri k x D | x f F f j X supp 0 G x D | x f F f j
193 192 a1i φ j S k x D | x f F f j X supp 0 G x D | x f F f j
194 suppssfifsupp k x D | x f F f j X V Fun k x D | x f F f j X 0 G V x D | x f F f j Fin k x D | x f F f j X supp 0 G x D | x f F f j finSupp 0 G k x D | x f F f j X
195 185 187 188 99 193 194 syl32anc φ j S finSupp 0 G k x D | x f F f j X
196 5 77 181 99 11 195 21 gsumf1o φ j S G k x D | x f F f j X = G k x D | x f F f j X m x D | x f F f j F f j f m
197 70 oveq2d φ j S G k x D | x f F f j X m x D | x f F f j F f j f m = G m x D | x f F f j F f m f j / k X
198 196 197 eqtrd φ j S G k x D | x f F f j X = G m x D | x f F f j F f m f j / k X
199 198 mpteq2dva φ j S G k x D | x f F f j X = j S G m x D | x f F f j F f m f j / k X
200 199 oveq2d φ G j S G k x D | x f F f j X = G j S G m x D | x f F f j F f m f j / k X
201 108 180 200 3eqtr4d φ G n S G j x D | x f n Y = G j S G k x D | x f F f j X