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 9	mgpbas	⊢ 𝐿 = ( Base ‘ ( mulGrp ‘ 𝑄 ) )
124	122	ringmgp	⊢ ( 𝑄 ∈ Ring → ( mulGrp ‘ 𝑄 ) ∈ Mnd )
125	18 124	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( mulGrp ‘ 𝑄 ) ∈ Mnd )
126	125	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( mulGrp ‘ 𝑄 ) ∈ Mnd )
127	6 8 9	vr1cl	⊢ ( 𝐴 ∈ Ring → 𝑋 ∈ 𝐿 )
128	16 127	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑋 ∈ 𝐿 )
129	128	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑋 ∈ 𝐿 )
130	123 5 126 52 129	mulgnn0cld	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐿 )
131		eqid	⊢ ( Scalar ‘ 𝑄 ) = ( Scalar ‘ 𝑄 )
132		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑄 ) ) = ( Base ‘ ( Scalar ‘ 𝑄 ) )
133		eqid	⊢ ( +g ‘ ( Scalar ‘ 𝑄 ) ) = ( +g ‘ ( Scalar ‘ 𝑄 ) )
134	9 12 131 4 132 133	lmodvsdir	⊢ ( ( 𝑄 ∈ LMod ∧ ( ( 𝑎 decompPMat 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ∧ ( 𝑏 decompPMat 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ∧ ( 𝑘 ↑ 𝑋 ) ∈ 𝐿 ) ) → ( ( ( 𝑎 decompPMat 𝑘 ) ( +g ‘ ( Scalar ‘ 𝑄 ) ) ( 𝑏 decompPMat 𝑘 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ( +g ‘ 𝑄 ) ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) )
135	108 116 121 130 134	syl13anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑎 decompPMat 𝑘 ) ( +g ‘ ( Scalar ‘ 𝑄 ) ) ( 𝑏 decompPMat 𝑘 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ( +g ‘ 𝑄 ) ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) )
136	105 135	eqtrd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ( +g ‘ 𝑄 ) ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) )
137	136	mpteq2dva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ( +g ‘ 𝑄 ) ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
138	137	oveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ( +g ‘ 𝑄 ) ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
139		eqid	⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ 𝑄 )
140		ringcmn	⊢ ( 𝑄 ∈ Ring → 𝑄 ∈ CMnd )
141	18 140	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ CMnd )
142	141	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑄 ∈ CMnd )
143		nn0ex	⊢ ℕ0 ∈ V
144	143	a1i	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ℕ0 ∈ V )
145	109	anim2i	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑎 ∈ 𝐵 ) )
146		df-3an	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑎 ∈ 𝐵 ) )
147	145 146	sylibr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ) )
148	1 2 3 4 5 6 7 8 9	pm2mpghmlem1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐿 )
149	147 148	sylan	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐿 )
150	117	anim2i	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑏 ∈ 𝐵 ) )
151		df-3an	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑏 ∈ 𝐵 ) )
152	150 151	sylibr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵 ) )
153	1 2 3 4 5 6 7 8 9	pm2mpghmlem1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐿 )
154	152 153	sylan	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐿 )
155		eqidd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) )
156		eqidd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) )
157	1 2 3 4 5 6 7 8	pm2mpghmlem2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑄 ) )
158	147 157	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑄 ) )
159	1 2 3 4 5 6 7 8	pm2mpghmlem2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑄 ) )
160	152 159	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑄 ) )
161	9 139 12 142 144 149 154 155 156 158 160	gsummptfsadd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ( +g ‘ 𝑄 ) ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) = ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ( +g ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
162	138 161	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ( +g ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
163		simpll	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑁 ∈ Fin )
164		simplr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑅 ∈ Ring )
165	1 2 3 4 5 6 7 8 10	pm2mpfval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
166	163 164 28 165	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑇 ‘ ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
167	1 2 3 4 5 6 7 8 10	pm2mpfval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑎 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
168	163 164 95 167	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑇 ‘ 𝑎 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
169	1 2 3 4 5 6 7 8 10	pm2mpfval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑏 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
170	163 164 99 169	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑇 ‘ 𝑏 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
171	168 170	oveq12d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑇 ‘ 𝑎 ) ( +g ‘ 𝑄 ) ( 𝑇 ‘ 𝑏 ) ) = ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑎 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ( +g ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑏 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
172	162 166 171	3eqtr4d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑇 ‘ ( 𝑎 ( +g ‘ 𝐶 ) 𝑏 ) ) = ( ( 𝑇 ‘ 𝑎 ) ( +g ‘ 𝑄 ) ( 𝑇 ‘ 𝑏 ) ) )
173	3 9 11 12 15 20 21 172	isghmd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐶 GrpHom 𝑄 ) )