Metamath Proof Explorer


Theorem mat2pmatlin

Description: The transformation of matrices into polynomial matrices is "linear", analogous to lmhmlin . Since A and C have different scalar rings, T cannot be a left module homomorphism as defined in df-lmhm , see lmhmsca . (Contributed by AV, 13-Nov-2019) (Proof shortened by AV, 28-Nov-2019)

Ref Expression
Hypotheses mat2pmatbas.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
mat2pmatbas.a 𝐴 = ( 𝑁 Mat 𝑅 )
mat2pmatbas.b 𝐵 = ( Base ‘ 𝐴 )
mat2pmatbas.p 𝑃 = ( Poly1𝑅 )
mat2pmatbas.c 𝐶 = ( 𝑁 Mat 𝑃 )
mat2pmatbas0.h 𝐻 = ( Base ‘ 𝐶 )
mat2pmatlin.k 𝐾 = ( Base ‘ 𝑅 )
mat2pmatlin.s 𝑆 = ( algSc ‘ 𝑃 )
mat2pmatlin.m · = ( ·𝑠𝐴 )
mat2pmatlin.n × = ( ·𝑠𝐶 )
Assertion mat2pmatlin ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) → ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝑆𝑋 ) × ( 𝑇𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 mat2pmatbas.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
2 mat2pmatbas.a 𝐴 = ( 𝑁 Mat 𝑅 )
3 mat2pmatbas.b 𝐵 = ( Base ‘ 𝐴 )
4 mat2pmatbas.p 𝑃 = ( Poly1𝑅 )
5 mat2pmatbas.c 𝐶 = ( 𝑁 Mat 𝑃 )
6 mat2pmatbas0.h 𝐻 = ( Base ‘ 𝐶 )
7 mat2pmatlin.k 𝐾 = ( Base ‘ 𝑅 )
8 mat2pmatlin.s 𝑆 = ( algSc ‘ 𝑃 )
9 mat2pmatlin.m · = ( ·𝑠𝐴 )
10 mat2pmatlin.n × = ( ·𝑠𝐶 )
11 simpr ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ CRing )
12 4 ply1assa ( 𝑅 ∈ CRing → 𝑃 ∈ AssAlg )
13 eqid ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
14 8 13 asclrhm ( 𝑃 ∈ AssAlg → 𝑆 ∈ ( ( Scalar ‘ 𝑃 ) RingHom 𝑃 ) )
15 11 12 14 3syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑆 ∈ ( ( Scalar ‘ 𝑃 ) RingHom 𝑃 ) )
16 4 ply1sca ( 𝑅 ∈ CRing → 𝑅 = ( Scalar ‘ 𝑃 ) )
17 16 adantl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
18 17 oveq1d ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑅 RingHom 𝑃 ) = ( ( Scalar ‘ 𝑃 ) RingHom 𝑃 ) )
19 15 18 eleqtrrd ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑆 ∈ ( 𝑅 RingHom 𝑃 ) )
20 19 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) → 𝑆 ∈ ( 𝑅 RingHom 𝑃 ) )
21 20 adantr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑆 ∈ ( 𝑅 RingHom 𝑃 ) )
22 7 eleq2i ( 𝑋𝐾𝑋 ∈ ( Base ‘ 𝑅 ) )
23 22 biimpi ( 𝑋𝐾𝑋 ∈ ( Base ‘ 𝑅 ) )
24 23 adantr ( ( 𝑋𝐾𝑌𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑅 ) )
25 24 ad2antlr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑋 ∈ ( Base ‘ 𝑅 ) )
26 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
27 simprl ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑖𝑁 )
28 simpr ( ( 𝑖𝑁𝑗𝑁 ) → 𝑗𝑁 )
29 28 adantl ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑗𝑁 )
30 simplrr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑌𝐵 )
31 2 26 3 27 29 30 matecld ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 𝑌 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
32 eqid ( .r𝑅 ) = ( .r𝑅 )
33 eqid ( .r𝑃 ) = ( .r𝑃 )
34 26 32 33 rhmmul ( ( 𝑆 ∈ ( 𝑅 RingHom 𝑃 ) ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑖 𝑌 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑆 ‘ ( 𝑋 ( .r𝑅 ) ( 𝑖 𝑌 𝑗 ) ) ) = ( ( 𝑆𝑋 ) ( .r𝑃 ) ( 𝑆 ‘ ( 𝑖 𝑌 𝑗 ) ) ) )
35 21 25 31 34 syl3anc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑆 ‘ ( 𝑋 ( .r𝑅 ) ( 𝑖 𝑌 𝑗 ) ) ) = ( ( 𝑆𝑋 ) ( .r𝑃 ) ( 𝑆 ‘ ( 𝑖 𝑌 𝑗 ) ) ) )
36 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
37 36 ad2antlr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) → 𝑅 ∈ Ring )
38 37 adantr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑅 ∈ Ring )
39 simpr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) → ( 𝑋𝐾𝑌𝐵 ) )
40 39 adantr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑋𝐾𝑌𝐵 ) )
41 simpr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖𝑁𝑗𝑁 ) )
42 2 3 7 9 32 matvscacell ( ( 𝑅 ∈ Ring ∧ ( 𝑋𝐾𝑌𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( 𝑋 · 𝑌 ) 𝑗 ) = ( 𝑋 ( .r𝑅 ) ( 𝑖 𝑌 𝑗 ) ) )
43 38 40 41 42 syl3anc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( 𝑋 · 𝑌 ) 𝑗 ) = ( 𝑋 ( .r𝑅 ) ( 𝑖 𝑌 𝑗 ) ) )
44 43 fveq2d ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑆 ‘ ( 𝑖 ( 𝑋 · 𝑌 ) 𝑗 ) ) = ( 𝑆 ‘ ( 𝑋 ( .r𝑅 ) ( 𝑖 𝑌 𝑗 ) ) ) )
45 36 anim2i ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
46 simpr ( ( 𝑋𝐾𝑌𝐵 ) → 𝑌𝐵 )
47 45 46 anim12i ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌𝐵 ) )
48 df-3an ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌𝐵 ) )
49 47 48 sylibr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌𝐵 ) )
50 1 2 3 4 8 mat2pmatvalel ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( 𝑇𝑌 ) 𝑗 ) = ( 𝑆 ‘ ( 𝑖 𝑌 𝑗 ) ) )
51 49 50 sylan ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( 𝑇𝑌 ) 𝑗 ) = ( 𝑆 ‘ ( 𝑖 𝑌 𝑗 ) ) )
52 51 oveq2d ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( ( 𝑆𝑋 ) ( .r𝑃 ) ( 𝑖 ( 𝑇𝑌 ) 𝑗 ) ) = ( ( 𝑆𝑋 ) ( .r𝑃 ) ( 𝑆 ‘ ( 𝑖 𝑌 𝑗 ) ) ) )
53 35 44 52 3eqtr4d ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑆 ‘ ( 𝑖 ( 𝑋 · 𝑌 ) 𝑗 ) ) = ( ( 𝑆𝑋 ) ( .r𝑃 ) ( 𝑖 ( 𝑇𝑌 ) 𝑗 ) ) )
54 simpll ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) → 𝑁 ∈ Fin )
55 54 adantr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑁 ∈ Fin )
56 7 2 3 9 matvscl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
57 45 56 sylan ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
58 57 adantr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
59 1 2 3 4 8 mat2pmatvalel ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑋 · 𝑌 ) ∈ 𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) 𝑗 ) = ( 𝑆 ‘ ( 𝑖 ( 𝑋 · 𝑌 ) 𝑗 ) ) )
60 55 38 58 41 59 syl31anc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) 𝑗 ) = ( 𝑆 ‘ ( 𝑖 ( 𝑋 · 𝑌 ) 𝑗 ) ) )
61 4 ply1ring ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
62 36 61 syl ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
63 62 ad2antlr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) → 𝑃 ∈ Ring )
64 63 adantr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑃 ∈ Ring )
65 36 adantl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
66 simpl ( ( 𝑋𝐾𝑌𝐵 ) → 𝑋𝐾 )
67 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
68 4 8 7 67 ply1sclcl ( ( 𝑅 ∈ Ring ∧ 𝑋𝐾 ) → ( 𝑆𝑋 ) ∈ ( Base ‘ 𝑃 ) )
69 65 66 68 syl2an ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) → ( 𝑆𝑋 ) ∈ ( Base ‘ 𝑃 ) )
70 1 2 3 4 5 6 mat2pmatbas0 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌𝐵 ) → ( 𝑇𝑌 ) ∈ 𝐻 )
71 49 70 syl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) → ( 𝑇𝑌 ) ∈ 𝐻 )
72 69 71 jca ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) → ( ( 𝑆𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑇𝑌 ) ∈ 𝐻 ) )
73 72 adantr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( ( 𝑆𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑇𝑌 ) ∈ 𝐻 ) )
74 5 6 67 10 33 matvscacell ( ( 𝑃 ∈ Ring ∧ ( ( 𝑆𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑇𝑌 ) ∈ 𝐻 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( ( 𝑆𝑋 ) × ( 𝑇𝑌 ) ) 𝑗 ) = ( ( 𝑆𝑋 ) ( .r𝑃 ) ( 𝑖 ( 𝑇𝑌 ) 𝑗 ) ) )
75 64 73 41 74 syl3anc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( ( 𝑆𝑋 ) × ( 𝑇𝑌 ) ) 𝑗 ) = ( ( 𝑆𝑋 ) ( .r𝑃 ) ( 𝑖 ( 𝑇𝑌 ) 𝑗 ) ) )
76 53 60 75 3eqtr4d ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) 𝑗 ) = ( 𝑖 ( ( 𝑆𝑋 ) × ( 𝑇𝑌 ) ) 𝑗 ) )
77 76 ralrimivva ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) → ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) 𝑗 ) = ( 𝑖 ( ( 𝑆𝑋 ) × ( 𝑇𝑌 ) ) 𝑗 ) )
78 1 2 3 4 5 6 mat2pmatbas0 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑋 · 𝑌 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) ∈ 𝐻 )
79 54 37 57 78 syl3anc ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) → ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) ∈ 𝐻 )
80 67 5 6 10 matvscl ( ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) ∧ ( ( 𝑆𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑇𝑌 ) ∈ 𝐻 ) ) → ( ( 𝑆𝑋 ) × ( 𝑇𝑌 ) ) ∈ 𝐻 )
81 54 63 72 80 syl21anc ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) → ( ( 𝑆𝑋 ) × ( 𝑇𝑌 ) ) ∈ 𝐻 )
82 5 6 eqmat ( ( ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) ∈ 𝐻 ∧ ( ( 𝑆𝑋 ) × ( 𝑇𝑌 ) ) ∈ 𝐻 ) → ( ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝑆𝑋 ) × ( 𝑇𝑌 ) ) ↔ ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) 𝑗 ) = ( 𝑖 ( ( 𝑆𝑋 ) × ( 𝑇𝑌 ) ) 𝑗 ) ) )
83 79 81 82 syl2anc ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) → ( ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝑆𝑋 ) × ( 𝑇𝑌 ) ) ↔ ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) 𝑗 ) = ( 𝑖 ( ( 𝑆𝑋 ) × ( 𝑇𝑌 ) ) 𝑗 ) ) )
84 77 83 mpbird ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐾𝑌𝐵 ) ) → ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝑆𝑋 ) × ( 𝑇𝑌 ) ) )