This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reprss

Description: Representations with terms in a subset. (Contributed by Thierry Arnoux, 11-Dec-2021)

Ref Expression
Hypotheses reprval.a 
|- ( ph -> A C_ NN )
reprval.m 
|- ( ph -> M e. ZZ )
reprval.s 
|- ( ph -> S e. NN0 )
reprss.1 
|- ( ph -> B C_ A )
Assertion reprss 
|- ( ph -> ( B ( repr ` S ) M ) C_ ( A ( repr ` S ) M ) )

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 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 ) )