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=f0I|f-1Fin
psrbagconf1o.s S=yD|yfF
gsumbagdiagOLD.i φIV
gsumbagdiagOLD.f φFD
gsumbagdiagOLD.b B=BaseG
gsumbagdiagOLD.g φGCMnd
gsumbagdiagOLD.x φjSkxD|xfFfjXB
psrass1lemOLD.y k=nfjX=Y
Assertion psrass1lemOLD φGnSGjxD|xfnY=GjSGkxD|xfFfjX

Proof

Step Hyp Ref Expression
1 psrbag.d D=f0I|f-1Fin
2 psrbagconf1o.s S=yD|yfF
3 gsumbagdiagOLD.i φIV
4 gsumbagdiagOLD.f φFD
5 gsumbagdiagOLD.b B=BaseG
6 gsumbagdiagOLD.g φGCMnd
7 gsumbagdiagOLD.x φjSkxD|xfFfjXB
8 psrass1lemOLD.y k=nfjX=Y
9 1 2 3 4 gsumbagdiaglemOLD φmSjxD|xfFfmjSmxD|xfFfj
10 7 anassrs φjSkxD|xfFfjXB
11 10 fmpttd φjSkxD|xfFfjX:xD|xfFfjB
12 3 adantr φjSIV
13 2 ssrab3 SD
14 4 adantr φjSFD
15 simpr φjSjS
16 1 2 psrbagconclOLD IVFDjSFfjS
17 12 14 15 16 syl3anc φjSFfjS
18 13 17 sselid φjSFfjD
19 eqid xD|xfFfj=xD|xfFfj
20 1 19 psrbagconf1oOLD IVFfjDmxD|xfFfjFfjfm:xD|xfFfj1-1 ontoxD|xfFfj
21 12 18 20 syl2anc φjSmxD|xfFfjFfjfm:xD|xfFfj1-1 ontoxD|xfFfj
22 f1of mxD|xfFfjFfjfm:xD|xfFfj1-1 ontoxD|xfFfjmxD|xfFfjFfjfm:xD|xfFfjxD|xfFfj
23 21 22 syl φjSmxD|xfFfjFfjfm:xD|xfFfjxD|xfFfj
24 fco kxD|xfFfjX:xD|xfFfjBmxD|xfFfjFfjfm:xD|xfFfjxD|xfFfjkxD|xfFfjXmxD|xfFfjFfjfm:xD|xfFfjB
25 11 23 24 syl2anc φjSkxD|xfFfjXmxD|xfFfjFfjfm:xD|xfFfjB
26 12 adantr φjSmxD|xfFfjIV
27 14 adantr φjSmxD|xfFfjFD
28 1 psrbagfOLD IVFDF:I0
29 26 27 28 syl2anc φjSmxD|xfFfjF:I0
30 29 ffvelrnda φjSmxD|xfFfjzIFz0
31 15 adantr φjSmxD|xfFfjjS
32 13 31 sselid φjSmxD|xfFfjjD
33 1 psrbagfOLD IVjDj:I0
34 26 32 33 syl2anc φjSmxD|xfFfjj:I0
35 34 ffvelrnda φjSmxD|xfFfjzIjz0
36 ssrab2 xD|xfFfjD
37 simpr φjSmxD|xfFfjmxD|xfFfj
38 36 37 sselid φjSmxD|xfFfjmD
39 1 psrbagfOLD IVmDm:I0
40 26 38 39 syl2anc φjSmxD|xfFfjm:I0
41 40 ffvelrnda φjSmxD|xfFfjzImz0
42 nn0cn Fz0Fz
43 nn0cn jz0jz
44 nn0cn mz0mz
45 sub32 FzjzmzFz-jz-mz=Fz-mz-jz
46 42 43 44 45 syl3an Fz0jz0mz0Fz-jz-mz=Fz-mz-jz
47 30 35 41 46 syl3anc φjSmxD|xfFfjzIFz-jz-mz=Fz-mz-jz
48 47 mpteq2dva φjSmxD|xfFfjzIFz-jz-mz=zIFz-mz-jz
49 ovexd φjSmxD|xfFfjzIFzjzV
50 29 feqmptd φjSmxD|xfFfjF=zIFz
51 34 feqmptd φjSmxD|xfFfjj=zIjz
52 26 30 35 50 51 offval2 φjSmxD|xfFfjFfj=zIFzjz
53 40 feqmptd φjSmxD|xfFfjm=zImz
54 26 49 41 52 53 offval2 φjSmxD|xfFfjFfjfm=zIFz-jz-mz
55 ovexd φjSmxD|xfFfjzIFzmzV
56 26 30 41 50 53 offval2 φjSmxD|xfFfjFfm=zIFzmz
57 26 55 35 56 51 offval2 φjSmxD|xfFfjFfmfj=zIFz-mz-jz
58 48 54 57 3eqtr4d φjSmxD|xfFfjFfjfm=Ffmfj
59 18 adantr φjSmxD|xfFfjFfjD
60 1 19 psrbagconclOLD IVFfjDmxD|xfFfjFfjfmxD|xfFfj
61 26 59 37 60 syl3anc φjSmxD|xfFfjFfjfmxD|xfFfj
62 58 61 eqeltrrd φjSmxD|xfFfjFfmfjxD|xfFfj
63 58 mpteq2dva φjSmxD|xfFfjFfjfm=mxD|xfFfjFfmfj
64 nfcv _nX
65 nfcsb1v _kn/kX
66 csbeq1a k=nX=n/kX
67 64 65 66 cbvmpt kxD|xfFfjX=nxD|xfFfjn/kX
68 67 a1i φjSkxD|xfFfjX=nxD|xfFfjn/kX
69 csbeq1 n=Ffmfjn/kX=Ffmfj/kX
70 62 63 68 69 fmptco φjSkxD|xfFfjXmxD|xfFfjFfjfm=mxD|xfFfjFfmfj/kX
71 70 feq1d φjSkxD|xfFfjXmxD|xfFfjFfjfm:xD|xfFfjBmxD|xfFfjFfmfj/kX:xD|xfFfjB
72 25 71 mpbid φjSmxD|xfFfjFfmfj/kX:xD|xfFfjB
73 72 fvmptelrn φjSmxD|xfFfjFfmfj/kXB
74 73 anasss φjSmxD|xfFfjFfmfj/kXB
75 9 74 syldan φmSjxD|xfFfmFfmfj/kXB
76 1 2 3 4 5 6 75 gsumbagdiagOLD φGmS,jxD|xfFfmFfmfj/kX=GjS,mxD|xfFfjFfmfj/kX
77 eqid 0G=0G
78 1 psrbaglefiOLD IVFDyD|yfFFin
79 3 4 78 syl2anc φyD|yfFFin
80 2 79 eqeltrid φSFin
81 3 adantr φmSIV
82 4 adantr φmSFD
83 simpr φmSmS
84 1 2 psrbagconclOLD IVFDmSFfmS
85 81 82 83 84 syl3anc φmSFfmS
86 13 85 sselid φmSFfmD
87 1 psrbaglefiOLD IVFfmDxD|xfFfmFin
88 81 86 87 syl2anc φmSxD|xfFfmFin
89 xpfi SFinSFinS×SFin
90 80 80 89 syl2anc φS×SFin
91 simprl φmSjxD|xfFfmmS
92 9 simpld φmSjxD|xfFfmjS
93 brxp mS×SjmSjS
94 91 92 93 sylanbrc φmSjxD|xfFfmmS×Sj
95 94 pm2.24d φmSjxD|xfFfm¬mS×SjFfmfj/kX=0G
96 95 impr φmSjxD|xfFfm¬mS×SjFfmfj/kX=0G
97 5 77 6 80 88 75 90 96 gsum2d2 φGmS,jxD|xfFfmFfmfj/kX=GmSGjxD|xfFfmFfmfj/kX
98 1 psrbaglefiOLD IVFfjDxD|xfFfjFin
99 12 18 98 syl2anc φjSxD|xfFfjFin
100 simprl φjSmxD|xfFfjjS
101 1 2 3 4 gsumbagdiaglemOLD φjSmxD|xfFfjmSjxD|xfFfm
102 101 simpld φjSmxD|xfFfjmS
103 brxp jS×SmjSmS
104 100 102 103 sylanbrc φjSmxD|xfFfjjS×Sm
105 104 pm2.24d φjSmxD|xfFfj¬jS×SmFfmfj/kX=0G
106 105 impr φjSmxD|xfFfj¬jS×SmFfmfj/kX=0G
107 5 77 6 80 99 74 90 106 gsum2d2 φGjS,mxD|xfFfjFfmfj/kX=GjSGmxD|xfFfjFfmfj/kX
108 76 97 107 3eqtr3d φGmSGjxD|xfFfmFfmfj/kX=GjSGmxD|xfFfjFfmfj/kX
109 6 adantr φmSGCMnd
110 75 anassrs φmSjxD|xfFfmFfmfj/kXB
111 110 fmpttd φmSjxD|xfFfmFfmfj/kX:xD|xfFfmB
112 ovex 0IV
113 1 112 rabex2 DV
114 113 a1i φmSDV
115 rabexg DVxD|xfFfmV
116 mptexg xD|xfFfmVjxD|xfFfmFfmfj/kXV
117 114 115 116 3syl φmSjxD|xfFfmFfmfj/kXV
118 funmpt FunjxD|xfFfmFfmfj/kX
119 118 a1i φmSFunjxD|xfFfmFfmfj/kX
120 fvexd φmS0GV
121 suppssdm jxD|xfFfmFfmfj/kXsupp0GdomjxD|xfFfmFfmfj/kX
122 eqid jxD|xfFfmFfmfj/kX=jxD|xfFfmFfmfj/kX
123 122 dmmptss domjxD|xfFfmFfmfj/kXxD|xfFfm
124 121 123 sstri jxD|xfFfmFfmfj/kXsupp0GxD|xfFfm
125 124 a1i φmSjxD|xfFfmFfmfj/kXsupp0GxD|xfFfm
126 suppssfifsupp jxD|xfFfmFfmfj/kXVFunjxD|xfFfmFfmfj/kX0GVxD|xfFfmFinjxD|xfFfmFfmfj/kXsupp0GxD|xfFfmfinSupp0GjxD|xfFfmFfmfj/kX
127 117 119 120 88 125 126 syl32anc φmSfinSupp0GjxD|xfFfmFfmfj/kX
128 5 77 109 88 111 127 gsumcl φmSGjxD|xfFfmFfmfj/kXB
129 128 fmpttd φmSGjxD|xfFfmFfmfj/kX:SB
130 1 2 psrbagconf1oOLD IVFDmSFfm:S1-1 ontoS
131 3 4 130 syl2anc φmSFfm:S1-1 ontoS
132 f1ocnv mSFfm:S1-1 ontoSmSFfm-1:S1-1 ontoS
133 f1of mSFfm-1:S1-1 ontoSmSFfm-1:SS
134 131 132 133 3syl φmSFfm-1:SS
135 fco mSGjxD|xfFfmFfmfj/kX:SBmSFfm-1:SSmSGjxD|xfFfmFfmfj/kXmSFfm-1:SB
136 129 134 135 syl2anc φmSGjxD|xfFfmFfmfj/kXmSFfm-1:SB
137 coass nSGjxD|xfnYmSFfmmSFfm-1=nSGjxD|xfnYmSFfmmSFfm-1
138 f1ococnv2 mSFfm:S1-1 ontoSmSFfmmSFfm-1=IS
139 131 138 syl φmSFfmmSFfm-1=IS
140 139 coeq2d φnSGjxD|xfnYmSFfmmSFfm-1=nSGjxD|xfnYIS
141 137 140 eqtrid φnSGjxD|xfnYmSFfmmSFfm-1=nSGjxD|xfnYIS
142 eqidd φmSFfm=mSFfm
143 eqidd φnSGjxD|xfnY=nSGjxD|xfnY
144 breq2 n=FfmxfnxfFfm
145 144 rabbidv n=FfmxD|xfn=xD|xfFfm
146 ovex nfjV
147 146 8 csbie nfj/kX=Y
148 oveq1 n=Ffmnfj=Ffmfj
149 148 csbeq1d n=Ffmnfj/kX=Ffmfj/kX
150 147 149 eqtr3id n=FfmY=Ffmfj/kX
151 145 150 mpteq12dv n=FfmjxD|xfnY=jxD|xfFfmFfmfj/kX
152 151 oveq2d n=FfmGjxD|xfnY=GjxD|xfFfmFfmfj/kX
153 85 142 143 152 fmptco φnSGjxD|xfnYmSFfm=mSGjxD|xfFfmFfmfj/kX
154 153 coeq1d φnSGjxD|xfnYmSFfmmSFfm-1=mSGjxD|xfFfmFfmfj/kXmSFfm-1
155 coires1 nSGjxD|xfnYIS=nSGjxD|xfnYS
156 ssid SS
157 resmpt SSnSGjxD|xfnYS=nSGjxD|xfnY
158 156 157 ax-mp nSGjxD|xfnYS=nSGjxD|xfnY
159 155 158 eqtri nSGjxD|xfnYIS=nSGjxD|xfnY
160 159 a1i φnSGjxD|xfnYIS=nSGjxD|xfnY
161 141 154 160 3eqtr3d φmSGjxD|xfFfmFfmfj/kXmSFfm-1=nSGjxD|xfnY
162 161 feq1d φmSGjxD|xfFfmFfmfj/kXmSFfm-1:SBnSGjxD|xfnY:SB
163 136 162 mpbid φnSGjxD|xfnY:SB
164 rabexg DVyD|yfFV
165 113 164 mp1i φyD|yfFV
166 2 165 eqeltrid φSV
167 166 mptexd φnSGjxD|xfnYV
168 funmpt FunnSGjxD|xfnY
169 168 a1i φFunnSGjxD|xfnY
170 fvexd φ0GV
171 suppssdm nSGjxD|xfnYsupp0GdomnSGjxD|xfnY
172 eqid nSGjxD|xfnY=nSGjxD|xfnY
173 172 dmmptss domnSGjxD|xfnYS
174 171 173 sstri nSGjxD|xfnYsupp0GS
175 174 a1i φnSGjxD|xfnYsupp0GS
176 suppssfifsupp nSGjxD|xfnYVFunnSGjxD|xfnY0GVSFinnSGjxD|xfnYsupp0GSfinSupp0GnSGjxD|xfnY
177 167 169 170 80 175 176 syl32anc φfinSupp0GnSGjxD|xfnY
178 5 77 6 80 163 177 131 gsumf1o φGnSGjxD|xfnY=GnSGjxD|xfnYmSFfm
179 153 oveq2d φGnSGjxD|xfnYmSFfm=GmSGjxD|xfFfmFfmfj/kX
180 178 179 eqtrd φGnSGjxD|xfnY=GmSGjxD|xfFfmFfmfj/kX
181 6 adantr φjSGCMnd
182 113 a1i φjSDV
183 rabexg DVxD|xfFfjV
184 mptexg xD|xfFfjVkxD|xfFfjXV
185 182 183 184 3syl φjSkxD|xfFfjXV
186 funmpt FunkxD|xfFfjX
187 186 a1i φjSFunkxD|xfFfjX
188 fvexd φjS0GV
189 suppssdm kxD|xfFfjXsupp0GdomkxD|xfFfjX
190 eqid kxD|xfFfjX=kxD|xfFfjX
191 190 dmmptss domkxD|xfFfjXxD|xfFfj
192 189 191 sstri kxD|xfFfjXsupp0GxD|xfFfj
193 192 a1i φjSkxD|xfFfjXsupp0GxD|xfFfj
194 suppssfifsupp kxD|xfFfjXVFunkxD|xfFfjX0GVxD|xfFfjFinkxD|xfFfjXsupp0GxD|xfFfjfinSupp0GkxD|xfFfjX
195 185 187 188 99 193 194 syl32anc φjSfinSupp0GkxD|xfFfjX
196 5 77 181 99 11 195 21 gsumf1o φjSGkxD|xfFfjX=GkxD|xfFfjXmxD|xfFfjFfjfm
197 70 oveq2d φjSGkxD|xfFfjXmxD|xfFfjFfjfm=GmxD|xfFfjFfmfj/kX
198 196 197 eqtrd φjSGkxD|xfFfjX=GmxD|xfFfjFfmfj/kX
199 198 mpteq2dva φjSGkxD|xfFfjX=jSGmxD|xfFfjFfmfj/kX
200 199 oveq2d φGjSGkxD|xfFfjX=GjSGmxD|xfFfjFfmfj/kX
201 108 180 200 3eqtr4d φGnSGjxD|xfnY=GjSGkxD|xfFfjX