Metamath Proof Explorer

Theorem mat2pmatmul

Description: The transformation of matrices into polynomial matrices preserves the multiplication. (Contributed by AV, 29-Oct-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 ‘ 𝐶 )
Assertion mat2pmatmul ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑇 ‘ ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( .r ‘ 𝐶 ) ( 𝑇 ‘ 𝑦 ) ) )

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 eqid ⊢ ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
8 2 7 matmulr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐴 ) )
9 8 eqcomd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( .r ‘ 𝐴 ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) )
10 9 oveqdr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑦 ) )
11 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
12 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
13 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
14 13 ad2antlr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑅 ∈ Ring )
15 simpll ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑁 ∈ Fin )
16 3 eleq2i ⊢ ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( Base ‘ 𝐴 ) )
17 16 biimpi ⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ( Base ‘ 𝐴 ) )
18 17 adantr ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
19 18 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
20 2 11 matbas2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
21 20 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
22 19 21 eleqtrrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
23 3 eleq2i ⊢ ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ( Base ‘ 𝐴 ) )
24 23 biimpi ⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ( Base ‘ 𝐴 ) )
25 24 ad2antll ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
26 20 eleq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ↔ 𝑦 ∈ ( Base ‘ 𝐴 ) ) )
27 26 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ↔ 𝑦 ∈ ( Base ‘ 𝐴 ) ) )
28 25 27 mpbird ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
29 7 11 12 14 15 15 15 22 28 mamuval ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑦 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑚 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑗 ) ) ) ) ) )
30 10 29 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑚 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑗 ) ) ) ) ) )
31 30 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑚 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑗 ) ) ) ) ) )
32 oveq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 𝑥 𝑚 ) = ( 𝑘 𝑥 𝑚 ) )
33 oveq2 ⊢ ( 𝑗 = 𝑙 → ( 𝑚 𝑦 𝑗 ) = ( 𝑚 𝑦 𝑙 ) )
34 32 33 oveqan12d ⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑙 ) → ( ( 𝑖 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑗 ) ) = ( ( 𝑘 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑙 ) ) )
35 34 mpteq2dv ⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑙 ) → ( 𝑚 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑗 ) ) ) = ( 𝑚 ∈ 𝑁 ↦ ( ( 𝑘 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑙 ) ) ) )
36 35 oveq2d ⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑙 ) → ( 𝑅 Σg ( 𝑚 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑚 ∈ 𝑁 ↦ ( ( 𝑘 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑙 ) ) ) ) )
37 36 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑙 ) ) → ( 𝑅 Σg ( 𝑚 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑚 ∈ 𝑁 ↦ ( ( 𝑘 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑙 ) ) ) ) )
38 simp2 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
39 simp3 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝑙 ∈ 𝑁 )
40 ovexd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑚 ∈ 𝑁 ↦ ( ( 𝑘 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑙 ) ) ) ) ∈ V )
41 31 37 38 39 40 ovmpod ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( 𝑘 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) 𝑙 ) = ( 𝑅 Σg ( 𝑚 ∈ 𝑁 ↦ ( ( 𝑘 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑙 ) ) ) ) )
42 41 fveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) 𝑙 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑅 Σg ( 𝑚 ∈ 𝑁 ↦ ( ( 𝑘 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑙 ) ) ) ) ) )
43 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
44 ringcmn ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
45 13 44 syl ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ CMnd )
46 45 ad2antlr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑅 ∈ CMnd )
47 46 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝑅 ∈ CMnd )
48 4 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
49 13 48 syl ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
50 ringmnd ⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ Mnd )
51 49 50 syl ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Mnd )
52 51 ad2antlr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑃 ∈ Mnd )
53 52 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝑃 ∈ Mnd )
54 15 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝑁 ∈ Fin )
55 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
56 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
57 49 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑃 ∈ Ring )
58 4 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
59 13 58 syl ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ LMod )
60 59 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑃 ∈ LMod )
61 55 56 57 60 asclghm ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( algSc ‘ 𝑃 ) ∈ ( ( Scalar ‘ 𝑃 ) GrpHom 𝑃 ) )
62 4 ply1sca ⊢ ( 𝑅 ∈ CRing → 𝑅 = ( Scalar ‘ 𝑃 ) )
63 62 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
64 63 oveq1d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑅 GrpHom 𝑃 ) = ( ( Scalar ‘ 𝑃 ) GrpHom 𝑃 ) )
65 61 64 eleqtrrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( algSc ‘ 𝑃 ) ∈ ( 𝑅 GrpHom 𝑃 ) )
66 ghmmhm ⊢ ( ( algSc ‘ 𝑃 ) ∈ ( 𝑅 GrpHom 𝑃 ) → ( algSc ‘ 𝑃 ) ∈ ( 𝑅 MndHom 𝑃 ) )
67 65 66 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( algSc ‘ 𝑃 ) ∈ ( 𝑅 MndHom 𝑃 ) )
68 67 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( algSc ‘ 𝑃 ) ∈ ( 𝑅 MndHom 𝑃 ) )
69 68 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( algSc ‘ 𝑃 ) ∈ ( 𝑅 MndHom 𝑃 ) )
70 14 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝑅 ∈ Ring )
71 70 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → 𝑅 ∈ Ring )
72 38 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
73 simpr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → 𝑚 ∈ 𝑁 )
74 19 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
75 74 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
76 75 16 sylibr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → 𝑥 ∈ 𝐵 )
77 2 11 3 72 73 76 matecld ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → ( 𝑘 𝑥 𝑚 ) ∈ ( Base ‘ 𝑅 ) )
78 39 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → 𝑙 ∈ 𝑁 )
79 2 fveq2i ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
80 3 79 eqtri ⊢ 𝐵 = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
81 80 eleq2i ⊢ ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
82 81 biimpi ⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
83 82 ad2antll ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
84 83 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝑦 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
85 84 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → 𝑦 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
86 85 81 sylibr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → 𝑦 ∈ 𝐵 )
87 2 11 3 73 78 86 matecld ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → ( 𝑚 𝑦 𝑙 ) ∈ ( Base ‘ 𝑅 ) )
88 11 12 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑘 𝑥 𝑚 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑚 𝑦 𝑙 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑘 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑙 ) ) ∈ ( Base ‘ 𝑅 ) )
89 71 77 87 88 syl3anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → ( ( 𝑘 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑙 ) ) ∈ ( Base ‘ 𝑅 ) )
90 eqid ⊢ ( 𝑚 ∈ 𝑁 ↦ ( ( 𝑘 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑙 ) ) ) = ( 𝑚 ∈ 𝑁 ↦ ( ( 𝑘 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑙 ) ) )
91 ovexd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → ( ( 𝑘 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑙 ) ) ∈ V )
92 fvexd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( 0g ‘ 𝑅 ) ∈ V )
93 90 54 91 92 fsuppmptdm ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( 𝑚 ∈ 𝑁 ↦ ( ( 𝑘 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑙 ) ) ) finSupp ( 0g ‘ 𝑅 ) )
94 11 43 47 53 54 69 89 93 gsummptmhm ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( 𝑃 Σg ( 𝑚 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( ( 𝑘 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑙 ) ) ) ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑅 Σg ( 𝑚 ∈ 𝑁 ↦ ( ( 𝑘 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑙 ) ) ) ) ) )
95 4 ply1assa ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ AssAlg )
96 95 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑃 ∈ AssAlg )
97 55 56 asclrhm ⊢ ( 𝑃 ∈ AssAlg → ( algSc ‘ 𝑃 ) ∈ ( ( Scalar ‘ 𝑃 ) RingHom 𝑃 ) )
98 96 97 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( algSc ‘ 𝑃 ) ∈ ( ( Scalar ‘ 𝑃 ) RingHom 𝑃 ) )
99 63 oveq1d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑅 RingHom 𝑃 ) = ( ( Scalar ‘ 𝑃 ) RingHom 𝑃 ) )
100 98 99 eleqtrrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( algSc ‘ 𝑃 ) ∈ ( 𝑅 RingHom 𝑃 ) )
101 100 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( algSc ‘ 𝑃 ) ∈ ( 𝑅 RingHom 𝑃 ) )
102 101 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( algSc ‘ 𝑃 ) ∈ ( 𝑅 RingHom 𝑃 ) )
103 102 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → ( algSc ‘ 𝑃 ) ∈ ( 𝑅 RingHom 𝑃 ) )
104 25 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
105 104 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
106 105 23 sylibr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → 𝑦 ∈ 𝐵 )
107 2 11 3 73 78 106 matecld ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → ( 𝑚 𝑦 𝑙 ) ∈ ( Base ‘ 𝑅 ) )
108 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
109 11 12 108 rhmmul ⊢ ( ( ( algSc ‘ 𝑃 ) ∈ ( 𝑅 RingHom 𝑃 ) ∧ ( 𝑘 𝑥 𝑚 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑚 𝑦 𝑙 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( ( 𝑘 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑙 ) ) ) = ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 𝑥 𝑚 ) ) ( .r ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑚 𝑦 𝑙 ) ) ) )
110 103 77 107 109 syl3anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( ( 𝑘 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑙 ) ) ) = ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 𝑥 𝑚 ) ) ( .r ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑚 𝑦 𝑙 ) ) ) )
111 110 mpteq2dva ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( 𝑚 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( ( 𝑘 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑙 ) ) ) ) = ( 𝑚 ∈ 𝑁 ↦ ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 𝑥 𝑚 ) ) ( .r ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑚 𝑦 𝑙 ) ) ) ) )
112 111 oveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( 𝑃 Σg ( 𝑚 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( ( 𝑘 𝑥 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑦 𝑙 ) ) ) ) ) = ( 𝑃 Σg ( 𝑚 ∈ 𝑁 ↦ ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 𝑥 𝑚 ) ) ( .r ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑚 𝑦 𝑙 ) ) ) ) ) )
113 42 94 112 3eqtr2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) 𝑙 ) ) = ( 𝑃 Σg ( 𝑚 ∈ 𝑁 ↦ ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 𝑥 𝑚 ) ) ( .r ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑚 𝑦 𝑙 ) ) ) ) ) )
114 113 mpoeq3dva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) 𝑙 ) ) ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑚 ∈ 𝑁 ↦ ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 𝑥 𝑚 ) ) ( .r ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑚 𝑦 𝑙 ) ) ) ) ) ) )
115 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
116 eqid ⊢ ( .r ‘ 𝐶 ) = ( .r ‘ 𝐶 )
117 49 ad2antlr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑃 ∈ Ring )
118 eqid ⊢ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) )
119 eqid ⊢ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) )
120 14 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
121 simp2 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
122 simp3 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
123 simp1rl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑥 ∈ 𝐵 )
124 2 11 3 121 122 123 matecld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
125 4 55 11 115 ply1sclcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ∈ ( Base ‘ 𝑃 ) )
126 120 124 125 syl2anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ∈ ( Base ‘ 𝑃 ) )
127 simp1rr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑦 ∈ 𝐵 )
128 2 11 3 121 122 127 matecld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
129 4 55 11 115 ply1sclcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ∈ ( Base ‘ 𝑃 ) )
130 120 128 129 syl2anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ∈ ( Base ‘ 𝑃 ) )
131 oveq12 ⊢ ( ( 𝑘 = 𝑖 ∧ 𝑚 = 𝑗 ) → ( 𝑘 𝑥 𝑚 ) = ( 𝑖 𝑥 𝑗 ) )
132 131 fveq2d ⊢ ( ( 𝑘 = 𝑖 ∧ 𝑚 = 𝑗 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 𝑥 𝑚 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) )
133 132 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑘 = 𝑖 ∧ 𝑚 = 𝑗 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 𝑥 𝑚 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) )
134 oveq12 ⊢ ( ( 𝑚 = 𝑖 ∧ 𝑙 = 𝑗 ) → ( 𝑚 𝑦 𝑙 ) = ( 𝑖 𝑦 𝑗 ) )
135 134 fveq2d ⊢ ( ( 𝑚 = 𝑖 ∧ 𝑙 = 𝑗 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑚 𝑦 𝑙 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) )
136 135 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑚 = 𝑖 ∧ 𝑙 = 𝑗 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑚 𝑦 𝑙 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) )
137 fvexd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑚 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 𝑥 𝑚 ) ) ∈ V )
138 fvexd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑚 𝑦 𝑙 ) ) ∈ V )
139 5 115 116 108 117 15 118 119 126 130 133 136 137 138 mpomatmul ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ( .r ‘ 𝐶 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑚 ∈ 𝑁 ↦ ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 𝑥 𝑚 ) ) ( .r ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑚 𝑦 𝑙 ) ) ) ) ) ) )
140 114 139 eqtr4d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) 𝑙 ) ) ) = ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ( .r ‘ 𝐶 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) )
141 2 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
142 13 141 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ Ring )
143 142 anim1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐴 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
144 3anass ⊢ ( ( 𝐴 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝐴 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
145 143 144 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐴 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
146 eqid ⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
147 3 146 ringcl ⊢ ( ( 𝐴 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ∈ 𝐵 )
148 145 147 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ∈ 𝐵 )
149 1 2 3 4 55 mat2pmatval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) 𝑙 ) ) ) )
150 15 14 148 149 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑇 ‘ ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑘 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) 𝑙 ) ) ) )
151 simpl ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
152 151 anim2i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑥 ∈ 𝐵 ) )
153 df-3an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑥 ∈ 𝐵 ) )
154 152 153 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵 ) )
155 1 2 3 4 55 mat2pmatval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑥 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) )
156 154 155 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑇 ‘ 𝑥 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) )
157 simpr ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
158 157 anim2i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑦 ∈ 𝐵 ) )
159 df-3an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑦 ∈ 𝐵 ) )
160 158 159 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵 ) )
161 1 2 3 4 55 mat2pmatval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑦 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) )
162 160 161 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑇 ‘ 𝑦 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) )
163 156 162 oveq12d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑇 ‘ 𝑥 ) ( .r ‘ 𝐶 ) ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ( .r ‘ 𝐶 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) )
164 140 150 163 3eqtr4d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑇 ‘ ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( .r ‘ 𝐶 ) ( 𝑇 ‘ 𝑦 ) ) )
165 164 ralrimivva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑇 ‘ ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( .r ‘ 𝐶 ) ( 𝑇 ‘ 𝑦 ) ) )