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 |
|
fin |
|- ( c : ( 0 ..^ S ) --> ( A i^i B ) <-> ( c : ( 0 ..^ S ) --> A /\ c : ( 0 ..^ S ) --> B ) ) |
5 |
|
df-f |
|- ( c : ( 0 ..^ S ) --> B <-> ( c Fn ( 0 ..^ S ) /\ ran c C_ B ) ) |
6 |
|
ffn |
|- ( c : ( 0 ..^ S ) --> A -> c Fn ( 0 ..^ S ) ) |
7 |
6
|
adantl |
|- ( ( ph /\ c : ( 0 ..^ S ) --> A ) -> c Fn ( 0 ..^ S ) ) |
8 |
7
|
biantrurd |
|- ( ( ph /\ c : ( 0 ..^ S ) --> A ) -> ( ran c C_ B <-> ( c Fn ( 0 ..^ S ) /\ ran c C_ B ) ) ) |
9 |
8
|
bicomd |
|- ( ( ph /\ c : ( 0 ..^ S ) --> A ) -> ( ( c Fn ( 0 ..^ S ) /\ ran c C_ B ) <-> ran c C_ B ) ) |
10 |
5 9
|
syl5bb |
|- ( ( ph /\ c : ( 0 ..^ S ) --> A ) -> ( c : ( 0 ..^ S ) --> B <-> ran c C_ B ) ) |
11 |
10
|
pm5.32da |
|- ( ph -> ( ( c : ( 0 ..^ S ) --> A /\ c : ( 0 ..^ S ) --> B ) <-> ( c : ( 0 ..^ S ) --> A /\ ran c C_ B ) ) ) |
12 |
4 11
|
syl5bb |
|- ( ph -> ( c : ( 0 ..^ S ) --> ( A i^i B ) <-> ( c : ( 0 ..^ S ) --> A /\ ran c C_ B ) ) ) |
13 |
|
nnex |
|- NN e. _V |
14 |
13
|
a1i |
|- ( ph -> NN e. _V ) |
15 |
14 1
|
ssexd |
|- ( ph -> A e. _V ) |
16 |
|
inex1g |
|- ( A e. _V -> ( A i^i B ) e. _V ) |
17 |
15 16
|
syl |
|- ( ph -> ( A i^i B ) e. _V ) |
18 |
|
ovex |
|- ( 0 ..^ S ) e. _V |
19 |
|
elmapg |
|- ( ( ( A i^i B ) e. _V /\ ( 0 ..^ S ) e. _V ) -> ( c e. ( ( A i^i B ) ^m ( 0 ..^ S ) ) <-> c : ( 0 ..^ S ) --> ( A i^i B ) ) ) |
20 |
17 18 19
|
sylancl |
|- ( ph -> ( c e. ( ( A i^i B ) ^m ( 0 ..^ S ) ) <-> c : ( 0 ..^ S ) --> ( A i^i B ) ) ) |
21 |
|
elmapg |
|- ( ( A e. _V /\ ( 0 ..^ S ) e. _V ) -> ( c e. ( A ^m ( 0 ..^ S ) ) <-> c : ( 0 ..^ S ) --> A ) ) |
22 |
15 18 21
|
sylancl |
|- ( ph -> ( c e. ( A ^m ( 0 ..^ S ) ) <-> c : ( 0 ..^ S ) --> A ) ) |
23 |
22
|
anbi1d |
|- ( ph -> ( ( c e. ( A ^m ( 0 ..^ S ) ) /\ ran c C_ B ) <-> ( c : ( 0 ..^ S ) --> A /\ ran c C_ B ) ) ) |
24 |
12 20 23
|
3bitr4d |
|- ( ph -> ( c e. ( ( A i^i B ) ^m ( 0 ..^ S ) ) <-> ( c e. ( A ^m ( 0 ..^ S ) ) /\ ran c C_ B ) ) ) |
25 |
24
|
anbi1d |
|- ( ph -> ( ( c e. ( ( A i^i B ) ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) <-> ( ( c e. ( A ^m ( 0 ..^ S ) ) /\ ran c C_ B ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) ) ) |
26 |
|
inss1 |
|- ( A i^i B ) C_ A |
27 |
26 1
|
sstrid |
|- ( ph -> ( A i^i B ) C_ NN ) |
28 |
27 2 3
|
reprval |
|- ( ph -> ( ( A i^i B ) ( repr ` S ) M ) = { c e. ( ( A i^i B ) ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } ) |
29 |
28
|
eleq2d |
|- ( ph -> ( c e. ( ( A i^i B ) ( repr ` S ) M ) <-> c e. { c e. ( ( A i^i B ) ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } ) ) |
30 |
|
rabid |
|- ( c e. { c e. ( ( A i^i B ) ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } <-> ( c e. ( ( A i^i B ) ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) ) |
31 |
29 30
|
bitrdi |
|- ( ph -> ( c e. ( ( A i^i B ) ( repr ` S ) M ) <-> ( c e. ( ( A i^i B ) ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) ) ) |
32 |
1 2 3
|
reprval |
|- ( ph -> ( A ( repr ` S ) M ) = { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } ) |
33 |
32
|
eleq2d |
|- ( ph -> ( c e. ( A ( repr ` S ) M ) <-> c e. { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } ) ) |
34 |
|
rabid |
|- ( c e. { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } <-> ( c e. ( A ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) ) |
35 |
33 34
|
bitrdi |
|- ( ph -> ( c e. ( A ( repr ` S ) M ) <-> ( c e. ( A ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) ) ) |
36 |
35
|
anbi1d |
|- ( ph -> ( ( c e. ( A ( repr ` S ) M ) /\ ran c C_ B ) <-> ( ( c e. ( A ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) /\ ran c C_ B ) ) ) |
37 |
|
an32 |
|- ( ( ( c e. ( A ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) /\ ran c C_ B ) <-> ( ( c e. ( A ^m ( 0 ..^ S ) ) /\ ran c C_ B ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) ) |
38 |
36 37
|
bitrdi |
|- ( ph -> ( ( c e. ( A ( repr ` S ) M ) /\ ran c C_ B ) <-> ( ( c e. ( A ^m ( 0 ..^ S ) ) /\ ran c C_ B ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) ) ) |
39 |
25 31 38
|
3bitr4d |
|- ( ph -> ( c e. ( ( A i^i B ) ( repr ` S ) M ) <-> ( c e. ( A ( repr ` S ) M ) /\ ran c C_ B ) ) ) |