Theorem m2pmfzmap

Description: The transformed values of a (finite) mapping of integers to matrices. (Contributed by AV, 4-Nov-2019)

	Ref	Expression
Hypotheses	m2pmfzmap.a	|- A = ( N Mat R )
	m2pmfzmap.b	|- B = ( Base ` A )
	m2pmfzmap.p	|- P = ( Poly1 ` R )
	m2pmfzmap.y	|- Y = ( N Mat P )
	m2pmfzmap.t	|- T = ( N matToPolyMat R )
Assertion	m2pmfzmap	|- ( ( ( N e. Fin /\ R e. Ring /\ S e. NN0 ) /\ ( b e. ( B ^m ( 0 ... S ) ) /\ I e. ( 0 ... S ) ) ) -> ( T ` ( b ` I ) ) e. ( Base ` Y ) )

Proof

Step	Hyp	Ref	Expression
1		m2pmfzmap.a	|- A = ( N Mat R )
2		m2pmfzmap.b	|- B = ( Base ` A )
3		m2pmfzmap.p	|- P = ( Poly1 ` R )
4		m2pmfzmap.y	|- Y = ( N Mat P )
5		m2pmfzmap.t	|- T = ( N matToPolyMat R )
6		simpl1	|- ( ( ( N e. Fin /\ R e. Ring /\ S e. NN0 ) /\ ( b e. ( B ^m ( 0 ... S ) ) /\ I e. ( 0 ... S ) ) ) -> N e. Fin )
7		simpl2	|- ( ( ( N e. Fin /\ R e. Ring /\ S e. NN0 ) /\ ( b e. ( B ^m ( 0 ... S ) ) /\ I e. ( 0 ... S ) ) ) -> R e. Ring )
8		elmapi	|- ( b e. ( B ^m ( 0 ... S ) ) -> b : ( 0 ... S ) --> B )
9	8	ffvelcdmda	|- ( ( b e. ( B ^m ( 0 ... S ) ) /\ I e. ( 0 ... S ) ) -> ( b ` I ) e. B )
10	9	adantl	|- ( ( ( N e. Fin /\ R e. Ring /\ S e. NN0 ) /\ ( b e. ( B ^m ( 0 ... S ) ) /\ I e. ( 0 ... S ) ) ) -> ( b ` I ) e. B )
11	5 1 2 3 4	mat2pmatbas	|- ( ( N e. Fin /\ R e. Ring /\ ( b ` I ) e. B ) -> ( T ` ( b ` I ) ) e. ( Base ` Y ) )
12	6 7 10 11	syl3anc	|- ( ( ( N e. Fin /\ R e. Ring /\ S e. NN0 ) /\ ( b e. ( B ^m ( 0 ... S ) ) /\ I e. ( 0 ... S ) ) ) -> ( T ` ( b ` I ) ) e. ( Base ` Y ) )