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