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