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 birani ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑅 ) )
24 23 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑋 ∈ ( Base ‘ 𝑅 ) )
25 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
26 simprl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑖 ∈ 𝑁 )
27 simpr ⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
28 27 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑗 ∈ 𝑁 )
29 simplrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑌 ∈ 𝐵 )
30 2 25 3 26 28 29 matecld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 𝑌 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
31 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
32 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
33 25 31 32 rhmmul ⊢ ( ( 𝑆 ∈ ( 𝑅 RingHom 𝑃 ) ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑖 𝑌 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑆 ‘ ( 𝑋 ( .r ‘ 𝑅 ) ( 𝑖 𝑌 𝑗 ) ) ) = ( ( 𝑆 ‘ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑆 ‘ ( 𝑖 𝑌 𝑗 ) ) ) )
34 21 24 30 33 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑋 ( .r ‘ 𝑅 ) ( 𝑖 𝑌 𝑗 ) ) ) = ( ( 𝑆 ‘ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑆 ‘ ( 𝑖 𝑌 𝑗 ) ) ) )
35 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
36 35 ad2antlr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑅 ∈ Ring )
37 36 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
38 simpr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) )
39 38 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) )
40 simpr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) )
41 2 3 7 9 31 matvscacell ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑋 · 𝑌 ) 𝑗 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( 𝑖 𝑌 𝑗 ) ) )
42 37 39 40 41 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑋 · 𝑌 ) 𝑗 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( 𝑖 𝑌 𝑗 ) ) )
43 42 fveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑖 ( 𝑋 · 𝑌 ) 𝑗 ) ) = ( 𝑆 ‘ ( 𝑋 ( .r ‘ 𝑅 ) ( 𝑖 𝑌 𝑗 ) ) ) )
44 35 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
45 simpr ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
46 44 45 anim12i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) )
47 df-3an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) )
48 46 47 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ) )
49 1 2 3 4 8 mat2pmatvalel ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ 𝑌 ) 𝑗 ) = ( 𝑆 ‘ ( 𝑖 𝑌 𝑗 ) ) )
50 48 49 sylan ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ 𝑌 ) 𝑗 ) = ( 𝑆 ‘ ( 𝑖 𝑌 𝑗 ) ) )
51 50 oveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑖 ( 𝑇 ‘ 𝑌 ) 𝑗 ) ) = ( ( 𝑆 ‘ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑆 ‘ ( 𝑖 𝑌 𝑗 ) ) ) )
52 34 43 51 3eqtr4d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑖 ( 𝑋 · 𝑌 ) 𝑗 ) ) = ( ( 𝑆 ‘ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑖 ( 𝑇 ‘ 𝑌 ) 𝑗 ) ) )
53 simpll ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑁 ∈ Fin )
54 53 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑁 ∈ Fin )
55 7 2 3 9 matvscl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
56 44 55 sylan ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
57 56 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
58 1 2 3 4 8 mat2pmatvalel ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑋 · 𝑌 ) ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) 𝑗 ) = ( 𝑆 ‘ ( 𝑖 ( 𝑋 · 𝑌 ) 𝑗 ) ) )
59 54 37 57 40 58 syl31anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) 𝑗 ) = ( 𝑆 ‘ ( 𝑖 ( 𝑋 · 𝑌 ) 𝑗 ) ) )
60 4 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
61 35 60 syl ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
62 61 ad2antlr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑃 ∈ Ring )
63 62 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑃 ∈ Ring )
64 35 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
65 simpl ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐾 )
66 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
67 4 8 7 66 ply1sclcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
68 64 65 67 syl2an ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
69 1 2 3 4 5 6 mat2pmatbas0 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑌 ) ∈ 𝐻 )
70 48 69 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑇 ‘ 𝑌 ) ∈ 𝐻 )
71 68 70 jca ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑇 ‘ 𝑌 ) ∈ 𝐻 ) )
72 71 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑇 ‘ 𝑌 ) ∈ 𝐻 ) )
73 5 6 66 10 32 matvscacell ⊢ ( ( 𝑃 ∈ Ring ∧ ( ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑇 ‘ 𝑌 ) ∈ 𝐻 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) 𝑗 ) = ( ( 𝑆 ‘ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑖 ( 𝑇 ‘ 𝑌 ) 𝑗 ) ) )
74 63 72 40 73 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) 𝑗 ) = ( ( 𝑆 ‘ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑖 ( 𝑇 ‘ 𝑌 ) 𝑗 ) ) )
75 52 59 74 3eqtr4d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) 𝑗 ) = ( 𝑖 ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) 𝑗 ) )
76 75 ralrimivva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) 𝑗 ) = ( 𝑖 ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) 𝑗 ) )
77 1 2 3 4 5 6 mat2pmatbas0 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑋 · 𝑌 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) ∈ 𝐻 )
78 53 36 56 77 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) ∈ 𝐻 )
79 66 5 6 10 matvscl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) ∧ ( ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑇 ‘ 𝑌 ) ∈ 𝐻 ) ) → ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) ∈ 𝐻 )
80 53 62 71 79 syl21anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) ∈ 𝐻 )
81 5 6 eqmat ⊢ ( ( ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) ∈ 𝐻 ∧ ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) ∈ 𝐻 ) → ( ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) 𝑗 ) = ( 𝑖 ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) 𝑗 ) ) )
82 78 80 81 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) 𝑗 ) = ( 𝑖 ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) 𝑗 ) ) )
83 76 82 mpbird ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) )