Metamath Proof Explorer

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 𝑛 ) ) ) 𝑏 ) )