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	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	m2pmfzmap.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	m2pmfzmap.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	m2pmfzmap.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
	m2pmfzmap.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
Assertion	m2pmfzmap	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑆 ∈ ℕ0 ) ∧ ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑆 ) ) ∧ 𝐼 ∈ ( 0 ... 𝑆 ) ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝐼 ) ) ∈ ( Base ‘ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		m2pmfzmap.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		m2pmfzmap.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		m2pmfzmap.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4		m2pmfzmap.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5		m2pmfzmap.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
6		simpl1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑆 ∈ ℕ0 ) ∧ ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑆 ) ) ∧ 𝐼 ∈ ( 0 ... 𝑆 ) ) ) → 𝑁 ∈ Fin )
7		simpl2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑆 ∈ ℕ0 ) ∧ ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑆 ) ) ∧ 𝐼 ∈ ( 0 ... 𝑆 ) ) ) → 𝑅 ∈ Ring )
8		elmapi	⊢ ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑆 ) ) → 𝑏 : ( 0 ... 𝑆 ) ⟶ 𝐵 )
9	8	ffvelrnda	⊢ ( ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑆 ) ) ∧ 𝐼 ∈ ( 0 ... 𝑆 ) ) → ( 𝑏 ‘ 𝐼 ) ∈ 𝐵 )
10	9	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑆 ∈ ℕ0 ) ∧ ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑆 ) ) ∧ 𝐼 ∈ ( 0 ... 𝑆 ) ) ) → ( 𝑏 ‘ 𝐼 ) ∈ 𝐵 )
11	5 1 2 3 4	mat2pmatbas	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ 𝐼 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝐼 ) ) ∈ ( Base ‘ 𝑌 ) )
12	6 7 10 11	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑆 ∈ ℕ0 ) ∧ ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑆 ) ) ∧ 𝐼 ∈ ( 0 ... 𝑆 ) ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝐼 ) ) ∈ ( Base ‘ 𝑌 ) )