Metamath Proof Explorer

Theorem reprsuc

Description: Express the representations recursively. (Contributed by Thierry Arnoux, 5-Dec-2021)

Ref Expression
Hypotheses reprval.a 
|- ( ph -> A C_ NN )
reprval.m 
|- ( ph -> M e. ZZ )
reprval.s 
|- ( ph -> S e. NN0 )
reprsuc.f 
|- F = ( c e. ( A ( repr ` S ) ( M - b ) ) |-> ( c u. { <. S , b >. } ) )
Assertion reprsuc 
|- ( ph -> ( A ( repr ` ( S + 1 ) ) M ) = U_ b e. A ran F )

Proof

Step Hyp Ref Expression
1 reprval.a 
 |-  ( ph -> A C_ NN )
2 reprval.m 
 |-  ( ph -> M e. ZZ )
3 reprval.s 
 |-  ( ph -> S e. NN0 )
4 reprsuc.f 
 |-  F = ( c e. ( A ( repr ` S ) ( M - b ) ) |-> ( c u. { <. S , b >. } ) )
5 1nn0 
 |-  1 e. NN0
6 5 a1i 
 |-  ( ph -> 1 e. NN0 )
7 3 6 nn0addcld 
 |-  ( ph -> ( S + 1 ) e. NN0 )
8 1 2 7 reprval 
 |-  ( ph -> ( A ( repr ` ( S + 1 ) ) M ) = { c e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) | sum_ a e. ( 0 ..^ ( S + 1 ) ) ( c ` a ) = M } )
9 simplr 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) )
10 elmapi 
 |-  ( e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) -> e : ( 0 ..^ ( S + 1 ) ) --> A )
11 9 10 syl 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> e : ( 0 ..^ ( S + 1 ) ) --> A )
12 3 ad2antrr 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> S e. NN0 )
13 fzonn0p1 
 |-  ( S e. NN0 -> S e. ( 0 ..^ ( S + 1 ) ) )
14 12 13 syl 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> S e. ( 0 ..^ ( S + 1 ) ) )
15 11 14 ffvelrnd 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> ( e ` S ) e. A )
16 simpr 
 |-  ( ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) /\ b = ( e ` S ) ) -> b = ( e ` S ) )
17 16 oveq2d 
 |-  ( ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) /\ b = ( e ` S ) ) -> ( M - b ) = ( M - ( e ` S ) ) )
18 17 oveq2d 
 |-  ( ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) /\ b = ( e ` S ) ) -> ( A ( repr ` S ) ( M - b ) ) = ( A ( repr ` S ) ( M - ( e ` S ) ) ) )
19 opeq2 
 |-  ( b = ( e ` S ) -> <. S , b >. = <. S , ( e ` S ) >. )
20 19 sneqd 
 |-  ( b = ( e ` S ) -> { <. S , b >. } = { <. S , ( e ` S ) >. } )
21 20 uneq2d 
 |-  ( b = ( e ` S ) -> ( c u. { <. S , b >. } ) = ( c u. { <. S , ( e ` S ) >. } ) )
22 21 eqeq2d 
 |-  ( b = ( e ` S ) -> ( e = ( c u. { <. S , b >. } ) <-> e = ( c u. { <. S , ( e ` S ) >. } ) ) )
23 22 adantl 
 |-  ( ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) /\ b = ( e ` S ) ) -> ( e = ( c u. { <. S , b >. } ) <-> e = ( c u. { <. S , ( e ` S ) >. } ) ) )
24 18 23 rexeqbidv 
 |-  ( ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) /\ b = ( e ` S ) ) -> ( E. c e. ( A ( repr ` S ) ( M - b ) ) e = ( c u. { <. S , b >. } ) <-> E. c e. ( A ( repr ` S ) ( M - ( e ` S ) ) ) e = ( c u. { <. S , ( e ` S ) >. } ) ) )
25 10 adantl 
 |-  ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) -> e : ( 0 ..^ ( S + 1 ) ) --> A )
26 3 adantr 
 |-  ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) -> S e. NN0 )
27 fzossfzop1 
 |-  ( S e. NN0 -> ( 0 ..^ S ) C_ ( 0 ..^ ( S + 1 ) ) )
28 26 27 syl 
 |-  ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) -> ( 0 ..^ S ) C_ ( 0 ..^ ( S + 1 ) ) )
29 25 28 fssresd 
 |-  ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) -> ( e |` ( 0 ..^ S ) ) : ( 0 ..^ S ) --> A )
30 29 adantr 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> ( e |` ( 0 ..^ S ) ) : ( 0 ..^ S ) --> A )
31 nnex 
 |-  NN e. _V
32 31 a1i 
 |-  ( ph -> NN e. _V )
33 32 1 ssexd 
 |-  ( ph -> A e. _V )
34 fzofi 
 |-  ( 0 ..^ S ) e. Fin
35 34 elexi 
 |-  ( 0 ..^ S ) e. _V
36 elmapg 
 |-  ( ( A e. _V /\ ( 0 ..^ S ) e. _V ) -> ( ( e |` ( 0 ..^ S ) ) e. ( A ^m ( 0 ..^ S ) ) <-> ( e |` ( 0 ..^ S ) ) : ( 0 ..^ S ) --> A ) )
37 33 35 36 sylancl 
 |-  ( ph -> ( ( e |` ( 0 ..^ S ) ) e. ( A ^m ( 0 ..^ S ) ) <-> ( e |` ( 0 ..^ S ) ) : ( 0 ..^ S ) --> A ) )
38 37 ad2antrr 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> ( ( e |` ( 0 ..^ S ) ) e. ( A ^m ( 0 ..^ S ) ) <-> ( e |` ( 0 ..^ S ) ) : ( 0 ..^ S ) --> A ) )
39 30 38 mpbird 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> ( e |` ( 0 ..^ S ) ) e. ( A ^m ( 0 ..^ S ) ) )
40 34 a1i 
 |-  ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) -> ( 0 ..^ S ) e. Fin )
41 nnsscn 
 |-  NN C_ CC
42 41 a1i 
 |-  ( ph -> NN C_ CC )
43 1 42 sstrd 
 |-  ( ph -> A C_ CC )
44 43 ad2antrr 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ a e. ( 0 ..^ S ) ) -> A C_ CC )
45 29 ffvelrnda 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( e |` ( 0 ..^ S ) ) ` a ) e. A )
46 44 45 sseldd 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( e |` ( 0 ..^ S ) ) ` a ) e. CC )
47 40 46 fsumcl 
 |-  ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) -> sum_ a e. ( 0 ..^ S ) ( ( e |` ( 0 ..^ S ) ) ` a ) e. CC )
48 47 adantr 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> sum_ a e. ( 0 ..^ S ) ( ( e |` ( 0 ..^ S ) ) ` a ) e. CC )
49 43 adantr 
 |-  ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) -> A C_ CC )
50 26 13 syl 
 |-  ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) -> S e. ( 0 ..^ ( S + 1 ) ) )
51 25 50 ffvelrnd 
 |-  ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) -> ( e ` S ) e. A )
52 49 51 sseldd 
 |-  ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) -> ( e ` S ) e. CC )
53 52 adantr 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> ( e ` S ) e. CC )
54 48 53 pncand 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> ( ( sum_ a e. ( 0 ..^ S ) ( ( e |` ( 0 ..^ S ) ) ` a ) + ( e ` S ) ) - ( e ` S ) ) = sum_ a e. ( 0 ..^ S ) ( ( e |` ( 0 ..^ S ) ) ` a ) )
55 nfv 
 |-  F/ a ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) )
56 nfcv 
 |-  F/_ a ( e ` S )
57 fzonel 
 |-  -. S e. ( 0 ..^ S )
58 57 a1i 
 |-  ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) -> -. S e. ( 0 ..^ S ) )
59 25 adantr 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ a e. ( 0 ..^ S ) ) -> e : ( 0 ..^ ( S + 1 ) ) --> A )
60 28 sselda 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ a e. ( 0 ..^ S ) ) -> a e. ( 0 ..^ ( S + 1 ) ) )
61 59 60 ffvelrnd 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( e ` a ) e. A )
62 44 61 sseldd 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( e ` a ) e. CC )
63 fveq2 
 |-  ( a = S -> ( e ` a ) = ( e ` S ) )
64 55 56 40 26 58 62 63 52 fsumsplitsn 
 |-  ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) -> sum_ a e. ( ( 0 ..^ S ) u. { S } ) ( e ` a ) = ( sum_ a e. ( 0 ..^ S ) ( e ` a ) + ( e ` S ) ) )
65 fzosplitsn 
 |-  ( S e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( S + 1 ) ) = ( ( 0 ..^ S ) u. { S } ) )
66 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
67 65 66 eleq2s 
 |-  ( S e. NN0 -> ( 0 ..^ ( S + 1 ) ) = ( ( 0 ..^ S ) u. { S } ) )
68 26 67 syl 
 |-  ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) -> ( 0 ..^ ( S + 1 ) ) = ( ( 0 ..^ S ) u. { S } ) )
69 68 sumeq1d 
 |-  ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) -> sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = sum_ a e. ( ( 0 ..^ S ) u. { S } ) ( e ` a ) )
70 simpr 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ a e. ( 0 ..^ S ) ) -> a e. ( 0 ..^ S ) )
71 70 fvresd 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( e |` ( 0 ..^ S ) ) ` a ) = ( e ` a ) )
72 71 sumeq2dv 
 |-  ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) -> sum_ a e. ( 0 ..^ S ) ( ( e |` ( 0 ..^ S ) ) ` a ) = sum_ a e. ( 0 ..^ S ) ( e ` a ) )
73 72 oveq1d 
 |-  ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) -> ( sum_ a e. ( 0 ..^ S ) ( ( e |` ( 0 ..^ S ) ) ` a ) + ( e ` S ) ) = ( sum_ a e. ( 0 ..^ S ) ( e ` a ) + ( e ` S ) ) )
74 64 69 73 3eqtr4d 
 |-  ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) -> sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = ( sum_ a e. ( 0 ..^ S ) ( ( e |` ( 0 ..^ S ) ) ` a ) + ( e ` S ) ) )
75 74 adantr 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = ( sum_ a e. ( 0 ..^ S ) ( ( e |` ( 0 ..^ S ) ) ` a ) + ( e ` S ) ) )
76 simpr 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M )
77 75 76 eqtr3d 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> ( sum_ a e. ( 0 ..^ S ) ( ( e |` ( 0 ..^ S ) ) ` a ) + ( e ` S ) ) = M )
78 77 oveq1d 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> ( ( sum_ a e. ( 0 ..^ S ) ( ( e |` ( 0 ..^ S ) ) ` a ) + ( e ` S ) ) - ( e ` S ) ) = ( M - ( e ` S ) ) )
79 54 78 eqtr3d 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> sum_ a e. ( 0 ..^ S ) ( ( e |` ( 0 ..^ S ) ) ` a ) = ( M - ( e ` S ) ) )
80 39 79 jca 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> ( ( e |` ( 0 ..^ S ) ) e. ( A ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( ( e |` ( 0 ..^ S ) ) ` a ) = ( M - ( e ` S ) ) ) )
81 fveq1 
 |-  ( d = ( e |` ( 0 ..^ S ) ) -> ( d ` a ) = ( ( e |` ( 0 ..^ S ) ) ` a ) )
82 81 sumeq2sdv 
 |-  ( d = ( e |` ( 0 ..^ S ) ) -> sum_ a e. ( 0 ..^ S ) ( d ` a ) = sum_ a e. ( 0 ..^ S ) ( ( e |` ( 0 ..^ S ) ) ` a ) )
83 82 eqeq1d 
 |-  ( d = ( e |` ( 0 ..^ S ) ) -> ( sum_ a e. ( 0 ..^ S ) ( d ` a ) = ( M - ( e ` S ) ) <-> sum_ a e. ( 0 ..^ S ) ( ( e |` ( 0 ..^ S ) ) ` a ) = ( M - ( e ` S ) ) ) )
84 83 elrab 
 |-  ( ( e |` ( 0 ..^ S ) ) e. { d e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( d ` a ) = ( M - ( e ` S ) ) } <-> ( ( e |` ( 0 ..^ S ) ) e. ( A ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( ( e |` ( 0 ..^ S ) ) ` a ) = ( M - ( e ` S ) ) ) )
85 80 84 sylibr 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> ( e |` ( 0 ..^ S ) ) e. { d e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( d ` a ) = ( M - ( e ` S ) ) } )
86 1 ad2antrr 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> A C_ NN )
87 2 ad2antrr 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> M e. ZZ )
88 nnssz 
 |-  NN C_ ZZ
89 1 88 sstrdi 
 |-  ( ph -> A C_ ZZ )
90 89 ad2antrr 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> A C_ ZZ )
91 90 15 sseldd 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> ( e ` S ) e. ZZ )
92 87 91 zsubcld 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> ( M - ( e ` S ) ) e. ZZ )
93 86 92 12 reprval 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> ( A ( repr ` S ) ( M - ( e ` S ) ) ) = { d e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( d ` a ) = ( M - ( e ` S ) ) } )
94 85 93 eleqtrrd 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> ( e |` ( 0 ..^ S ) ) e. ( A ( repr ` S ) ( M - ( e ` S ) ) ) )
95 simpr 
 |-  ( ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) /\ c = ( e |` ( 0 ..^ S ) ) ) -> c = ( e |` ( 0 ..^ S ) ) )
96 95 uneq1d 
 |-  ( ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) /\ c = ( e |` ( 0 ..^ S ) ) ) -> ( c u. { <. S , ( e ` S ) >. } ) = ( ( e |` ( 0 ..^ S ) ) u. { <. S , ( e ` S ) >. } ) )
97 96 eqeq2d 
 |-  ( ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) /\ c = ( e |` ( 0 ..^ S ) ) ) -> ( e = ( c u. { <. S , ( e ` S ) >. } ) <-> e = ( ( e |` ( 0 ..^ S ) ) u. { <. S , ( e ` S ) >. } ) ) )
98 11 ffnd 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> e Fn ( 0 ..^ ( S + 1 ) ) )
99 fnsnsplit 
 |-  ( ( e Fn ( 0 ..^ ( S + 1 ) ) /\ S e. ( 0 ..^ ( S + 1 ) ) ) -> e = ( ( e |` ( ( 0 ..^ ( S + 1 ) ) \ { S } ) ) u. { <. S , ( e ` S ) >. } ) )
100 98 14 99 syl2anc 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> e = ( ( e |` ( ( 0 ..^ ( S + 1 ) ) \ { S } ) ) u. { <. S , ( e ` S ) >. } ) )
101 12 66 eleqtrdi 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> S e. ( ZZ>= ` 0 ) )
102 fzodif2 
 |-  ( S e. ( ZZ>= ` 0 ) -> ( ( 0 ..^ ( S + 1 ) ) \ { S } ) = ( 0 ..^ S ) )
103 101 102 syl 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> ( ( 0 ..^ ( S + 1 ) ) \ { S } ) = ( 0 ..^ S ) )
104 103 reseq2d 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> ( e |` ( ( 0 ..^ ( S + 1 ) ) \ { S } ) ) = ( e |` ( 0 ..^ S ) ) )
105 104 uneq1d 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> ( ( e |` ( ( 0 ..^ ( S + 1 ) ) \ { S } ) ) u. { <. S , ( e ` S ) >. } ) = ( ( e |` ( 0 ..^ S ) ) u. { <. S , ( e ` S ) >. } ) )
106 100 105 eqtrd 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> e = ( ( e |` ( 0 ..^ S ) ) u. { <. S , ( e ` S ) >. } ) )
107 94 97 106 rspcedvd 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> E. c e. ( A ( repr ` S ) ( M - ( e ` S ) ) ) e = ( c u. { <. S , ( e ` S ) >. } ) )
108 15 24 107 rspcedvd 
 |-  ( ( ( ph /\ e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) -> E. b e. A E. c e. ( A ( repr ` S ) ( M - b ) ) e = ( c u. { <. S , b >. } ) )
109 108 anasss 
 |-  ( ( ph /\ ( e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) ) -> E. b e. A E. c e. ( A ( repr ` S ) ( M - b ) ) e = ( c u. { <. S , b >. } ) )
110 simpr 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> e = ( c u. { <. S , b >. } ) )
111 1 adantr 
 |-  ( ( ph /\ b e. A ) -> A C_ NN )
112 111 adantr 
 |-  ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) -> A C_ NN )
113 2 adantr 
 |-  ( ( ph /\ b e. A ) -> M e. ZZ )
114 89 sselda 
 |-  ( ( ph /\ b e. A ) -> b e. ZZ )
115 113 114 zsubcld 
 |-  ( ( ph /\ b e. A ) -> ( M - b ) e. ZZ )
116 115 adantr 
 |-  ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) -> ( M - b ) e. ZZ )
117 3 adantr 
 |-  ( ( ph /\ b e. A ) -> S e. NN0 )
118 117 adantr 
 |-  ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) -> S e. NN0 )
119 simpr 
 |-  ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) -> c e. ( A ( repr ` S ) ( M - b ) ) )
120 112 116 118 119 reprf 
 |-  ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) -> c : ( 0 ..^ S ) --> A )
121 simplr 
 |-  ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) -> b e. A )
122 118 121 fsnd 
 |-  ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) -> { <. S , b >. } : { S } --> A )
123 fzodisjsn 
 |-  ( ( 0 ..^ S ) i^i { S } ) = (/)
124 123 a1i 
 |-  ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) -> ( ( 0 ..^ S ) i^i { S } ) = (/) )
125 120 122 124 fun2d 
 |-  ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) -> ( c u. { <. S , b >. } ) : ( ( 0 ..^ S ) u. { S } ) --> A )
126 118 67 syl 
 |-  ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) -> ( 0 ..^ ( S + 1 ) ) = ( ( 0 ..^ S ) u. { S } ) )
127 126 feq2d 
 |-  ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) -> ( ( c u. { <. S , b >. } ) : ( 0 ..^ ( S + 1 ) ) --> A <-> ( c u. { <. S , b >. } ) : ( ( 0 ..^ S ) u. { S } ) --> A ) )
128 125 127 mpbird 
 |-  ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) -> ( c u. { <. S , b >. } ) : ( 0 ..^ ( S + 1 ) ) --> A )
129 ovex 
 |-  ( 0 ..^ ( S + 1 ) ) e. _V
130 elmapg 
 |-  ( ( A e. _V /\ ( 0 ..^ ( S + 1 ) ) e. _V ) -> ( ( c u. { <. S , b >. } ) e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) <-> ( c u. { <. S , b >. } ) : ( 0 ..^ ( S + 1 ) ) --> A ) )
131 33 129 130 sylancl 
 |-  ( ph -> ( ( c u. { <. S , b >. } ) e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) <-> ( c u. { <. S , b >. } ) : ( 0 ..^ ( S + 1 ) ) --> A ) )
132 131 ad2antrr 
 |-  ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) -> ( ( c u. { <. S , b >. } ) e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) <-> ( c u. { <. S , b >. } ) : ( 0 ..^ ( S + 1 ) ) --> A ) )
133 128 132 mpbird 
 |-  ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) -> ( c u. { <. S , b >. } ) e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) )
134 133 adantr 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> ( c u. { <. S , b >. } ) e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) )
135 110 134 eqeltrd 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) )
136 126 adantr 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> ( 0 ..^ ( S + 1 ) ) = ( ( 0 ..^ S ) u. { S } ) )
137 136 sumeq1d 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = sum_ a e. ( ( 0 ..^ S ) u. { S } ) ( e ` a ) )
138 nfv 
 |-  F/ a ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) )
139 34 a1i 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> ( 0 ..^ S ) e. Fin )
140 118 adantr 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> S e. NN0 )
141 57 a1i 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> -. S e. ( 0 ..^ S ) )
142 43 ad4antr 
 |-  ( ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) /\ a e. ( 0 ..^ S ) ) -> A C_ CC )
143 128 adantr 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> ( c u. { <. S , b >. } ) : ( 0 ..^ ( S + 1 ) ) --> A )
144 110 feq1d 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> ( e : ( 0 ..^ ( S + 1 ) ) --> A <-> ( c u. { <. S , b >. } ) : ( 0 ..^ ( S + 1 ) ) --> A ) )
145 143 144 mpbird 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> e : ( 0 ..^ ( S + 1 ) ) --> A )
146 145 adantr 
 |-  ( ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) /\ a e. ( 0 ..^ S ) ) -> e : ( 0 ..^ ( S + 1 ) ) --> A )
147 simpr 
 |-  ( ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) /\ a e. ( 0 ..^ S ) ) -> a e. ( 0 ..^ S ) )
148 elun1 
 |-  ( a e. ( 0 ..^ S ) -> a e. ( ( 0 ..^ S ) u. { S } ) )
149 147 148 syl 
 |-  ( ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) /\ a e. ( 0 ..^ S ) ) -> a e. ( ( 0 ..^ S ) u. { S } ) )
150 126 ad2antrr 
 |-  ( ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) /\ a e. ( 0 ..^ S ) ) -> ( 0 ..^ ( S + 1 ) ) = ( ( 0 ..^ S ) u. { S } ) )
151 149 150 eleqtrrd 
 |-  ( ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) /\ a e. ( 0 ..^ S ) ) -> a e. ( 0 ..^ ( S + 1 ) ) )
152 146 151 ffvelrnd 
 |-  ( ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) /\ a e. ( 0 ..^ S ) ) -> ( e ` a ) e. A )
153 142 152 sseldd 
 |-  ( ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) /\ a e. ( 0 ..^ S ) ) -> ( e ` a ) e. CC )
154 43 ad3antrrr 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> A C_ CC )
155 140 13 syl 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> S e. ( 0 ..^ ( S + 1 ) ) )
156 145 155 ffvelrnd 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> ( e ` S ) e. A )
157 154 156 sseldd 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> ( e ` S ) e. CC )
158 138 56 139 140 141 153 63 157 fsumsplitsn 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> sum_ a e. ( ( 0 ..^ S ) u. { S } ) ( e ` a ) = ( sum_ a e. ( 0 ..^ S ) ( e ` a ) + ( e ` S ) ) )
159 simplr 
 |-  ( ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) /\ a e. ( 0 ..^ S ) ) -> e = ( c u. { <. S , b >. } ) )
160 159 fveq1d 
 |-  ( ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) /\ a e. ( 0 ..^ S ) ) -> ( e ` a ) = ( ( c u. { <. S , b >. } ) ` a ) )
161 120 ffnd 
 |-  ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) -> c Fn ( 0 ..^ S ) )
162 161 ad2antrr 
 |-  ( ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) /\ a e. ( 0 ..^ S ) ) -> c Fn ( 0 ..^ S ) )
163 122 ffnd 
 |-  ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) -> { <. S , b >. } Fn { S } )
164 163 ad2antrr 
 |-  ( ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) /\ a e. ( 0 ..^ S ) ) -> { <. S , b >. } Fn { S } )
165 123 a1i 
 |-  ( ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( 0 ..^ S ) i^i { S } ) = (/) )
166 fvun1 
 |-  ( ( c Fn ( 0 ..^ S ) /\ { <. S , b >. } Fn { S } /\ ( ( ( 0 ..^ S ) i^i { S } ) = (/) /\ a e. ( 0 ..^ S ) ) ) -> ( ( c u. { <. S , b >. } ) ` a ) = ( c ` a ) )
167 162 164 165 147 166 syl112anc 
 |-  ( ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( c u. { <. S , b >. } ) ` a ) = ( c ` a ) )
168 160 167 eqtrd 
 |-  ( ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) /\ a e. ( 0 ..^ S ) ) -> ( e ` a ) = ( c ` a ) )
169 168 ralrimiva 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> A. a e. ( 0 ..^ S ) ( e ` a ) = ( c ` a ) )
170 169 sumeq2d 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> sum_ a e. ( 0 ..^ S ) ( e ` a ) = sum_ a e. ( 0 ..^ S ) ( c ` a ) )
171 112 adantr 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> A C_ NN )
172 116 adantr 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> ( M - b ) e. ZZ )
173 119 adantr 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> c e. ( A ( repr ` S ) ( M - b ) ) )
174 171 172 140 173 reprsum 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> sum_ a e. ( 0 ..^ S ) ( c ` a ) = ( M - b ) )
175 170 174 eqtrd 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> sum_ a e. ( 0 ..^ S ) ( e ` a ) = ( M - b ) )
176 110 fveq1d 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> ( e ` S ) = ( ( c u. { <. S , b >. } ) ` S ) )
177 161 adantr 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> c Fn ( 0 ..^ S ) )
178 163 adantr 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> { <. S , b >. } Fn { S } )
179 123 a1i 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> ( ( 0 ..^ S ) i^i { S } ) = (/) )
180 snidg 
 |-  ( S e. NN0 -> S e. { S } )
181 140 180 syl 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> S e. { S } )
182 fvun2 
 |-  ( ( c Fn ( 0 ..^ S ) /\ { <. S , b >. } Fn { S } /\ ( ( ( 0 ..^ S ) i^i { S } ) = (/) /\ S e. { S } ) ) -> ( ( c u. { <. S , b >. } ) ` S ) = ( { <. S , b >. } ` S ) )
183 177 178 179 181 182 syl112anc 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> ( ( c u. { <. S , b >. } ) ` S ) = ( { <. S , b >. } ` S ) )
184 121 adantr 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> b e. A )
185 fvsng 
 |-  ( ( S e. NN0 /\ b e. A ) -> ( { <. S , b >. } ` S ) = b )
186 140 184 185 syl2anc 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> ( { <. S , b >. } ` S ) = b )
187 176 183 186 3eqtrd 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> ( e ` S ) = b )
188 175 187 oveq12d 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> ( sum_ a e. ( 0 ..^ S ) ( e ` a ) + ( e ` S ) ) = ( ( M - b ) + b ) )
189 zsscn 
 |-  ZZ C_ CC
190 113 ad2antrr 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> M e. ZZ )
191 189 190 sseldi 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> M e. CC )
192 187 157 eqeltrrd 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> b e. CC )
193 191 192 npcand 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> ( ( M - b ) + b ) = M )
194 188 193 eqtrd 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> ( sum_ a e. ( 0 ..^ S ) ( e ` a ) + ( e ` S ) ) = M )
195 137 158 194 3eqtrd 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M )
196 135 195 jca 
 |-  ( ( ( ( ph /\ b e. A ) /\ c e. ( A ( repr ` S ) ( M - b ) ) ) /\ e = ( c u. { <. S , b >. } ) ) -> ( e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) )
197 196 r19.29ffa 
 |-  ( ( ph /\ E. b e. A E. c e. ( A ( repr ` S ) ( M - b ) ) e = ( c u. { <. S , b >. } ) ) -> ( e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) )
198 109 197 impbida 
 |-  ( ph -> ( ( e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) <-> E. b e. A E. c e. ( A ( repr ` S ) ( M - b ) ) e = ( c u. { <. S , b >. } ) ) )
199 vex 
 |-  c e. _V
200 snex 
 |-  { <. S , b >. } e. _V
201 199 200 unex 
 |-  ( c u. { <. S , b >. } ) e. _V
202 4 201 elrnmpti 
 |-  ( e e. ran F <-> E. c e. ( A ( repr ` S ) ( M - b ) ) e = ( c u. { <. S , b >. } ) )
203 202 rexbii 
 |-  ( E. b e. A e e. ran F <-> E. b e. A E. c e. ( A ( repr ` S ) ( M - b ) ) e = ( c u. { <. S , b >. } ) )
204 198 203 bitr4di 
 |-  ( ph -> ( ( e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) <-> E. b e. A e e. ran F ) )
205 fveq1 
 |-  ( c = e -> ( c ` a ) = ( e ` a ) )
206 205 sumeq2sdv 
 |-  ( c = e -> sum_ a e. ( 0 ..^ ( S + 1 ) ) ( c ` a ) = sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) )
207 206 eqeq1d 
 |-  ( c = e -> ( sum_ a e. ( 0 ..^ ( S + 1 ) ) ( c ` a ) = M <-> sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) )
208 207 cbvrabv 
 |-  { c e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) | sum_ a e. ( 0 ..^ ( S + 1 ) ) ( c ` a ) = M } = { e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) | sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M }
209 208 rabeq2i 
 |-  ( e e. { c e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) | sum_ a e. ( 0 ..^ ( S + 1 ) ) ( c ` a ) = M } <-> ( e e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) /\ sum_ a e. ( 0 ..^ ( S + 1 ) ) ( e ` a ) = M ) )
210 eliun 
 |-  ( e e. U_ b e. A ran F <-> E. b e. A e e. ran F )
211 204 209 210 3bitr4g 
 |-  ( ph -> ( e e. { c e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) | sum_ a e. ( 0 ..^ ( S + 1 ) ) ( c ` a ) = M } <-> e e. U_ b e. A ran F ) )
212 211 eqrdv 
 |-  ( ph -> { c e. ( A ^m ( 0 ..^ ( S + 1 ) ) ) | sum_ a e. ( 0 ..^ ( S + 1 ) ) ( c ` a ) = M } = U_ b e. A ran F )
213 8 212 eqtrd 
 |-  ( ph -> ( A ( repr ` ( S + 1 ) ) M ) = U_ b e. A ran F )