Theorem mat2pmatscmxcl

Description: A transformed matrix multiplied with a power of the variable of a polynomial is a polynomial matrix. (Contributed by AV, 6-Nov-2019) (Proof shortened by AV, 28-Nov-2019)

	Ref	Expression
Hypotheses	mat2pmatscmxcl.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mat2pmatscmxcl.k	⊢ 𝐾 = ( Base ‘ 𝐴 )
	mat2pmatscmxcl.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	mat2pmatscmxcl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	mat2pmatscmxcl.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	mat2pmatscmxcl.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	mat2pmatscmxcl.m	⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
	mat2pmatscmxcl.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	mat2pmatscmxcl.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
Assertion	mat2pmatscmxcl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝐿 ↑ 𝑋 ) ∗ ( 𝑇 ‘ 𝑀 ) ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mat2pmatscmxcl.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		mat2pmatscmxcl.k	⊢ 𝐾 = ( Base ‘ 𝐴 )
3		mat2pmatscmxcl.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
4		mat2pmatscmxcl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
5		mat2pmatscmxcl.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
6		mat2pmatscmxcl.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
7		mat2pmatscmxcl.m	⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
8		mat2pmatscmxcl.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
9		mat2pmatscmxcl.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
10		simpll	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → 𝑁 ∈ Fin )
11	4	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
12	11	ad2antlr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → 𝑃 ∈ Ring )
13		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
14		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
15	4 9 13 8 14	ply1moncl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐿 ∈ ℕ0 ) → ( 𝐿 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
16	15	ad2ant2l	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝐿 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
17		simpl	⊢ ( ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) → 𝑀 ∈ 𝐾 )
18	17	anim2i	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑀 ∈ 𝐾 ) )
19		df-3an	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑀 ∈ 𝐾 ) )
20	18 19	sylibr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) )
21	3 1 2 4 5 6	mat2pmatbas0	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) → ( 𝑇 ‘ 𝑀 ) ∈ 𝐵 )
22	20 21	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑇 ‘ 𝑀 ) ∈ 𝐵 )
23	14 5 6 7	matvscl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) ∧ ( ( 𝐿 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑇 ‘ 𝑀 ) ∈ 𝐵 ) ) → ( ( 𝐿 ↑ 𝑋 ) ∗ ( 𝑇 ‘ 𝑀 ) ) ∈ 𝐵 )
24	10 12 16 22 23	syl22anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝐿 ↑ 𝑋 ) ∗ ( 𝑇 ‘ 𝑀 ) ) ∈ 𝐵 )