Theorem mp2pm2mp

Description: A polynomial over matrices transformed into a polynomial matrix transformed back into the polynomial over matrices. (Contributed by AV, 12-Oct-2019)

	Ref	Expression
Hypotheses	mp2pm2mp.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mp2pm2mp.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
	mp2pm2mp.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
	mp2pm2mp.m	⊢ · = ( ·𝑠 ‘ 𝑃 )
	mp2pm2mp.e	⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	mp2pm2mp.y	⊢ 𝑌 = ( var1 ‘ 𝑅 )
	mp2pm2mp.i	⊢ 𝐼 = ( 𝑝 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
	mp2pm2mplem2.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	mp2pm2mp.t	⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
Assertion	mp2pm2mp	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑇 ‘ ( 𝐼 ‘ 𝑂 ) ) = 𝑂 )

Proof

Step	Hyp	Ref	Expression
1		mp2pm2mp.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		mp2pm2mp.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
3		mp2pm2mp.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
4		mp2pm2mp.m	⊢ · = ( ·𝑠 ‘ 𝑃 )
5		mp2pm2mp.e	⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
6		mp2pm2mp.y	⊢ 𝑌 = ( var1 ‘ 𝑅 )
7		mp2pm2mp.i	⊢ 𝐼 = ( 𝑝 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
8		mp2pm2mplem2.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
9		mp2pm2mp.t	⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
10		eqid	⊢ ( 𝑁 Mat 𝑃 ) = ( 𝑁 Mat 𝑃 )
11		eqid	⊢ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) = ( Base ‘ ( 𝑁 Mat 𝑃 ) )
12	1 2 3 8 4 5 6 7 10 11	mply1topmatcl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝐼 ‘ 𝑂 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
13		eqid	⊢ ( ·𝑠 ‘ 𝑄 ) = ( ·𝑠 ‘ 𝑄 )
14		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝑄 ) ) = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
15		eqid	⊢ ( var1 ‘ 𝐴 ) = ( var1 ‘ 𝐴 )
16	8 10 11 13 14 15 1 2 9	pm2mpfval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝐼 ‘ 𝑂 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) ) → ( 𝑇 ‘ ( 𝐼 ‘ 𝑂 ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) )
17	12 16	syld3an3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑇 ‘ ( 𝐼 ‘ 𝑂 ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) )
18	1	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
19	18	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝐴 ∈ Ring )
20		eqid	⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ 𝑄 )
21	2	ply1ring	⊢ ( 𝐴 ∈ Ring → 𝑄 ∈ Ring )
22		ringcmn	⊢ ( 𝑄 ∈ Ring → 𝑄 ∈ CMnd )
23	18 21 22	3syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ CMnd )
24	23	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑄 ∈ CMnd )
25		nn0ex	⊢ ℕ0 ∈ V
26	25	a1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ℕ0 ∈ V )
27	19	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑛 ∈ ℕ0 ) → 𝐴 ∈ Ring )
28		simpl2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑅 ∈ Ring )
29	12	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐼 ‘ 𝑂 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
30		simpr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
31		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
32	8 10 11 1 31	decpmatcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐼 ‘ 𝑂 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ∈ ( Base ‘ 𝐴 ) )
33	28 29 30 32	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ∈ ( Base ‘ 𝐴 ) )
34		eqid	⊢ ( mulGrp ‘ 𝑄 ) = ( mulGrp ‘ 𝑄 )
35	31 2 15 13 34 14 3	ply1tmcl	⊢ ( ( 𝐴 ∈ Ring ∧ ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ∈ ( Base ‘ 𝐴 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ∈ 𝐿 )
36	27 33 30 35	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ∈ 𝐿 )
37	36	fmpttd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) : ℕ0 ⟶ 𝐿 )
38		fveq2	⊢ ( 𝑘 = 𝑛 → ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝑝 ) ‘ 𝑛 ) )
39	38	oveqd	⊢ ( 𝑘 = 𝑛 → ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) = ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑛 ) 𝑗 ) )
40		oveq1	⊢ ( 𝑘 = 𝑛 → ( 𝑘 𝐸 𝑌 ) = ( 𝑛 𝐸 𝑌 ) )
41	39 40	oveq12d	⊢ ( 𝑘 = 𝑛 → ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) = ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑛 ) 𝑗 ) · ( 𝑛 𝐸 𝑌 ) ) )
42	41	cbvmptv	⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑛 ) 𝑗 ) · ( 𝑛 𝐸 𝑌 ) ) )
43	42	a1i	⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑛 ) 𝑗 ) · ( 𝑛 𝐸 𝑌 ) ) ) )
44	43	oveq2d	⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) = ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑛 ) 𝑗 ) · ( 𝑛 𝐸 𝑌 ) ) ) ) )
45	44	mpoeq3ia	⊢ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑛 ) 𝑗 ) · ( 𝑛 𝐸 𝑌 ) ) ) ) )
46	45	mpteq2i	⊢ ( 𝑝 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ) = ( 𝑝 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑛 ) 𝑗 ) · ( 𝑛 𝐸 𝑌 ) ) ) ) ) )
47	7 46	eqtri	⊢ 𝐼 = ( 𝑝 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑛 ) 𝑗 ) · ( 𝑛 𝐸 𝑌 ) ) ) ) ) )
48	1 2 3 4 5 6 47 8 13 14 15	mp2pm2mplem5	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) finSupp ( 0g ‘ 𝑄 ) )
49	3 20 24 26 37 48	gsumcl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ∈ 𝐿 )
50		simp3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑂 ∈ 𝐿 )
51	19 49 50	3jca	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝐴 ∈ Ring ∧ ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ∈ 𝐿 ∧ 𝑂 ∈ 𝐿 ) )
52	1 2 3 4 5 6 7 8	mp2pm2mplem4	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝑛 ) )
53	52	oveq1d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) = ( ( ( coe1 ‘ 𝑂 ) ‘ 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) )
54	53	adantlr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑙 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) = ( ( ( coe1 ‘ 𝑂 ) ‘ 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) )
55	54	mpteq2dva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑙 ∈ ℕ0 ) → ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑂 ) ‘ 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) )
56	55	oveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑙 ∈ ℕ0 ) → ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑂 ) ‘ 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) )
57	56	fveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑙 ∈ ℕ0 ) → ( coe1 ‘ ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) = ( coe1 ‘ ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑂 ) ‘ 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) )
58	57	fveq1d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑙 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) = ( ( coe1 ‘ ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑂 ) ‘ 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) )
59	19 50	jca	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝐴 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) )
60	59	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑙 ∈ ℕ0 ) → ( 𝐴 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) )
61		eqid	⊢ ( coe1 ‘ 𝑂 ) = ( coe1 ‘ 𝑂 )
62	2 15 3 13 34 14 61	ply1coe	⊢ ( ( 𝐴 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑂 = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑂 ) ‘ 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) )
63	60 62	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑙 ∈ ℕ0 ) → 𝑂 = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑂 ) ‘ 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) )
64	63	eqcomd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑙 ∈ ℕ0 ) → ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑂 ) ‘ 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) = 𝑂 )
65	64	fveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑙 ∈ ℕ0 ) → ( coe1 ‘ ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑂 ) ‘ 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) = ( coe1 ‘ 𝑂 ) )
66	65	fveq1d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑙 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑂 ) ‘ 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝑙 ) )
67	58 66	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑙 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝑙 ) )
68	67	ralrimiva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ∀ 𝑙 ∈ ℕ0 ( ( coe1 ‘ ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝑙 ) )
69		eqid	⊢ ( coe1 ‘ ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) = ( coe1 ‘ ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) )
70	2 3 69 61	eqcoe1ply1eq	⊢ ( ( 𝐴 ∈ Ring ∧ ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ∈ 𝐿 ∧ 𝑂 ∈ 𝐿 ) → ( ∀ 𝑙 ∈ ℕ0 ( ( coe1 ‘ ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝑙 ) → ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) = 𝑂 ) )
71	51 68 70	sylc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑛 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) = 𝑂 )
72	17 71	eqtrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑇 ‘ ( 𝐼 ‘ 𝑂 ) ) = 𝑂 )