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 = {Poly}_{1} (R)$
	m2pmfzmap.y	$⊢ Y = N Mat P$
	m2pmfzmap.t	$⊢ T = N matToPolyMat R$
Assertion	m2pmfzmap	$⊢ ((N \in Fin \land R \in Ring \land S \in ℕ_{0}) \land (b \in (B^{(0 \dots S)}) \land I \in (0 \dots S))) \to T (b (I)) \in {Base}_{Y}$

Step	Hyp	Ref	Expression
1		m2pmfzmap.a	$⊢ A = N Mat R$
2		m2pmfzmap.b	$⊢ B = {Base}_{A}$
3		m2pmfzmap.p	$⊢ P = {Poly}_{1} (R)$
4		m2pmfzmap.y	$⊢ Y = N Mat P$
5		m2pmfzmap.t	$⊢ T = N matToPolyMat R$
6		simpl1	$⊢ ((N \in Fin \land R \in Ring \land S \in ℕ_{0}) \land (b \in (B^{(0 \dots S)}) \land I \in (0 \dots S))) \to N \in Fin$
7		simpl2	$⊢ ((N \in Fin \land R \in Ring \land S \in ℕ_{0}) \land (b \in (B^{(0 \dots S)}) \land I \in (0 \dots S))) \to R \in Ring$
8		elmapi	$⊢ b \in (B^{(0 \dots S)}) \to b : (0 \dots S) ⟶ B$
9	8	ffvelcdmda	$⊢ (b \in (B^{(0 \dots S)}) \land I \in (0 \dots S)) \to b (I) \in B$
10	9	adantl	$⊢ ((N \in Fin \land R \in Ring \land S \in ℕ_{0}) \land (b \in (B^{(0 \dots S)}) \land I \in (0 \dots S))) \to b (I) \in B$
11	5 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land b (I) \in B) \to T (b (I)) \in {Base}_{Y}$
12	6 7 10 11	syl3anc	$⊢ ((N \in Fin \land R \in Ring \land S \in ℕ_{0}) \land (b \in (B^{(0 \dots S)}) \land I \in (0 \dots S))) \to T (b (I)) \in {Base}_{Y}$

Metamath Proof Explorer