Step |
Hyp |
Ref |
Expression |
1 |
|
gsummpt2co.b |
|- B = ( Base ` W ) |
2 |
|
gsummpt2co.z |
|- .0. = ( 0g ` W ) |
3 |
|
gsummpt2co.w |
|- ( ph -> W e. CMnd ) |
4 |
|
gsummpt2co.a |
|- ( ph -> A e. Fin ) |
5 |
|
gsummpt2co.e |
|- ( ph -> E e. V ) |
6 |
|
gsummpt2co.1 |
|- ( ( ph /\ x e. A ) -> C e. B ) |
7 |
|
gsummpt2co.2 |
|- ( ( ph /\ x e. A ) -> D e. E ) |
8 |
|
gsummpt2co.3 |
|- F = ( x e. A |-> D ) |
9 |
|
nfcsb1v |
|- F/_ x [_ ( 2nd ` p ) / x ]_ C |
10 |
|
csbeq1a |
|- ( x = ( 2nd ` p ) -> C = [_ ( 2nd ` p ) / x ]_ C ) |
11 |
|
ssidd |
|- ( ph -> B C_ B ) |
12 |
|
elcnv |
|- ( p e. `' F <-> E. z E. x ( p = <. z , x >. /\ x F z ) ) |
13 |
|
vex |
|- z e. _V |
14 |
|
vex |
|- x e. _V |
15 |
13 14
|
op2ndd |
|- ( p = <. z , x >. -> ( 2nd ` p ) = x ) |
16 |
15
|
adantr |
|- ( ( p = <. z , x >. /\ x F z ) -> ( 2nd ` p ) = x ) |
17 |
8
|
dmmptss |
|- dom F C_ A |
18 |
14 13
|
breldm |
|- ( x F z -> x e. dom F ) |
19 |
17 18
|
sseldi |
|- ( x F z -> x e. A ) |
20 |
19
|
adantl |
|- ( ( p = <. z , x >. /\ x F z ) -> x e. A ) |
21 |
16 20
|
eqeltrd |
|- ( ( p = <. z , x >. /\ x F z ) -> ( 2nd ` p ) e. A ) |
22 |
21
|
exlimivv |
|- ( E. z E. x ( p = <. z , x >. /\ x F z ) -> ( 2nd ` p ) e. A ) |
23 |
12 22
|
sylbi |
|- ( p e. `' F -> ( 2nd ` p ) e. A ) |
24 |
23
|
adantl |
|- ( ( ph /\ p e. `' F ) -> ( 2nd ` p ) e. A ) |
25 |
8
|
funmpt2 |
|- Fun F |
26 |
|
funcnvcnv |
|- ( Fun F -> Fun `' `' F ) |
27 |
25 26
|
ax-mp |
|- Fun `' `' F |
28 |
27
|
a1i |
|- ( ( ph /\ x e. A ) -> Fun `' `' F ) |
29 |
|
dfdm4 |
|- dom F = ran `' F |
30 |
8
|
dmeqi |
|- dom F = dom ( x e. A |-> D ) |
31 |
7
|
ralrimiva |
|- ( ph -> A. x e. A D e. E ) |
32 |
|
dmmptg |
|- ( A. x e. A D e. E -> dom ( x e. A |-> D ) = A ) |
33 |
31 32
|
syl |
|- ( ph -> dom ( x e. A |-> D ) = A ) |
34 |
30 33
|
syl5eq |
|- ( ph -> dom F = A ) |
35 |
29 34
|
syl5eqr |
|- ( ph -> ran `' F = A ) |
36 |
35
|
eleq2d |
|- ( ph -> ( x e. ran `' F <-> x e. A ) ) |
37 |
36
|
biimpar |
|- ( ( ph /\ x e. A ) -> x e. ran `' F ) |
38 |
|
relcnv |
|- Rel `' F |
39 |
|
fcnvgreu |
|- ( ( ( Rel `' F /\ Fun `' `' F ) /\ x e. ran `' F ) -> E! p e. `' F x = ( 2nd ` p ) ) |
40 |
38 39
|
mpanl1 |
|- ( ( Fun `' `' F /\ x e. ran `' F ) -> E! p e. `' F x = ( 2nd ` p ) ) |
41 |
28 37 40
|
syl2anc |
|- ( ( ph /\ x e. A ) -> E! p e. `' F x = ( 2nd ` p ) ) |
42 |
9 1 2 10 3 4 11 6 24 41
|
gsummptf1o |
|- ( ph -> ( W gsum ( x e. A |-> C ) ) = ( W gsum ( p e. `' F |-> [_ ( 2nd ` p ) / x ]_ C ) ) ) |
43 |
8
|
rnmptss |
|- ( A. x e. A D e. E -> ran F C_ E ) |
44 |
31 43
|
syl |
|- ( ph -> ran F C_ E ) |
45 |
|
dfcnv2 |
|- ( ran F C_ E -> `' F = U_ z e. E ( { z } X. ( `' F " { z } ) ) ) |
46 |
44 45
|
syl |
|- ( ph -> `' F = U_ z e. E ( { z } X. ( `' F " { z } ) ) ) |
47 |
46
|
mpteq1d |
|- ( ph -> ( p e. `' F |-> [_ ( 2nd ` p ) / x ]_ C ) = ( p e. U_ z e. E ( { z } X. ( `' F " { z } ) ) |-> [_ ( 2nd ` p ) / x ]_ C ) ) |
48 |
|
nfcv |
|- F/_ z [_ ( 2nd ` p ) / x ]_ C |
49 |
|
csbeq1 |
|- ( ( 2nd ` p ) = x -> [_ ( 2nd ` p ) / x ]_ C = [_ x / x ]_ C ) |
50 |
15 49
|
syl |
|- ( p = <. z , x >. -> [_ ( 2nd ` p ) / x ]_ C = [_ x / x ]_ C ) |
51 |
|
csbid |
|- [_ x / x ]_ C = C |
52 |
50 51
|
eqtrdi |
|- ( p = <. z , x >. -> [_ ( 2nd ` p ) / x ]_ C = C ) |
53 |
48 9 52
|
mpomptxf |
|- ( p e. U_ z e. E ( { z } X. ( `' F " { z } ) ) |-> [_ ( 2nd ` p ) / x ]_ C ) = ( z e. E , x e. ( `' F " { z } ) |-> C ) |
54 |
47 53
|
eqtrdi |
|- ( ph -> ( p e. `' F |-> [_ ( 2nd ` p ) / x ]_ C ) = ( z e. E , x e. ( `' F " { z } ) |-> C ) ) |
55 |
54
|
oveq2d |
|- ( ph -> ( W gsum ( p e. `' F |-> [_ ( 2nd ` p ) / x ]_ C ) ) = ( W gsum ( z e. E , x e. ( `' F " { z } ) |-> C ) ) ) |
56 |
|
mptfi |
|- ( A e. Fin -> ( x e. A |-> D ) e. Fin ) |
57 |
8 56
|
eqeltrid |
|- ( A e. Fin -> F e. Fin ) |
58 |
|
cnvfi |
|- ( F e. Fin -> `' F e. Fin ) |
59 |
4 57 58
|
3syl |
|- ( ph -> `' F e. Fin ) |
60 |
|
imaexg |
|- ( `' F e. Fin -> ( `' F " { z } ) e. _V ) |
61 |
59 60
|
syl |
|- ( ph -> ( `' F " { z } ) e. _V ) |
62 |
61
|
adantr |
|- ( ( ph /\ z e. E ) -> ( `' F " { z } ) e. _V ) |
63 |
|
simpll |
|- ( ( ( ph /\ z e. E ) /\ x e. ( `' F " { z } ) ) -> ph ) |
64 |
|
imassrn |
|- ( `' F " { z } ) C_ ran `' F |
65 |
64 29
|
sseqtrri |
|- ( `' F " { z } ) C_ dom F |
66 |
65 17
|
sstri |
|- ( `' F " { z } ) C_ A |
67 |
13 14
|
elimasn |
|- ( x e. ( `' F " { z } ) <-> <. z , x >. e. `' F ) |
68 |
67
|
biimpi |
|- ( x e. ( `' F " { z } ) -> <. z , x >. e. `' F ) |
69 |
68
|
adantl |
|- ( ( ( ph /\ z e. E ) /\ x e. ( `' F " { z } ) ) -> <. z , x >. e. `' F ) |
70 |
69 67
|
sylibr |
|- ( ( ( ph /\ z e. E ) /\ x e. ( `' F " { z } ) ) -> x e. ( `' F " { z } ) ) |
71 |
66 70
|
sseldi |
|- ( ( ( ph /\ z e. E ) /\ x e. ( `' F " { z } ) ) -> x e. A ) |
72 |
63 71 6
|
syl2anc |
|- ( ( ( ph /\ z e. E ) /\ x e. ( `' F " { z } ) ) -> C e. B ) |
73 |
72
|
anasss |
|- ( ( ph /\ ( z e. E /\ x e. ( `' F " { z } ) ) ) -> C e. B ) |
74 |
|
df-br |
|- ( z `' F x <-> <. z , x >. e. `' F ) |
75 |
69 74
|
sylibr |
|- ( ( ( ph /\ z e. E ) /\ x e. ( `' F " { z } ) ) -> z `' F x ) |
76 |
75
|
anasss |
|- ( ( ph /\ ( z e. E /\ x e. ( `' F " { z } ) ) ) -> z `' F x ) |
77 |
76
|
pm2.24d |
|- ( ( ph /\ ( z e. E /\ x e. ( `' F " { z } ) ) ) -> ( -. z `' F x -> C = .0. ) ) |
78 |
77
|
imp |
|- ( ( ( ph /\ ( z e. E /\ x e. ( `' F " { z } ) ) ) /\ -. z `' F x ) -> C = .0. ) |
79 |
78
|
anasss |
|- ( ( ph /\ ( ( z e. E /\ x e. ( `' F " { z } ) ) /\ -. z `' F x ) ) -> C = .0. ) |
80 |
1 2 3 5 62 73 59 79
|
gsum2d2 |
|- ( ph -> ( W gsum ( z e. E , x e. ( `' F " { z } ) |-> C ) ) = ( W gsum ( z e. E |-> ( W gsum ( x e. ( `' F " { z } ) |-> C ) ) ) ) ) |
81 |
42 55 80
|
3eqtrd |
|- ( ph -> ( W gsum ( x e. A |-> C ) ) = ( W gsum ( z e. E |-> ( W gsum ( x e. ( `' F " { z } ) |-> C ) ) ) ) ) |
82 |
|
nfcv |
|- F/_ z ( W gsum ( x e. ( `' F " { y } ) |-> C ) ) |
83 |
|
nfcv |
|- F/_ y ( W gsum ( x e. ( `' F " { z } ) |-> C ) ) |
84 |
|
sneq |
|- ( y = z -> { y } = { z } ) |
85 |
84
|
imaeq2d |
|- ( y = z -> ( `' F " { y } ) = ( `' F " { z } ) ) |
86 |
85
|
mpteq1d |
|- ( y = z -> ( x e. ( `' F " { y } ) |-> C ) = ( x e. ( `' F " { z } ) |-> C ) ) |
87 |
86
|
oveq2d |
|- ( y = z -> ( W gsum ( x e. ( `' F " { y } ) |-> C ) ) = ( W gsum ( x e. ( `' F " { z } ) |-> C ) ) ) |
88 |
82 83 87
|
cbvmpt |
|- ( y e. E |-> ( W gsum ( x e. ( `' F " { y } ) |-> C ) ) ) = ( z e. E |-> ( W gsum ( x e. ( `' F " { z } ) |-> C ) ) ) |
89 |
88
|
oveq2i |
|- ( W gsum ( y e. E |-> ( W gsum ( x e. ( `' F " { y } ) |-> C ) ) ) ) = ( W gsum ( z e. E |-> ( W gsum ( x e. ( `' F " { z } ) |-> C ) ) ) ) |
90 |
81 89
|
eqtr4di |
|- ( ph -> ( W gsum ( x e. A |-> C ) ) = ( W gsum ( y e. E |-> ( W gsum ( x e. ( `' F " { y } ) |-> C ) ) ) ) ) |