Metamath Proof Explorer

Theorem pm2mpghm

Description: The transformation of polynomial matrices into polynomials over matrices is an additive group homomorphism. (Contributed by AV, 16-Oct-2019) (Revised by AV, 6-Dec-2019)

Ref Expression
Hypotheses pm2mpfo.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
pm2mpfo.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
pm2mpfo.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
pm2mpfo.m ⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
pm2mpfo.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
pm2mpfo.x ⊢ 𝑋 = ( var1 ‘ 𝐴 )
pm2mpfo.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
pm2mpfo.q ⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
pm2mpfo.l ⊢ 𝐿 = ( Base ‘ 𝑄 )
pm2mpfo.t ⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
Assertion pm2mpghm ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐶 GrpHom 𝑄 ) )

Proof

Step Hyp Ref Expression
1 pm2mpfo.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 pm2mpfo.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3 pm2mpfo.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 pm2mpfo.m ⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
5 pm2mpfo.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
6 pm2mpfo.x ⊢ 𝑋 = ( var1 ‘ 𝐴 )
7 pm2mpfo.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
8 pm2mpfo.q ⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
9 pm2mpfo.l ⊢ 𝐿 = ( Base ‘ 𝑄 )
10 pm2mpfo.t ⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
11 eqid ⊢ ( +g ‘ 𝐶 ) = ( +g ‘ 𝐶 )
12 eqid ⊢ ( +g ‘ 𝑄 ) = ( +g ‘ 𝑄 )
13 1 2 pmatring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
14 ringgrp ⊢ ( 𝐶 ∈ Ring → 𝐶 ∈ Grp )
15 13 14 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Grp )
16 7 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
17 8 ply1ring ⊢ ( 𝐴 ∈ Ring → 𝑄 ∈ Ring )
18 16 17 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ Ring )
19 ringgrp ⊢ ( 𝑄 ∈ Ring → 𝑄 ∈ Grp )
20 18 19 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ Grp )
21 1 2 3 4 5 6 7 8 10 9 pm2mpf ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 ⟶ 𝐿 )
22 ringmnd ⊢ ( 𝐶 ∈ Ring → 𝐶 ∈ Mnd )
23 13 22 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Mnd )
24 23 anim1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐶 ∈ Mnd ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) )
25 3anass ⊢ ( ( 𝐶 ∈ Mnd ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ↔ ( 𝐶 ∈ Mnd ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) )
26 24 25 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐶 ∈ Mnd ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) )
27 3 11 mndcl ⊢ ( ( 𝐶 ∈ Mnd ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) ∈ 𝐵 )
28 26 27 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) ∈ 𝐵 )
29 2 3 decpmatval ⊢ ( ( ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) decompPMat 𝑘 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) 𝑗 ) ) ‘ 𝑘 ) ) )
30 28 29 sylan ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) decompPMat 𝑘 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) 𝑗 ) ) ‘ 𝑘 ) ) )
31 simplll ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ∈ Fin )
32 fvexd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ∈ V )
33 fvexd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ∈ V )
34 eqidd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ) )
35 eqidd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ) )
36 31 31 32 33 34 35 offval22 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ) ) )
37 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
38 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
39 simpllr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑅 ∈ Ring )
40 simprl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑖 ∈ 𝑁 )
41 simprr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑗 ∈ 𝑁 )
42 3 eleq2i ⊢ ( 𝑎 ∈ 𝐵 ↔ 𝑎 ∈ ( Base ‘ 𝐶 ) )
43 42 biimpi ⊢ ( 𝑎 ∈ 𝐵 → 𝑎 ∈ ( Base ‘ 𝐶 ) )
44 43 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑎 ∈ ( Base ‘ 𝐶 ) )
45 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
46 2 45 matecl ⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑖 𝑎 𝑗 ) ∈ ( Base ‘ 𝑃 ) )
47 40 41 44 46 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 𝑎 𝑗 ) ∈ ( Base ‘ 𝑃 ) )
48 47 ex ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑎 𝑗 ) ∈ ( Base ‘ 𝑃 ) ) )
49 48 adantrr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑎 𝑗 ) ∈ ( Base ‘ 𝑃 ) ) )
50 49 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑎 𝑗 ) ∈ ( Base ‘ 𝑃 ) ) )
51 50 3impib ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑎 𝑗 ) ∈ ( Base ‘ 𝑃 ) )
52 simpr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
53 52 3ad2ant1 ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑘 ∈ ℕ0 )
54 eqid ⊢ ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) = ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) )
55 54 45 1 37 coe1fvalcl ⊢ ( ( ( 𝑖 𝑎 𝑗 ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
56 51 53 55 syl2anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
57 7 37 38 31 39 56 matbas2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ) ∈ ( Base ‘ 𝐴 ) )
58 simprl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑖 ∈ 𝑁 )
59 simprr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑗 ∈ 𝑁 )
60 3 eleq2i ⊢ ( 𝑏 ∈ 𝐵 ↔ 𝑏 ∈ ( Base ‘ 𝐶 ) )
61 60 biimpi ⊢ ( 𝑏 ∈ 𝐵 → 𝑏 ∈ ( Base ‘ 𝐶 ) )
62 61 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑏 ∈ ( Base ‘ 𝐶 ) )
63 2 45 matecl ⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑖 𝑏 𝑗 ) ∈ ( Base ‘ 𝑃 ) )
64 58 59 62 63 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 𝑏 𝑗 ) ∈ ( Base ‘ 𝑃 ) )
65 64 ex ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑏 𝑗 ) ∈ ( Base ‘ 𝑃 ) ) )
66 65 adantrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑏 𝑗 ) ∈ ( Base ‘ 𝑃 ) ) )
67 66 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑏 𝑗 ) ∈ ( Base ‘ 𝑃 ) ) )
68 67 3impib ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑏 𝑗 ) ∈ ( Base ‘ 𝑃 ) )
69 eqid ⊢ ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) = ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) )
70 69 45 1 37 coe1fvalcl ⊢ ( ( ( 𝑖 𝑏 𝑗 ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
71 68 53 70 syl2anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
72 7 37 38 31 39 71 matbas2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ) ∈ ( Base ‘ 𝐴 ) )
73 eqid ⊢ ( +g ‘ 𝐴 ) = ( +g ‘ 𝐴 )
74 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
75 7 38 73 74 matplusg2 ⊢ ( ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ) ∈ ( Base ‘ 𝐴 ) ∧ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ) ∈ ( Base ‘ 𝐴 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ) ( +g ‘ 𝐴 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ) ) = ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ) ) )
76 57 72 75 syl2anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ) ( +g ‘ 𝐴 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ) ) = ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ) ) )
77 simplr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) )
78 77 anim1i ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) )
79 78 3impb ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) )
80 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
81 2 3 11 80 matplusgcell ⊢ ( ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) 𝑗 ) = ( ( 𝑖 𝑎 𝑗 ) ( +g ‘ 𝑃 ) ( 𝑖 𝑏 𝑗 ) ) )
82 79 81 syl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) 𝑗 ) = ( ( 𝑖 𝑎 𝑗 ) ( +g ‘ 𝑃 ) ( 𝑖 𝑏 𝑗 ) ) )
83 82 fveq2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( coe1 ‘ ( 𝑖 ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) 𝑗 ) ) = ( coe1 ‘ ( ( 𝑖 𝑎 𝑗 ) ( +g ‘ 𝑃 ) ( 𝑖 𝑏 𝑗 ) ) ) )
84 83 fveq1d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) 𝑗 ) ) ‘ 𝑘 ) = ( ( coe1 ‘ ( ( 𝑖 𝑎 𝑗 ) ( +g ‘ 𝑃 ) ( 𝑖 𝑏 𝑗 ) ) ) ‘ 𝑘 ) )
85 39 3ad2ant1 ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
86 1 45 80 74 coe1addfv ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑖 𝑎 𝑗 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑖 𝑏 𝑗 ) ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 𝑖 𝑎 𝑗 ) ( +g ‘ 𝑃 ) ( 𝑖 𝑏 𝑗 ) ) ) ‘ 𝑘 ) = ( ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ) )
87 85 51 68 53 86 syl31anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( ( 𝑖 𝑎 𝑗 ) ( +g ‘ 𝑃 ) ( 𝑖 𝑏 𝑗 ) ) ) ‘ 𝑘 ) = ( ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ) )
88 84 87 eqtrd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) 𝑗 ) ) ‘ 𝑘 ) = ( ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ) )
89 88 mpoeq3dva ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) 𝑗 ) ) ‘ 𝑘 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ) ) )
90 36 76 89 3eqtr4rd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) 𝑗 ) ) ‘ 𝑘 ) ) = ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ) ( +g ‘ 𝐴 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ) ) )
91 8 ply1sca ⊢ ( 𝐴 ∈ Ring → 𝐴 = ( Scalar ‘ 𝑄 ) )
92 16 91 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 = ( Scalar ‘ 𝑄 ) )
93 92 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 = ( Scalar ‘ 𝑄 ) )
94 93 fveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( +g ‘ 𝐴 ) = ( +g ‘ ( Scalar ‘ 𝑄 ) ) )
95 simprl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ∈ 𝐵 )
96 2 3 decpmatval ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑎 decompPMat 𝑘 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ) )
97 95 96 sylan ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑎 decompPMat 𝑘 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ) )
98 97 eqcomd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ) = ( 𝑎 decompPMat 𝑘 ) )
99 simprr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 ∈ 𝐵 )
100 2 3 decpmatval ⊢ ( ( 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑏 decompPMat 𝑘 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ) )
101 99 100 sylan ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑏 decompPMat 𝑘 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ) )
102 101 eqcomd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ) = ( 𝑏 decompPMat 𝑘 ) )
103 94 98 102 oveq123d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑎 𝑗 ) ) ‘ 𝑘 ) ) ( +g ‘ 𝐴 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑏 𝑗 ) ) ‘ 𝑘 ) ) ) = ( ( 𝑎 decompPMat 𝑘 ) ( +g ‘ ( Scalar ‘ 𝑄 ) ) ( 𝑏 decompPMat 𝑘 ) ) )
104 30 90 103 3eqtrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) decompPMat 𝑘 ) = ( ( 𝑎 decompPMat 𝑘 ) ( +g ‘ ( Scalar ‘ 𝑄 ) ) ( 𝑏 decompPMat 𝑘 ) ) )
105 104 oveq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( ( ( 𝑎 decompPMat 𝑘 ) ( +g ‘ ( Scalar ‘ 𝑄 ) ) ( 𝑏 decompPMat 𝑘 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) )
106 8 ply1lmod ⊢ ( 𝐴 ∈ Ring → 𝑄 ∈ LMod )
107 16 106 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ LMod )
108 107 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑄 ∈ LMod )
109 simpl ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
110 109 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑎 ∈ 𝐵 )
111 1 2 3 7 38 decpmatcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑎 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
112 39 110 52 111 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑎 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
113 92 eqcomd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Scalar ‘ 𝑄 ) = 𝐴 )
114 113 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( Scalar ‘ 𝑄 ) = 𝐴 )
115 114 fveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( Base ‘ ( Scalar ‘ 𝑄 ) ) = ( Base ‘ 𝐴 ) )
116 112 115 eleqtrrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑎 decompPMat 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) )
117 simpr ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
118 117 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑏 ∈ 𝐵 )
119 1 2 3 7 38 decpmatcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑏 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
120 39 118 52 119 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑏 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
121 120 115 eleqtrrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑏 decompPMat 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) )
122 eqid ⊢ ( mulGrp ‘ 𝑄 ) = ( mulGrp ‘ 𝑄 )
123 122 ringmgp ⊢ ( 𝑄 ∈ Ring → ( mulGrp ‘ 𝑄 ) ∈ Mnd )
124 18 123 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( mulGrp ‘ 𝑄 ) ∈ Mnd )
125 124 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( mulGrp ‘ 𝑄 ) ∈ Mnd )
126 6 8 9 vr1cl ⊢ ( 𝐴 ∈ Ring → 𝑋 ∈ 𝐿 )
127 16 126 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑋 ∈ 𝐿 )
128 127 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑋 ∈ 𝐿 )
129 122 9 mgpbas ⊢ 𝐿 = ( Base ‘ ( mulGrp ‘ 𝑄 ) )
130 129 5 mulgnn0cl ⊢ ( ( ( mulGrp ‘ 𝑄 ) ∈ Mnd ∧ 𝑘 ∈ ℕ0 ∧ 𝑋 ∈ 𝐿 ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐿 )
131 125 52 128 130 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐿 )
132 eqid ⊢ ( Scalar ‘ 𝑄 ) = ( Scalar ‘ 𝑄 )
133 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑄 ) ) = ( Base ‘ ( Scalar ‘ 𝑄 ) )
134 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑄 ) ) = ( +g ‘ ( Scalar ‘ 𝑄 ) )
135 9 12 132 4 133 134 lmodvsdir ⊢ ( ( 𝑄 ∈ LMod ∧ ( ( 𝑎 decompPMat 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ∧ ( 𝑏 decompPMat 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ∧ ( 𝑘 ↑ 𝑋 ) ∈ 𝐿 ) ) → ( ( ( 𝑎 decompPMat 𝑘 ) ( +g ‘ ( Scalar ‘ 𝑄 ) ) ( 𝑏 decompPMat 𝑘 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ( +g ‘ 𝑄 ) ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) )
136 108 116 121 131 135 syl13anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑎 decompPMat 𝑘 ) ( +g ‘ ( Scalar ‘ 𝑄 ) ) ( 𝑏 decompPMat 𝑘 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ( +g ‘ 𝑄 ) ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) )
137 105 136 eqtrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ( +g ‘ 𝑄 ) ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) )
138 137 mpteq2dva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ( +g ‘ 𝑄 ) ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
139 138 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ( +g ‘ 𝑄 ) ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
140 eqid ⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ 𝑄 )
141 ringcmn ⊢ ( 𝑄 ∈ Ring → 𝑄 ∈ CMnd )
142 18 141 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ CMnd )
143 142 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑄 ∈ CMnd )
144 nn0ex ⊢ ℕ0 ∈ V
145 144 a1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ℕ0 ∈ V )
146 109 anim2i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑎 ∈ 𝐵 ) )
147 df-3an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑎 ∈ 𝐵 ) )
148 146 147 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ) )
149 1 2 3 4 5 6 7 8 9 pm2mpghmlem1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐿 )
150 148 149 sylan ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐿 )
151 117 anim2i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑏 ∈ 𝐵 ) )
152 df-3an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑏 ∈ 𝐵 ) )
153 151 152 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵 ) )
154 1 2 3 4 5 6 7 8 9 pm2mpghmlem1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐿 )
155 153 154 sylan ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐿 )
156 eqidd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) )
157 eqidd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) )
158 1 2 3 4 5 6 7 8 pm2mpghmlem2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑄 ) )
159 148 158 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑄 ) )
160 1 2 3 4 5 6 7 8 pm2mpghmlem2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑄 ) )
161 153 160 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑄 ) )
162 9 140 12 143 145 150 155 156 157 159 161 gsummptfsadd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ( +g ‘ 𝑄 ) ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) = ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ( +g ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
163 139 162 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ( +g ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
164 simpll ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑁 ∈ Fin )
165 simplr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑅 ∈ Ring )
166 1 2 3 4 5 6 7 8 10 pm2mpfval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
167 164 165 28 166 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑇 ‘ ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
168 1 2 3 4 5 6 7 8 10 pm2mpfval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑎 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
169 164 165 95 168 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑇 ‘ 𝑎 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
170 1 2 3 4 5 6 7 8 10 pm2mpfval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑏 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
171 164 165 99 170 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑇 ‘ 𝑏 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
172 169 171 oveq12d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑇 ‘ 𝑎 ) ( +g ‘ 𝑄 ) ( 𝑇 ‘ 𝑏 ) ) = ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ( +g ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
173 163 167 172 3eqtr4d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑇 ‘ ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) ) = ( ( 𝑇 ‘ 𝑎 ) ( +g ‘ 𝑄 ) ( 𝑇 ‘ 𝑏 ) ) )
174 3 9 11 12 15 20 21 173 isghmd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐶 GrpHom 𝑄 ) )