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 |
|
reprss.1 |
|- ( ph -> B C_ A ) |
5 |
|
nnex |
|- NN e. _V |
6 |
5
|
a1i |
|- ( ph -> NN e. _V ) |
7 |
6 1
|
ssexd |
|- ( ph -> A e. _V ) |
8 |
|
mapss |
|- ( ( A e. _V /\ B C_ A ) -> ( B ^m ( 0 ..^ S ) ) C_ ( A ^m ( 0 ..^ S ) ) ) |
9 |
7 4 8
|
syl2anc |
|- ( ph -> ( B ^m ( 0 ..^ S ) ) C_ ( A ^m ( 0 ..^ S ) ) ) |
10 |
9
|
sselda |
|- ( ( ph /\ c e. ( B ^m ( 0 ..^ S ) ) ) -> c e. ( A ^m ( 0 ..^ S ) ) ) |
11 |
10
|
adantrr |
|- ( ( ph /\ ( c e. ( B ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) ) -> c e. ( A ^m ( 0 ..^ S ) ) ) |
12 |
11
|
rabss3d |
|- ( ph -> { c e. ( B ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } C_ { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } ) |
13 |
4 1
|
sstrd |
|- ( ph -> B C_ NN ) |
14 |
13 2 3
|
reprval |
|- ( ph -> ( B ( repr ` S ) M ) = { c e. ( B ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } ) |
15 |
1 2 3
|
reprval |
|- ( ph -> ( A ( repr ` S ) M ) = { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } ) |
16 |
12 14 15
|
3sstr4d |
|- ( ph -> ( B ( repr ` S ) M ) C_ ( A ( repr ` S ) M ) ) |