Metamath Proof Explorer


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 ) ) → ( ( 𝐿 𝑋 ) ( 𝑇𝑀 ) ) ∈ 𝐵 )