Metamath Proof Explorer


Theorem m2cpm

Description: The result of a matrix transformation is a constant polynomial matrix. (Contributed by AV, 18-Nov-2019) (Proof shortened by AV, 28-Nov-2019)

Ref Expression
Hypotheses m2cpm.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
m2cpm.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
m2cpm.a 𝐴 = ( 𝑁 Mat 𝑅 )
m2cpm.b 𝐵 = ( Base ‘ 𝐴 )
Assertion m2cpm ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝑇𝑀 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 m2cpm.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2 m2cpm.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
3 m2cpm.a 𝐴 = ( 𝑁 Mat 𝑅 )
4 m2cpm.b 𝐵 = ( Base ‘ 𝐴 )
5 eqid ( Poly1𝑅 ) = ( Poly1𝑅 )
6 eqid ( algSc ‘ ( Poly1𝑅 ) ) = ( algSc ‘ ( Poly1𝑅 ) )
7 2 3 4 5 6 mat2pmatvalel ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( 𝑇𝑀 ) 𝑗 ) = ( ( algSc ‘ ( Poly1𝑅 ) ) ‘ ( 𝑖 𝑀 𝑗 ) ) )
8 7 adantr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑖 ( 𝑇𝑀 ) 𝑗 ) = ( ( algSc ‘ ( Poly1𝑅 ) ) ‘ ( 𝑖 𝑀 𝑗 ) ) )
9 8 fveq2d ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → ( coe1 ‘ ( 𝑖 ( 𝑇𝑀 ) 𝑗 ) ) = ( coe1 ‘ ( ( algSc ‘ ( Poly1𝑅 ) ) ‘ ( 𝑖 𝑀 𝑗 ) ) ) )
10 9 fveq1d ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( coe1 ‘ ( 𝑖 ( 𝑇𝑀 ) 𝑗 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( ( algSc ‘ ( Poly1𝑅 ) ) ‘ ( 𝑖 𝑀 𝑗 ) ) ) ‘ 𝑛 ) )
11 simpl2 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑅 ∈ Ring )
12 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
13 simprl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑖𝑁 )
14 simprr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑗𝑁 )
15 simpl3 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑀𝐵 )
16 3 12 4 13 14 15 matecld ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
17 11 16 jca ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑅 ∈ Ring ∧ ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) )
18 17 adantr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑅 ∈ Ring ∧ ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) )
19 eqid ( 0g𝑅 ) = ( 0g𝑅 )
20 5 6 12 19 coe1scl ( ( 𝑅 ∈ Ring ∧ ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) → ( coe1 ‘ ( ( algSc ‘ ( Poly1𝑅 ) ) ‘ ( 𝑖 𝑀 𝑗 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( 𝑖 𝑀 𝑗 ) , ( 0g𝑅 ) ) ) )
21 18 20 syl ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → ( coe1 ‘ ( ( algSc ‘ ( Poly1𝑅 ) ) ‘ ( 𝑖 𝑀 𝑗 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( 𝑖 𝑀 𝑗 ) , ( 0g𝑅 ) ) ) )
22 eqeq1 ( 𝑘 = 𝑛 → ( 𝑘 = 0 ↔ 𝑛 = 0 ) )
23 22 ifbid ( 𝑘 = 𝑛 → if ( 𝑘 = 0 , ( 𝑖 𝑀 𝑗 ) , ( 0g𝑅 ) ) = if ( 𝑛 = 0 , ( 𝑖 𝑀 𝑗 ) , ( 0g𝑅 ) ) )
24 23 adantl ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → if ( 𝑘 = 0 , ( 𝑖 𝑀 𝑗 ) , ( 0g𝑅 ) ) = if ( 𝑛 = 0 , ( 𝑖 𝑀 𝑗 ) , ( 0g𝑅 ) ) )
25 nnnn0 ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
26 25 adantl ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ0 )
27 ovex ( 𝑖 𝑀 𝑗 ) ∈ V
28 fvex ( 0g𝑅 ) ∈ V
29 27 28 ifex if ( 𝑛 = 0 , ( 𝑖 𝑀 𝑗 ) , ( 0g𝑅 ) ) ∈ V
30 29 a1i ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → if ( 𝑛 = 0 , ( 𝑖 𝑀 𝑗 ) , ( 0g𝑅 ) ) ∈ V )
31 21 24 26 30 fvmptd ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( coe1 ‘ ( ( algSc ‘ ( Poly1𝑅 ) ) ‘ ( 𝑖 𝑀 𝑗 ) ) ) ‘ 𝑛 ) = if ( 𝑛 = 0 , ( 𝑖 𝑀 𝑗 ) , ( 0g𝑅 ) ) )
32 nnne0 ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 )
33 32 neneqd ( 𝑛 ∈ ℕ → ¬ 𝑛 = 0 )
34 33 adantl ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → ¬ 𝑛 = 0 )
35 34 iffalsed ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → if ( 𝑛 = 0 , ( 𝑖 𝑀 𝑗 ) , ( 0g𝑅 ) ) = ( 0g𝑅 ) )
36 10 31 35 3eqtrd ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( coe1 ‘ ( 𝑖 ( 𝑇𝑀 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0g𝑅 ) )
37 36 ralrimiva ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ ( 𝑖 ( 𝑇𝑀 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0g𝑅 ) )
38 37 ralrimivva ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ∀ 𝑖𝑁𝑗𝑁𝑛 ∈ ℕ ( ( coe1 ‘ ( 𝑖 ( 𝑇𝑀 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0g𝑅 ) )
39 eqid ( 𝑁 Mat ( Poly1𝑅 ) ) = ( 𝑁 Mat ( Poly1𝑅 ) )
40 2 3 4 5 39 mat2pmatbas ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝑇𝑀 ) ∈ ( Base ‘ ( 𝑁 Mat ( Poly1𝑅 ) ) ) )
41 eqid ( Base ‘ ( 𝑁 Mat ( Poly1𝑅 ) ) ) = ( Base ‘ ( 𝑁 Mat ( Poly1𝑅 ) ) )
42 1 5 39 41 cpmatel ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑇𝑀 ) ∈ ( Base ‘ ( 𝑁 Mat ( Poly1𝑅 ) ) ) ) → ( ( 𝑇𝑀 ) ∈ 𝑆 ↔ ∀ 𝑖𝑁𝑗𝑁𝑛 ∈ ℕ ( ( coe1 ‘ ( 𝑖 ( 𝑇𝑀 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0g𝑅 ) ) )
43 40 42 syld3an3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( 𝑇𝑀 ) ∈ 𝑆 ↔ ∀ 𝑖𝑁𝑗𝑁𝑛 ∈ ℕ ( ( coe1 ‘ ( 𝑖 ( 𝑇𝑀 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0g𝑅 ) ) )
44 38 43 mpbird ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝑇𝑀 ) ∈ 𝑆 )