Metamath Proof Explorer

Theorem psrgsum

Description: Finite commutative sums of power series are taken componentwise. (Contributed by Thierry Arnoux, 16-Mar-2026)

Ref Expression
Hypotheses psrgsum.s 
|- S = ( I mPwSer R )
psrgsum.b 
|- B = ( Base ` S )
psrgsum.r 
|- ( ph -> R e. Ring )
psrgsum.i 
|- ( ph -> I e. V )
psrgsum.d 
|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
psrgsum.a 
|- ( ph -> A e. Fin )
psrgsum.f 
|- ( ph -> F : A --> B )
Assertion psrgsum 
|- ( ph -> ( S gsum F ) = ( y e. D |-> ( R gsum ( k e. A |-> ( ( F ` k ) ` y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 psrgsum.s 
 |-  S = ( I mPwSer R )
2 psrgsum.b 
 |-  B = ( Base ` S )
3 psrgsum.r 
 |-  ( ph -> R e. Ring )
4 psrgsum.i 
 |-  ( ph -> I e. V )
5 psrgsum.d 
 |-  D = { h e. ( NN0 ^m I ) | h finSupp 0 }
6 psrgsum.a 
 |-  ( ph -> A e. Fin )
7 psrgsum.f 
 |-  ( ph -> F : A --> B )
8 7 feqmptd 
 |-  ( ph -> F = ( k e. A |-> ( F ` k ) ) )
9 8 oveq2d 
 |-  ( ph -> ( S gsum F ) = ( S gsum ( k e. A |-> ( F ` k ) ) ) )
10 mpteq1 
 |-  ( a = (/) -> ( k e. a |-> ( F ` k ) ) = ( k e. (/) |-> ( F ` k ) ) )
11 10 oveq2d 
 |-  ( a = (/) -> ( S gsum ( k e. a |-> ( F ` k ) ) ) = ( S gsum ( k e. (/) |-> ( F ` k ) ) ) )
12 mpteq1 
 |-  ( a = (/) -> ( k e. a |-> ( ( F ` k ) ` y ) ) = ( k e. (/) |-> ( ( F ` k ) ` y ) ) )
13 12 oveq2d 
 |-  ( a = (/) -> ( R gsum ( k e. a |-> ( ( F ` k ) ` y ) ) ) = ( R gsum ( k e. (/) |-> ( ( F ` k ) ` y ) ) ) )
14 13 mpteq2dv 
 |-  ( a = (/) -> ( y e. D |-> ( R gsum ( k e. a |-> ( ( F ` k ) ` y ) ) ) ) = ( y e. D |-> ( R gsum ( k e. (/) |-> ( ( F ` k ) ` y ) ) ) ) )
15 11 14 eqeq12d 
 |-  ( a = (/) -> ( ( S gsum ( k e. a |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. a |-> ( ( F ` k ) ` y ) ) ) ) <-> ( S gsum ( k e. (/) |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. (/) |-> ( ( F ` k ) ` y ) ) ) ) ) )
16 mpteq1 
 |-  ( a = b -> ( k e. a |-> ( F ` k ) ) = ( k e. b |-> ( F ` k ) ) )
17 16 oveq2d 
 |-  ( a = b -> ( S gsum ( k e. a |-> ( F ` k ) ) ) = ( S gsum ( k e. b |-> ( F ` k ) ) ) )
18 mpteq1 
 |-  ( a = b -> ( k e. a |-> ( ( F ` k ) ` y ) ) = ( k e. b |-> ( ( F ` k ) ` y ) ) )
19 18 oveq2d 
 |-  ( a = b -> ( R gsum ( k e. a |-> ( ( F ` k ) ` y ) ) ) = ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) )
20 19 mpteq2dv 
 |-  ( a = b -> ( y e. D |-> ( R gsum ( k e. a |-> ( ( F ` k ) ` y ) ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) )
21 17 20 eqeq12d 
 |-  ( a = b -> ( ( S gsum ( k e. a |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. a |-> ( ( F ` k ) ` y ) ) ) ) <-> ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) )
22 mpteq1 
 |-  ( a = ( b u. { f } ) -> ( k e. a |-> ( F ` k ) ) = ( k e. ( b u. { f } ) |-> ( F ` k ) ) )
23 fveq2 
 |-  ( k = l -> ( F ` k ) = ( F ` l ) )
24 23 cbvmptv 
 |-  ( k e. ( b u. { f } ) |-> ( F ` k ) ) = ( l e. ( b u. { f } ) |-> ( F ` l ) )
25 22 24 eqtrdi 
 |-  ( a = ( b u. { f } ) -> ( k e. a |-> ( F ` k ) ) = ( l e. ( b u. { f } ) |-> ( F ` l ) ) )
26 25 oveq2d 
 |-  ( a = ( b u. { f } ) -> ( S gsum ( k e. a |-> ( F ` k ) ) ) = ( S gsum ( l e. ( b u. { f } ) |-> ( F ` l ) ) ) )
27 mpteq1 
 |-  ( a = ( b u. { f } ) -> ( k e. a |-> ( ( F ` k ) ` y ) ) = ( k e. ( b u. { f } ) |-> ( ( F ` k ) ` y ) ) )
28 27 oveq2d 
 |-  ( a = ( b u. { f } ) -> ( R gsum ( k e. a |-> ( ( F ` k ) ` y ) ) ) = ( R gsum ( k e. ( b u. { f } ) |-> ( ( F ` k ) ` y ) ) ) )
29 28 mpteq2dv 
 |-  ( a = ( b u. { f } ) -> ( y e. D |-> ( R gsum ( k e. a |-> ( ( F ` k ) ` y ) ) ) ) = ( y e. D |-> ( R gsum ( k e. ( b u. { f } ) |-> ( ( F ` k ) ` y ) ) ) ) )
30 26 29 eqeq12d 
 |-  ( a = ( b u. { f } ) -> ( ( S gsum ( k e. a |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. a |-> ( ( F ` k ) ` y ) ) ) ) <-> ( S gsum ( l e. ( b u. { f } ) |-> ( F ` l ) ) ) = ( y e. D |-> ( R gsum ( k e. ( b u. { f } ) |-> ( ( F ` k ) ` y ) ) ) ) ) )
31 mpteq1 
 |-  ( a = A -> ( k e. a |-> ( F ` k ) ) = ( k e. A |-> ( F ` k ) ) )
32 31 oveq2d 
 |-  ( a = A -> ( S gsum ( k e. a |-> ( F ` k ) ) ) = ( S gsum ( k e. A |-> ( F ` k ) ) ) )
33 mpteq1 
 |-  ( a = A -> ( k e. a |-> ( ( F ` k ) ` y ) ) = ( k e. A |-> ( ( F ` k ) ` y ) ) )
34 33 oveq2d 
 |-  ( a = A -> ( R gsum ( k e. a |-> ( ( F ` k ) ` y ) ) ) = ( R gsum ( k e. A |-> ( ( F ` k ) ` y ) ) ) )
35 34 mpteq2dv 
 |-  ( a = A -> ( y e. D |-> ( R gsum ( k e. a |-> ( ( F ` k ) ` y ) ) ) ) = ( y e. D |-> ( R gsum ( k e. A |-> ( ( F ` k ) ` y ) ) ) ) )
36 32 35 eqeq12d 
 |-  ( a = A -> ( ( S gsum ( k e. a |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. a |-> ( ( F ` k ) ` y ) ) ) ) <-> ( S gsum ( k e. A |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. A |-> ( ( F ` k ) ` y ) ) ) ) ) )
37 mpt0 
 |-  ( k e. (/) |-> ( F ` k ) ) = (/)
38 37 a1i 
 |-  ( ph -> ( k e. (/) |-> ( F ` k ) ) = (/) )
39 38 oveq2d 
 |-  ( ph -> ( S gsum ( k e. (/) |-> ( F ` k ) ) ) = ( S gsum (/) ) )
40 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
41 40 gsum0 
 |-  ( S gsum (/) ) = ( 0g ` S )
42 41 a1i 
 |-  ( ph -> ( S gsum (/) ) = ( 0g ` S ) )
43 fconstmpt 
 |-  ( D X. { ( 0g ` R ) } ) = ( y e. D |-> ( 0g ` R ) )
44 3 ringgrpd 
 |-  ( ph -> R e. Grp )
45 5 psrbasfsupp 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
46 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
47 1 4 44 45 46 40 psr0 
 |-  ( ph -> ( 0g ` S ) = ( D X. { ( 0g ` R ) } ) )
48 mpt0 
 |-  ( k e. (/) |-> ( ( F ` k ) ` y ) ) = (/)
49 48 oveq2i 
 |-  ( R gsum ( k e. (/) |-> ( ( F ` k ) ` y ) ) ) = ( R gsum (/) )
50 46 gsum0 
 |-  ( R gsum (/) ) = ( 0g ` R )
51 49 50 eqtri 
 |-  ( R gsum ( k e. (/) |-> ( ( F ` k ) ` y ) ) ) = ( 0g ` R )
52 51 a1i 
 |-  ( ph -> ( R gsum ( k e. (/) |-> ( ( F ` k ) ` y ) ) ) = ( 0g ` R ) )
53 52 mpteq2dv 
 |-  ( ph -> ( y e. D |-> ( R gsum ( k e. (/) |-> ( ( F ` k ) ` y ) ) ) ) = ( y e. D |-> ( 0g ` R ) ) )
54 43 47 53 3eqtr4a 
 |-  ( ph -> ( 0g ` S ) = ( y e. D |-> ( R gsum ( k e. (/) |-> ( ( F ` k ) ` y ) ) ) ) )
55 39 42 54 3eqtrd 
 |-  ( ph -> ( S gsum ( k e. (/) |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. (/) |-> ( ( F ` k ) ` y ) ) ) ) )
56 ovex 
 |-  ( NN0 ^m I ) e. _V
57 5 56 rabex2 
 |-  D e. _V
58 nfv 
 |-  F/ y ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) )
59 ovexd 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ y e. D ) -> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) e. _V )
60 eqid 
 |-  ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) )
61 58 59 60 fnmptd 
 |-  ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) Fn D )
62 fvexd 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ y e. D ) -> ( ( F ` f ) ` y ) e. _V )
63 eqid 
 |-  ( y e. D |-> ( ( F ` f ) ` y ) ) = ( y e. D |-> ( ( F ` f ) ` y ) )
64 58 62 63 fnmptd 
 |-  ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( y e. D |-> ( ( F ` f ) ` y ) ) Fn D )
65 ofmpteq 
 |-  ( ( D e. _V /\ ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) Fn D /\ ( y e. D |-> ( ( F ` f ) ` y ) ) Fn D ) -> ( ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) oF ( +g ` R ) ( y e. D |-> ( ( F ` f ) ` y ) ) ) = ( y e. D |-> ( ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ( +g ` R ) ( ( F ` f ) ` y ) ) ) )
66 57 61 64 65 mp3an2i 
 |-  ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) oF ( +g ` R ) ( y e. D |-> ( ( F ` f ) ` y ) ) ) = ( y e. D |-> ( ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ( +g ` R ) ( ( F ` f ) ` y ) ) ) )
67 66 adantr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> ( ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) oF ( +g ` R ) ( y e. D |-> ( ( F ` f ) ` y ) ) ) = ( y e. D |-> ( ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ( +g ` R ) ( ( F ` f ) ` y ) ) ) )
68 eqid 
 |-  ( +g ` S ) = ( +g ` S )
69 1 4 3 psrring 
 |-  ( ph -> S e. Ring )
70 69 ringcmnd 
 |-  ( ph -> S e. CMnd )
71 70 ad3antrrr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> S e. CMnd )
72 6 ad3antrrr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> A e. Fin )
73 simpllr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> b C_ A )
74 72 73 ssfid 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> b e. Fin )
75 7 ad4antr 
 |-  ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) /\ l e. b ) -> F : A --> B )
76 73 sselda 
 |-  ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) /\ l e. b ) -> l e. A )
77 75 76 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) /\ l e. b ) -> ( F ` l ) e. B )
78 simplr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> f e. ( A \ b ) )
79 78 eldifbd 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> -. f e. b )
80 7 ad3antrrr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> F : A --> B )
81 78 eldifad 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> f e. A )
82 80 81 ffvelcdmd 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> ( F ` f ) e. B )
83 fveq2 
 |-  ( l = f -> ( F ` l ) = ( F ` f ) )
84 2 68 71 74 77 78 79 82 83 gsumunsn 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> ( S gsum ( l e. ( b u. { f } ) |-> ( F ` l ) ) ) = ( ( S gsum ( l e. b |-> ( F ` l ) ) ) ( +g ` S ) ( F ` f ) ) )
85 eqid 
 |-  ( +g ` R ) = ( +g ` R )
86 77 fmpttd 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> ( l e. b |-> ( F ` l ) ) : b --> B )
87 eqid 
 |-  ( l e. b |-> ( F ` l ) ) = ( l e. b |-> ( F ` l ) )
88 fvexd 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> ( 0g ` S ) e. _V )
89 87 74 77 88 fsuppmptdm 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> ( l e. b |-> ( F ` l ) ) finSupp ( 0g ` S ) )
90 2 40 71 74 86 89 gsumcl 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> ( S gsum ( l e. b |-> ( F ` l ) ) ) e. B )
91 1 2 85 68 90 82 psradd 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> ( ( S gsum ( l e. b |-> ( F ` l ) ) ) ( +g ` S ) ( F ` f ) ) = ( ( S gsum ( l e. b |-> ( F ` l ) ) ) oF ( +g ` R ) ( F ` f ) ) )
92 23 cbvmptv 
 |-  ( k e. b |-> ( F ` k ) ) = ( l e. b |-> ( F ` l ) )
93 92 oveq2i 
 |-  ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( S gsum ( l e. b |-> ( F ` l ) ) )
94 simpr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) )
95 93 94 eqtr3id 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> ( S gsum ( l e. b |-> ( F ` l ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) )
96 eqid 
 |-  ( Base ` R ) = ( Base ` R )
97 1 96 45 2 82 psrelbas 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> ( F ` f ) : D --> ( Base ` R ) )
98 97 feqmptd 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> ( F ` f ) = ( y e. D |-> ( ( F ` f ) ` y ) ) )
99 95 98 oveq12d 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> ( ( S gsum ( l e. b |-> ( F ` l ) ) ) oF ( +g ` R ) ( F ` f ) ) = ( ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) oF ( +g ` R ) ( y e. D |-> ( ( F ` f ) ` y ) ) ) )
100 84 91 99 3eqtrd 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> ( S gsum ( l e. ( b u. { f } ) |-> ( F ` l ) ) ) = ( ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) oF ( +g ` R ) ( y e. D |-> ( ( F ` f ) ` y ) ) ) )
101 3 ringcmnd 
 |-  ( ph -> R e. CMnd )
102 101 ad3antrrr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ y e. D ) -> R e. CMnd )
103 6 ad3antrrr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ y e. D ) -> A e. Fin )
104 simpllr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ y e. D ) -> b C_ A )
105 103 104 ssfid 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ y e. D ) -> b e. Fin )
106 7 ad4antr 
 |-  ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ y e. D ) /\ k e. b ) -> F : A --> B )
107 104 sselda 
 |-  ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ y e. D ) /\ k e. b ) -> k e. A )
108 106 107 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ y e. D ) /\ k e. b ) -> ( F ` k ) e. B )
109 1 96 45 2 108 psrelbas 
 |-  ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ y e. D ) /\ k e. b ) -> ( F ` k ) : D --> ( Base ` R ) )
110 simplr 
 |-  ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ y e. D ) /\ k e. b ) -> y e. D )
111 109 110 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ y e. D ) /\ k e. b ) -> ( ( F ` k ) ` y ) e. ( Base ` R ) )
112 simplr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ y e. D ) -> f e. ( A \ b ) )
113 112 eldifbd 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ y e. D ) -> -. f e. b )
114 7 ad2antrr 
 |-  ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> F : A --> B )
115 simpr 
 |-  ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> f e. ( A \ b ) )
116 115 eldifad 
 |-  ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> f e. A )
117 114 116 ffvelcdmd 
 |-  ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( F ` f ) e. B )
118 1 96 45 2 117 psrelbas 
 |-  ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( F ` f ) : D --> ( Base ` R ) )
119 118 ffvelcdmda 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ y e. D ) -> ( ( F ` f ) ` y ) e. ( Base ` R ) )
120 fveq2 
 |-  ( k = f -> ( F ` k ) = ( F ` f ) )
121 120 fveq1d 
 |-  ( k = f -> ( ( F ` k ) ` y ) = ( ( F ` f ) ` y ) )
122 96 85 102 105 111 112 113 119 121 gsumunsn 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ y e. D ) -> ( R gsum ( k e. ( b u. { f } ) |-> ( ( F ` k ) ` y ) ) ) = ( ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ( +g ` R ) ( ( F ` f ) ` y ) ) )
123 122 mpteq2dva 
 |-  ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( y e. D |-> ( R gsum ( k e. ( b u. { f } ) |-> ( ( F ` k ) ` y ) ) ) ) = ( y e. D |-> ( ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ( +g ` R ) ( ( F ` f ) ` y ) ) ) )
124 123 adantr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> ( y e. D |-> ( R gsum ( k e. ( b u. { f } ) |-> ( ( F ` k ) ` y ) ) ) ) = ( y e. D |-> ( ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ( +g ` R ) ( ( F ` f ) ` y ) ) ) )
125 67 100 124 3eqtr4d 
 |-  ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) ) -> ( S gsum ( l e. ( b u. { f } ) |-> ( F ` l ) ) ) = ( y e. D |-> ( R gsum ( k e. ( b u. { f } ) |-> ( ( F ` k ) ` y ) ) ) ) )
126 125 ex 
 |-  ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) -> ( S gsum ( l e. ( b u. { f } ) |-> ( F ` l ) ) ) = ( y e. D |-> ( R gsum ( k e. ( b u. { f } ) |-> ( ( F ` k ) ` y ) ) ) ) ) )
127 126 anasss 
 |-  ( ( ph /\ ( b C_ A /\ f e. ( A \ b ) ) ) -> ( ( S gsum ( k e. b |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. b |-> ( ( F ` k ) ` y ) ) ) ) -> ( S gsum ( l e. ( b u. { f } ) |-> ( F ` l ) ) ) = ( y e. D |-> ( R gsum ( k e. ( b u. { f } ) |-> ( ( F ` k ) ` y ) ) ) ) ) )
128 15 21 30 36 55 127 6 findcard2d 
 |-  ( ph -> ( S gsum ( k e. A |-> ( F ` k ) ) ) = ( y e. D |-> ( R gsum ( k e. A |-> ( ( F ` k ) ` y ) ) ) ) )
129 9 128 eqtrd 
 |-  ( ph -> ( S gsum F ) = ( y e. D |-> ( R gsum ( k e. A |-> ( ( F ` k ) ` y ) ) ) ) )