Metamath Proof Explorer

Theorem reprpmtf1o

Description: Transposing 0 and X maps representations with a condition on the first index to transpositions with the same condition on the index X . (Contributed by Thierry Arnoux, 27-Dec-2021)

Ref Expression
Hypotheses reprpmtf1o.s 
|- ( ph -> S e. NN )
reprpmtf1o.m 
|- ( ph -> M e. ZZ )
reprpmtf1o.a 
|- ( ph -> A C_ NN )
reprpmtf1o.x 
|- ( ph -> X e. ( 0 ..^ S ) )
reprpmtf1o.o 
|- O = { c e. ( A ( repr ` S ) M ) | -. ( c ` 0 ) e. B }
reprpmtf1o.p 
|- P = { c e. ( A ( repr ` S ) M ) | -. ( c ` X ) e. B }
reprpmtf1o.t 
|- T = if ( X = 0 , ( _I |` ( 0 ..^ S ) ) , ( ( pmTrsp ` ( 0 ..^ S ) ) ` { X , 0 } ) )
reprpmtf1o.f 
|- F = ( c e. P |-> ( c o. T ) )
Assertion reprpmtf1o 
|- ( ph -> F : P -1-1-onto-> O )

Proof

Step Hyp Ref Expression
1 reprpmtf1o.s 
 |-  ( ph -> S e. NN )
2 reprpmtf1o.m 
 |-  ( ph -> M e. ZZ )
3 reprpmtf1o.a 
 |-  ( ph -> A C_ NN )
4 reprpmtf1o.x 
 |-  ( ph -> X e. ( 0 ..^ S ) )
5 reprpmtf1o.o 
 |-  O = { c e. ( A ( repr ` S ) M ) | -. ( c ` 0 ) e. B }
6 reprpmtf1o.p 
 |-  P = { c e. ( A ( repr ` S ) M ) | -. ( c ` X ) e. B }
7 reprpmtf1o.t 
 |-  T = if ( X = 0 , ( _I |` ( 0 ..^ S ) ) , ( ( pmTrsp ` ( 0 ..^ S ) ) ` { X , 0 } ) )
8 reprpmtf1o.f 
 |-  F = ( c e. P |-> ( c o. T ) )
9 eqid 
 |-  ( A ^m ( 0 ..^ S ) ) = ( A ^m ( 0 ..^ S ) )
10 eqid 
 |-  ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) = ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) )
11 ovexd 
 |-  ( ph -> ( 0 ..^ S ) e. _V )
12 nnex 
 |-  NN e. _V
13 12 a1i 
 |-  ( ph -> NN e. _V )
14 13 3 ssexd 
 |-  ( ph -> A e. _V )
15 lbfzo0 
 |-  ( 0 e. ( 0 ..^ S ) <-> S e. NN )
16 1 15 sylibr 
 |-  ( ph -> 0 e. ( 0 ..^ S ) )
17 11 4 16 7 pmtridf1o 
 |-  ( ph -> T : ( 0 ..^ S ) -1-1-onto-> ( 0 ..^ S ) )
18 9 9 10 11 11 14 17 fmptco1f1o 
 |-  ( ph -> ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) : ( A ^m ( 0 ..^ S ) ) -1-1-onto-> ( A ^m ( 0 ..^ S ) ) )
19 f1of1 
 |-  ( ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) : ( A ^m ( 0 ..^ S ) ) -1-1-onto-> ( A ^m ( 0 ..^ S ) ) -> ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) : ( A ^m ( 0 ..^ S ) ) -1-1-> ( A ^m ( 0 ..^ S ) ) )
20 18 19 syl 
 |-  ( ph -> ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) : ( A ^m ( 0 ..^ S ) ) -1-1-> ( A ^m ( 0 ..^ S ) ) )
21 ssrab2 
 |-  { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } C_ ( A ^m ( 0 ..^ S ) )
22 6 ssrab3 
 |-  P C_ ( A ( repr ` S ) M )
23 22 a1i 
 |-  ( ph -> P C_ ( A ( repr ` S ) M ) )
24 1 nnnn0d 
 |-  ( ph -> S e. NN0 )
25 3 2 24 reprval 
 |-  ( ph -> ( A ( repr ` S ) M ) = { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } )
26 23 25 sseqtrd 
 |-  ( ph -> P C_ { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } )
27 26 sselda 
 |-  ( ( ph /\ c e. P ) -> c e. { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } )
28 21 27 sseldi 
 |-  ( ( ph /\ c e. P ) -> c e. ( A ^m ( 0 ..^ S ) ) )
29 28 ex 
 |-  ( ph -> ( c e. P -> c e. ( A ^m ( 0 ..^ S ) ) ) )
30 29 ssrdv 
 |-  ( ph -> P C_ ( A ^m ( 0 ..^ S ) ) )
31 f1ores 
 |-  ( ( ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) : ( A ^m ( 0 ..^ S ) ) -1-1-> ( A ^m ( 0 ..^ S ) ) /\ P C_ ( A ^m ( 0 ..^ S ) ) ) -> ( ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) |` P ) : P -1-1-onto-> ( ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) " P ) )
32 20 30 31 syl2anc 
 |-  ( ph -> ( ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) |` P ) : P -1-1-onto-> ( ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) " P ) )
33 resmpt 
 |-  ( P C_ ( A ^m ( 0 ..^ S ) ) -> ( ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) |` P ) = ( c e. P |-> ( c o. T ) ) )
34 30 33 syl 
 |-  ( ph -> ( ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) |` P ) = ( c e. P |-> ( c o. T ) ) )
35 34 8 eqtr4di 
 |-  ( ph -> ( ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) |` P ) = F )
36 eqidd 
 |-  ( ph -> P = P )
37 vex 
 |-  d e. _V
38 37 a1i 
 |-  ( ph -> d e. _V )
39 10 38 30 elimampt 
 |-  ( ph -> ( d e. ( ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) " P ) <-> E. c e. P d = ( c o. T ) ) )
40 simpr 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> d = ( c o. T ) )
41 f1of 
 |-  ( ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) : ( A ^m ( 0 ..^ S ) ) -1-1-onto-> ( A ^m ( 0 ..^ S ) ) -> ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) : ( A ^m ( 0 ..^ S ) ) --> ( A ^m ( 0 ..^ S ) ) )
42 18 41 syl 
 |-  ( ph -> ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) : ( A ^m ( 0 ..^ S ) ) --> ( A ^m ( 0 ..^ S ) ) )
43 42 ad2antrr 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) : ( A ^m ( 0 ..^ S ) ) --> ( A ^m ( 0 ..^ S ) ) )
44 10 fmpt 
 |-  ( A. c e. ( A ^m ( 0 ..^ S ) ) ( c o. T ) e. ( A ^m ( 0 ..^ S ) ) <-> ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) : ( A ^m ( 0 ..^ S ) ) --> ( A ^m ( 0 ..^ S ) ) )
45 43 44 sylibr 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> A. c e. ( A ^m ( 0 ..^ S ) ) ( c o. T ) e. ( A ^m ( 0 ..^ S ) ) )
46 28 adantr 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> c e. ( A ^m ( 0 ..^ S ) ) )
47 rspa 
 |-  ( ( A. c e. ( A ^m ( 0 ..^ S ) ) ( c o. T ) e. ( A ^m ( 0 ..^ S ) ) /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> ( c o. T ) e. ( A ^m ( 0 ..^ S ) ) )
48 45 46 47 syl2anc 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> ( c o. T ) e. ( A ^m ( 0 ..^ S ) ) )
49 40 48 eqeltrd 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> d e. ( A ^m ( 0 ..^ S ) ) )
50 40 adantr 
 |-  ( ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) /\ a e. ( 0 ..^ S ) ) -> d = ( c o. T ) )
51 50 fveq1d 
 |-  ( ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) /\ a e. ( 0 ..^ S ) ) -> ( d ` a ) = ( ( c o. T ) ` a ) )
52 f1ofun 
 |-  ( T : ( 0 ..^ S ) -1-1-onto-> ( 0 ..^ S ) -> Fun T )
53 17 52 syl 
 |-  ( ph -> Fun T )
54 53 ad2antrr 
 |-  ( ( ( ph /\ c e. P ) /\ a e. ( 0 ..^ S ) ) -> Fun T )
55 simpr 
 |-  ( ( ( ph /\ c e. P ) /\ a e. ( 0 ..^ S ) ) -> a e. ( 0 ..^ S ) )
56 f1odm 
 |-  ( T : ( 0 ..^ S ) -1-1-onto-> ( 0 ..^ S ) -> dom T = ( 0 ..^ S ) )
57 17 56 syl 
 |-  ( ph -> dom T = ( 0 ..^ S ) )
58 57 ad2antrr 
 |-  ( ( ( ph /\ c e. P ) /\ a e. ( 0 ..^ S ) ) -> dom T = ( 0 ..^ S ) )
59 55 58 eleqtrrd 
 |-  ( ( ( ph /\ c e. P ) /\ a e. ( 0 ..^ S ) ) -> a e. dom T )
60 fvco 
 |-  ( ( Fun T /\ a e. dom T ) -> ( ( c o. T ) ` a ) = ( c ` ( T ` a ) ) )
61 54 59 60 syl2anc 
 |-  ( ( ( ph /\ c e. P ) /\ a e. ( 0 ..^ S ) ) -> ( ( c o. T ) ` a ) = ( c ` ( T ` a ) ) )
62 61 adantlr 
 |-  ( ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( c o. T ) ` a ) = ( c ` ( T ` a ) ) )
63 51 62 eqtrd 
 |-  ( ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) /\ a e. ( 0 ..^ S ) ) -> ( d ` a ) = ( c ` ( T ` a ) ) )
64 63 sumeq2dv 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> sum_ a e. ( 0 ..^ S ) ( d ` a ) = sum_ a e. ( 0 ..^ S ) ( c ` ( T ` a ) ) )
65 fveq2 
 |-  ( b = ( T ` a ) -> ( c ` b ) = ( c ` ( T ` a ) ) )
66 fzofi 
 |-  ( 0 ..^ S ) e. Fin
67 66 a1i 
 |-  ( ( ph /\ c e. P ) -> ( 0 ..^ S ) e. Fin )
68 17 adantr 
 |-  ( ( ph /\ c e. P ) -> T : ( 0 ..^ S ) -1-1-onto-> ( 0 ..^ S ) )
69 eqidd 
 |-  ( ( ( ph /\ c e. P ) /\ a e. ( 0 ..^ S ) ) -> ( T ` a ) = ( T ` a ) )
70 3 ad2antrr 
 |-  ( ( ( ph /\ c e. P ) /\ b e. ( 0 ..^ S ) ) -> A C_ NN )
71 3 adantr 
 |-  ( ( ph /\ c e. P ) -> A C_ NN )
72 2 adantr 
 |-  ( ( ph /\ c e. P ) -> M e. ZZ )
73 24 adantr 
 |-  ( ( ph /\ c e. P ) -> S e. NN0 )
74 23 sselda 
 |-  ( ( ph /\ c e. P ) -> c e. ( A ( repr ` S ) M ) )
75 71 72 73 74 reprf 
 |-  ( ( ph /\ c e. P ) -> c : ( 0 ..^ S ) --> A )
76 75 ffvelrnda 
 |-  ( ( ( ph /\ c e. P ) /\ b e. ( 0 ..^ S ) ) -> ( c ` b ) e. A )
77 70 76 sseldd 
 |-  ( ( ( ph /\ c e. P ) /\ b e. ( 0 ..^ S ) ) -> ( c ` b ) e. NN )
78 77 nncnd 
 |-  ( ( ( ph /\ c e. P ) /\ b e. ( 0 ..^ S ) ) -> ( c ` b ) e. CC )
79 65 67 68 69 78 fsumf1o 
 |-  ( ( ph /\ c e. P ) -> sum_ b e. ( 0 ..^ S ) ( c ` b ) = sum_ a e. ( 0 ..^ S ) ( c ` ( T ` a ) ) )
80 79 adantr 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> sum_ b e. ( 0 ..^ S ) ( c ` b ) = sum_ a e. ( 0 ..^ S ) ( c ` ( T ` a ) ) )
81 71 72 73 74 reprsum 
 |-  ( ( ph /\ c e. P ) -> sum_ b e. ( 0 ..^ S ) ( c ` b ) = M )
82 81 adantr 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> sum_ b e. ( 0 ..^ S ) ( c ` b ) = M )
83 64 80 82 3eqtr2d 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> sum_ a e. ( 0 ..^ S ) ( d ` a ) = M )
84 fveq1 
 |-  ( c = d -> ( c ` a ) = ( d ` a ) )
85 84 sumeq2sdv 
 |-  ( c = d -> sum_ a e. ( 0 ..^ S ) ( c ` a ) = sum_ a e. ( 0 ..^ S ) ( d ` a ) )
86 85 eqeq1d 
 |-  ( c = d -> ( sum_ a e. ( 0 ..^ S ) ( c ` a ) = M <-> sum_ a e. ( 0 ..^ S ) ( d ` a ) = M ) )
87 86 elrab 
 |-  ( d e. { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } <-> ( d e. ( A ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( d ` a ) = M ) )
88 49 83 87 sylanbrc 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> d e. { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } )
89 25 ad2antrr 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> ( A ( repr ` S ) M ) = { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } )
90 88 89 eleqtrrd 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> d e. ( A ( repr ` S ) M ) )
91 40 fveq1d 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> ( d ` 0 ) = ( ( c o. T ) ` 0 ) )
92 53 ad2antrr 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> Fun T )
93 16 57 eleqtrrd 
 |-  ( ph -> 0 e. dom T )
94 93 ad2antrr 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> 0 e. dom T )
95 fvco 
 |-  ( ( Fun T /\ 0 e. dom T ) -> ( ( c o. T ) ` 0 ) = ( c ` ( T ` 0 ) ) )
96 92 94 95 syl2anc 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> ( ( c o. T ) ` 0 ) = ( c ` ( T ` 0 ) ) )
97 11 4 16 7 pmtridfv2 
 |-  ( ph -> ( T ` 0 ) = X )
98 97 ad2antrr 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> ( T ` 0 ) = X )
99 98 fveq2d 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> ( c ` ( T ` 0 ) ) = ( c ` X ) )
100 simpr 
 |-  ( ( ph /\ c e. P ) -> c e. P )
101 100 6 eleqtrdi 
 |-  ( ( ph /\ c e. P ) -> c e. { c e. ( A ( repr ` S ) M ) | -. ( c ` X ) e. B } )
102 rabid 
 |-  ( c e. { c e. ( A ( repr ` S ) M ) | -. ( c ` X ) e. B } <-> ( c e. ( A ( repr ` S ) M ) /\ -. ( c ` X ) e. B ) )
103 101 102 sylib 
 |-  ( ( ph /\ c e. P ) -> ( c e. ( A ( repr ` S ) M ) /\ -. ( c ` X ) e. B ) )
104 103 simprd 
 |-  ( ( ph /\ c e. P ) -> -. ( c ` X ) e. B )
105 104 adantr 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> -. ( c ` X ) e. B )
106 99 105 eqneltrd 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> -. ( c ` ( T ` 0 ) ) e. B )
107 96 106 eqneltrd 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> -. ( ( c o. T ) ` 0 ) e. B )
108 91 107 eqneltrd 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> -. ( d ` 0 ) e. B )
109 90 108 jca 
 |-  ( ( ( ph /\ c e. P ) /\ d = ( c o. T ) ) -> ( d e. ( A ( repr ` S ) M ) /\ -. ( d ` 0 ) e. B ) )
110 109 r19.29an 
 |-  ( ( ph /\ E. c e. P d = ( c o. T ) ) -> ( d e. ( A ( repr ` S ) M ) /\ -. ( d ` 0 ) e. B ) )
111 3 adantr 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> A C_ NN )
112 2 adantr 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> M e. ZZ )
113 24 adantr 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> S e. NN0 )
114 simpr 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> d e. ( A ( repr ` S ) M ) )
115 111 112 113 114 reprf 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> d : ( 0 ..^ S ) --> A )
116 f1ocnv 
 |-  ( T : ( 0 ..^ S ) -1-1-onto-> ( 0 ..^ S ) -> `' T : ( 0 ..^ S ) -1-1-onto-> ( 0 ..^ S ) )
117 f1of 
 |-  ( `' T : ( 0 ..^ S ) -1-1-onto-> ( 0 ..^ S ) -> `' T : ( 0 ..^ S ) --> ( 0 ..^ S ) )
118 17 116 117 3syl 
 |-  ( ph -> `' T : ( 0 ..^ S ) --> ( 0 ..^ S ) )
119 118 adantr 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> `' T : ( 0 ..^ S ) --> ( 0 ..^ S ) )
120 fco 
 |-  ( ( d : ( 0 ..^ S ) --> A /\ `' T : ( 0 ..^ S ) --> ( 0 ..^ S ) ) -> ( d o. `' T ) : ( 0 ..^ S ) --> A )
121 115 119 120 syl2anc 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> ( d o. `' T ) : ( 0 ..^ S ) --> A )
122 elmapg 
 |-  ( ( A e. _V /\ ( 0 ..^ S ) e. _V ) -> ( ( d o. `' T ) e. ( A ^m ( 0 ..^ S ) ) <-> ( d o. `' T ) : ( 0 ..^ S ) --> A ) )
123 14 11 122 syl2anc 
 |-  ( ph -> ( ( d o. `' T ) e. ( A ^m ( 0 ..^ S ) ) <-> ( d o. `' T ) : ( 0 ..^ S ) --> A ) )
124 123 adantr 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> ( ( d o. `' T ) e. ( A ^m ( 0 ..^ S ) ) <-> ( d o. `' T ) : ( 0 ..^ S ) --> A ) )
125 121 124 mpbird 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> ( d o. `' T ) e. ( A ^m ( 0 ..^ S ) ) )
126 125 adantr 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ -. ( d ` 0 ) e. B ) -> ( d o. `' T ) e. ( A ^m ( 0 ..^ S ) ) )
127 f1ofun 
 |-  ( `' T : ( 0 ..^ S ) -1-1-onto-> ( 0 ..^ S ) -> Fun `' T )
128 17 116 127 3syl 
 |-  ( ph -> Fun `' T )
129 128 ad2antrr 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ a e. ( 0 ..^ S ) ) -> Fun `' T )
130 simpr 
 |-  ( ( ph /\ a e. ( 0 ..^ S ) ) -> a e. ( 0 ..^ S ) )
131 f1odm 
 |-  ( `' T : ( 0 ..^ S ) -1-1-onto-> ( 0 ..^ S ) -> dom `' T = ( 0 ..^ S ) )
132 17 116 131 3syl 
 |-  ( ph -> dom `' T = ( 0 ..^ S ) )
133 132 adantr 
 |-  ( ( ph /\ a e. ( 0 ..^ S ) ) -> dom `' T = ( 0 ..^ S ) )
134 130 133 eleqtrrd 
 |-  ( ( ph /\ a e. ( 0 ..^ S ) ) -> a e. dom `' T )
135 134 adantlr 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ a e. ( 0 ..^ S ) ) -> a e. dom `' T )
136 fvco 
 |-  ( ( Fun `' T /\ a e. dom `' T ) -> ( ( d o. `' T ) ` a ) = ( d ` ( `' T ` a ) ) )
137 129 135 136 syl2anc 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( d o. `' T ) ` a ) = ( d ` ( `' T ` a ) ) )
138 137 sumeq2dv 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> sum_ a e. ( 0 ..^ S ) ( ( d o. `' T ) ` a ) = sum_ a e. ( 0 ..^ S ) ( d ` ( `' T ` a ) ) )
139 fveq2 
 |-  ( b = ( `' T ` a ) -> ( d ` b ) = ( d ` ( `' T ` a ) ) )
140 66 a1i 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> ( 0 ..^ S ) e. Fin )
141 17 116 syl 
 |-  ( ph -> `' T : ( 0 ..^ S ) -1-1-onto-> ( 0 ..^ S ) )
142 141 adantr 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> `' T : ( 0 ..^ S ) -1-1-onto-> ( 0 ..^ S ) )
143 eqidd 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ a e. ( 0 ..^ S ) ) -> ( `' T ` a ) = ( `' T ` a ) )
144 111 adantr 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ b e. ( 0 ..^ S ) ) -> A C_ NN )
145 115 ffvelrnda 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ b e. ( 0 ..^ S ) ) -> ( d ` b ) e. A )
146 144 145 sseldd 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ b e. ( 0 ..^ S ) ) -> ( d ` b ) e. NN )
147 146 nncnd 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ b e. ( 0 ..^ S ) ) -> ( d ` b ) e. CC )
148 139 140 142 143 147 fsumf1o 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> sum_ b e. ( 0 ..^ S ) ( d ` b ) = sum_ a e. ( 0 ..^ S ) ( d ` ( `' T ` a ) ) )
149 111 112 113 114 reprsum 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> sum_ b e. ( 0 ..^ S ) ( d ` b ) = M )
150 138 148 149 3eqtr2d 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> sum_ a e. ( 0 ..^ S ) ( ( d o. `' T ) ` a ) = M )
151 150 adantr 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ -. ( d ` 0 ) e. B ) -> sum_ a e. ( 0 ..^ S ) ( ( d o. `' T ) ` a ) = M )
152 fveq1 
 |-  ( c = ( d o. `' T ) -> ( c ` a ) = ( ( d o. `' T ) ` a ) )
153 152 sumeq2sdv 
 |-  ( c = ( d o. `' T ) -> sum_ a e. ( 0 ..^ S ) ( c ` a ) = sum_ a e. ( 0 ..^ S ) ( ( d o. `' T ) ` a ) )
154 153 eqeq1d 
 |-  ( c = ( d o. `' T ) -> ( sum_ a e. ( 0 ..^ S ) ( c ` a ) = M <-> sum_ a e. ( 0 ..^ S ) ( ( d o. `' T ) ` a ) = M ) )
155 154 elrab 
 |-  ( ( d o. `' T ) e. { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } <-> ( ( d o. `' T ) e. ( A ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( ( d o. `' T ) ` a ) = M ) )
156 126 151 155 sylanbrc 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ -. ( d ` 0 ) e. B ) -> ( d o. `' T ) e. { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } )
157 25 ad2antrr 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ -. ( d ` 0 ) e. B ) -> ( A ( repr ` S ) M ) = { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } )
158 156 157 eleqtrrd 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ -. ( d ` 0 ) e. B ) -> ( d o. `' T ) e. ( A ( repr ` S ) M ) )
159 128 ad2antrr 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ -. ( d ` 0 ) e. B ) -> Fun `' T )
160 4 132 eleqtrrd 
 |-  ( ph -> X e. dom `' T )
161 160 ad2antrr 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ -. ( d ` 0 ) e. B ) -> X e. dom `' T )
162 fvco 
 |-  ( ( Fun `' T /\ X e. dom `' T ) -> ( ( d o. `' T ) ` X ) = ( d ` ( `' T ` X ) ) )
163 159 161 162 syl2anc 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ -. ( d ` 0 ) e. B ) -> ( ( d o. `' T ) ` X ) = ( d ` ( `' T ` X ) ) )
164 f1ocnvfv 
 |-  ( ( T : ( 0 ..^ S ) -1-1-onto-> ( 0 ..^ S ) /\ 0 e. ( 0 ..^ S ) ) -> ( ( T ` 0 ) = X -> ( `' T ` X ) = 0 ) )
165 164 imp 
 |-  ( ( ( T : ( 0 ..^ S ) -1-1-onto-> ( 0 ..^ S ) /\ 0 e. ( 0 ..^ S ) ) /\ ( T ` 0 ) = X ) -> ( `' T ` X ) = 0 )
166 17 16 97 165 syl21anc 
 |-  ( ph -> ( `' T ` X ) = 0 )
167 166 ad2antrr 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ -. ( d ` 0 ) e. B ) -> ( `' T ` X ) = 0 )
168 167 fveq2d 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ -. ( d ` 0 ) e. B ) -> ( d ` ( `' T ` X ) ) = ( d ` 0 ) )
169 simpr 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ -. ( d ` 0 ) e. B ) -> -. ( d ` 0 ) e. B )
170 168 169 eqneltrd 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ -. ( d ` 0 ) e. B ) -> -. ( d ` ( `' T ` X ) ) e. B )
171 163 170 eqneltrd 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ -. ( d ` 0 ) e. B ) -> -. ( ( d o. `' T ) ` X ) e. B )
172 fveq1 
 |-  ( c = ( d o. `' T ) -> ( c ` X ) = ( ( d o. `' T ) ` X ) )
173 172 eleq1d 
 |-  ( c = ( d o. `' T ) -> ( ( c ` X ) e. B <-> ( ( d o. `' T ) ` X ) e. B ) )
174 173 notbid 
 |-  ( c = ( d o. `' T ) -> ( -. ( c ` X ) e. B <-> -. ( ( d o. `' T ) ` X ) e. B ) )
175 174 elrab 
 |-  ( ( d o. `' T ) e. { c e. ( A ( repr ` S ) M ) | -. ( c ` X ) e. B } <-> ( ( d o. `' T ) e. ( A ( repr ` S ) M ) /\ -. ( ( d o. `' T ) ` X ) e. B ) )
176 158 171 175 sylanbrc 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ -. ( d ` 0 ) e. B ) -> ( d o. `' T ) e. { c e. ( A ( repr ` S ) M ) | -. ( c ` X ) e. B } )
177 176 6 eleqtrrdi 
 |-  ( ( ( ph /\ d e. ( A ( repr ` S ) M ) ) /\ -. ( d ` 0 ) e. B ) -> ( d o. `' T ) e. P )
178 177 anasss 
 |-  ( ( ph /\ ( d e. ( A ( repr ` S ) M ) /\ -. ( d ` 0 ) e. B ) ) -> ( d o. `' T ) e. P )
179 simpr 
 |-  ( ( ( ph /\ ( d e. ( A ( repr ` S ) M ) /\ -. ( d ` 0 ) e. B ) ) /\ c = ( d o. `' T ) ) -> c = ( d o. `' T ) )
180 179 coeq1d 
 |-  ( ( ( ph /\ ( d e. ( A ( repr ` S ) M ) /\ -. ( d ` 0 ) e. B ) ) /\ c = ( d o. `' T ) ) -> ( c o. T ) = ( ( d o. `' T ) o. T ) )
181 180 eqeq2d 
 |-  ( ( ( ph /\ ( d e. ( A ( repr ` S ) M ) /\ -. ( d ` 0 ) e. B ) ) /\ c = ( d o. `' T ) ) -> ( d = ( c o. T ) <-> d = ( ( d o. `' T ) o. T ) ) )
182 f1ococnv1 
 |-  ( T : ( 0 ..^ S ) -1-1-onto-> ( 0 ..^ S ) -> ( `' T o. T ) = ( _I |` ( 0 ..^ S ) ) )
183 17 182 syl 
 |-  ( ph -> ( `' T o. T ) = ( _I |` ( 0 ..^ S ) ) )
184 183 adantr 
 |-  ( ( ph /\ ( d e. ( A ( repr ` S ) M ) /\ -. ( d ` 0 ) e. B ) ) -> ( `' T o. T ) = ( _I |` ( 0 ..^ S ) ) )
185 184 coeq2d 
 |-  ( ( ph /\ ( d e. ( A ( repr ` S ) M ) /\ -. ( d ` 0 ) e. B ) ) -> ( d o. ( `' T o. T ) ) = ( d o. ( _I |` ( 0 ..^ S ) ) ) )
186 115 adantrr 
 |-  ( ( ph /\ ( d e. ( A ( repr ` S ) M ) /\ -. ( d ` 0 ) e. B ) ) -> d : ( 0 ..^ S ) --> A )
187 fcoi1 
 |-  ( d : ( 0 ..^ S ) --> A -> ( d o. ( _I |` ( 0 ..^ S ) ) ) = d )
188 186 187 syl 
 |-  ( ( ph /\ ( d e. ( A ( repr ` S ) M ) /\ -. ( d ` 0 ) e. B ) ) -> ( d o. ( _I |` ( 0 ..^ S ) ) ) = d )
189 185 188 eqtr2d 
 |-  ( ( ph /\ ( d e. ( A ( repr ` S ) M ) /\ -. ( d ` 0 ) e. B ) ) -> d = ( d o. ( `' T o. T ) ) )
190 coass 
 |-  ( ( d o. `' T ) o. T ) = ( d o. ( `' T o. T ) )
191 189 190 eqtr4di 
 |-  ( ( ph /\ ( d e. ( A ( repr ` S ) M ) /\ -. ( d ` 0 ) e. B ) ) -> d = ( ( d o. `' T ) o. T ) )
192 178 181 191 rspcedvd 
 |-  ( ( ph /\ ( d e. ( A ( repr ` S ) M ) /\ -. ( d ` 0 ) e. B ) ) -> E. c e. P d = ( c o. T ) )
193 110 192 impbida 
 |-  ( ph -> ( E. c e. P d = ( c o. T ) <-> ( d e. ( A ( repr ` S ) M ) /\ -. ( d ` 0 ) e. B ) ) )
194 39 193 bitrd 
 |-  ( ph -> ( d e. ( ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) " P ) <-> ( d e. ( A ( repr ` S ) M ) /\ -. ( d ` 0 ) e. B ) ) )
195 fveq1 
 |-  ( c = d -> ( c ` 0 ) = ( d ` 0 ) )
196 195 eleq1d 
 |-  ( c = d -> ( ( c ` 0 ) e. B <-> ( d ` 0 ) e. B ) )
197 196 notbid 
 |-  ( c = d -> ( -. ( c ` 0 ) e. B <-> -. ( d ` 0 ) e. B ) )
198 197 elrab 
 |-  ( d e. { c e. ( A ( repr ` S ) M ) | -. ( c ` 0 ) e. B } <-> ( d e. ( A ( repr ` S ) M ) /\ -. ( d ` 0 ) e. B ) )
199 194 198 bitr4di 
 |-  ( ph -> ( d e. ( ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) " P ) <-> d e. { c e. ( A ( repr ` S ) M ) | -. ( c ` 0 ) e. B } ) )
200 199 eqrdv 
 |-  ( ph -> ( ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) " P ) = { c e. ( A ( repr ` S ) M ) | -. ( c ` 0 ) e. B } )
201 200 5 eqtr4di 
 |-  ( ph -> ( ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) " P ) = O )
202 35 36 201 f1oeq123d 
 |-  ( ph -> ( ( ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) |` P ) : P -1-1-onto-> ( ( c e. ( A ^m ( 0 ..^ S ) ) |-> ( c o. T ) ) " P ) <-> F : P -1-1-onto-> O ) )
203 32 202 mpbid 
 |-  ( ph -> F : P -1-1-onto-> O )