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 ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) )