Theorem pmatcollpwlem

Description: Lemma for pmatcollpw . (Contributed by AV, 26-Oct-2019) (Revised by AV, 4-Dec-2019)

	Ref	Expression
Hypotheses	pmatcollpw.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	pmatcollpw.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	pmatcollpw.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	pmatcollpw.m	⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
	pmatcollpw.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	pmatcollpw.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	pmatcollpw.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
Assertion	pmatcollpwlem	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) = ( 𝑎 ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) 𝑏 ) )

Proof

Step	Hyp	Ref	Expression
1		pmatcollpw.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pmatcollpw.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pmatcollpw.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		pmatcollpw.m	⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
5		pmatcollpw.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
6		pmatcollpw.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
7		pmatcollpw.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
8	1	ply1assa	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ AssAlg )
9	8	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ AssAlg )
10	9	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑃 ∈ AssAlg )
11	10	3ad2ant1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑃 ∈ AssAlg )
12		eqid	⊢ ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat 𝑅 )
13		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14		eqid	⊢ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
15		simp2	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑎 ∈ 𝑁 )
16		simp3	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑏 ∈ 𝑁 )
17		simp2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ CRing )
18	17	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑅 ∈ CRing )
19		simp3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
20	19	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑀 ∈ 𝐵 )
21		simpr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
22	1 2 3 12 14	decpmatcl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝑛 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
23	18 20 21 22	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝑛 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
24	23	3ad2ant1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑀 decompPMat 𝑛 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
25	12 13 14 15 16 24	matecld	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ∈ ( Base ‘ 𝑅 ) )
26		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
27	26	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
28	1	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
29	27 28	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
30	29	eqcomd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Scalar ‘ 𝑃 ) = 𝑅 )
31	30	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
32	31	eleq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↔ ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ∈ ( Base ‘ 𝑅 ) ) )
33	32	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↔ ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ∈ ( Base ‘ 𝑅 ) ) )
34	33	3ad2ant1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↔ ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ∈ ( Base ‘ 𝑅 ) ) )
35	25 34	mpbird	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
36		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
37		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
38	1 6 36 5 37	ply1moncl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
39	27 38	sylan	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
40	39	3ad2ant1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑛 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
41		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
42		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
43		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
44		eqid	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
45		eqid	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
46	41 42 43 37 44 45	asclmul2	⊢ ( ( 𝑃 ∈ AssAlg ∧ ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑛 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑛 ↑ 𝑋 ) ( .r ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ) ) = ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) )
47	11 35 40 46	syl3anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑛 ↑ 𝑋 ) ( .r ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ) ) = ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) )
48		eqidd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ) )
49		oveq12	⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) = ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) )
50	49	fveq2d	⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ) )
51	50	adantl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ) )
52		fvexd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ) ∈ V )
53	48 51 15 16 52	ovmpod	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ) 𝑏 ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ) )
54	53	eqcomd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ) 𝑏 ) )
55	54	oveq2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑛 ↑ 𝑋 ) ( .r ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ) ) = ( ( 𝑛 ↑ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ) 𝑏 ) ) )
56	47 55	eqtr3d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) = ( ( 𝑛 ↑ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ) 𝑏 ) ) )
57	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
58	26 57	syl	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
59	58	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ Ring )
60	59	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑃 ∈ Ring )
61	60	3ad2ant1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑃 ∈ Ring )
62		simpl1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑁 ∈ Fin )
63	18 26	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑅 ∈ Ring )
64	63	3ad2ant1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
65		simp2	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
66		simp3	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
67	23	3ad2ant1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑀 decompPMat 𝑛 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
68	12 13 14 65 66 67	matecld	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
69	1 41 13 37	ply1sclcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ∈ ( Base ‘ 𝑃 ) )
70	64 68 69	syl2anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ∈ ( Base ‘ 𝑃 ) )
71	2 37 3 62 60 70	matbas2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ) ∈ 𝐵 )
72	39 71	jca	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ) ∈ 𝐵 ) )
73	72	3ad2ant1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑛 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ) ∈ 𝐵 ) )
74	15 16	jca	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) )
75	2 3 37 4 44	matvscacell	⊢ ( ( 𝑃 ∈ Ring ∧ ( ( 𝑛 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ) ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ) ) 𝑏 ) = ( ( 𝑛 ↑ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ) 𝑏 ) ) )
76	61 73 74 75	syl3anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑎 ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ) ) 𝑏 ) = ( ( 𝑛 ↑ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ) 𝑏 ) ) )
77	27	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑅 ∈ Ring )
78	7 12 14 1 41	mat2pmatval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑀 decompPMat 𝑛 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ) → ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ) )
79	62 77 23 78	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ) )
80	79	eqcomd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ) = ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) )
81	80	oveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ) ) = ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) )
82	81	oveqd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑎 ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ) ) 𝑏 ) = ( 𝑎 ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) 𝑏 ) )
83	82	3ad2ant1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑎 ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ) ) ) 𝑏 ) = ( 𝑎 ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) 𝑏 ) )
84	56 76 83	3eqtr2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑎 ( 𝑀 decompPMat 𝑛 ) 𝑏 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑛 ↑ 𝑋 ) ) = ( 𝑎 ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) 𝑏 ) )