Metamath Proof Explorer

Theorem m2cpminvid2

Description: The transformation applied to the inverse transformation of a constant polynomial matrix over the ring R results in the matrix itself. (Contributed by AV, 12-Nov-2019) (Revised by AV, 14-Dec-2019)

Ref Expression
Hypotheses m2cpminvid2.s ⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
m2cpminvid2.i ⊢ 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 )
m2cpminvid2.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
Assertion m2cpminvid2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → ( 𝑇 ‘ ( 𝐼 ‘ 𝑀 ) ) = 𝑀 )

Proof

Step Hyp Ref Expression
1 m2cpminvid2.s ⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2 m2cpminvid2.i ⊢ 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 )
3 m2cpminvid2.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
4 2 1 cpm2mval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → ( 𝐼 ‘ 𝑀 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) )
5 4 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → ( 𝑇 ‘ ( 𝐼 ‘ 𝑀 ) ) = ( 𝑇 ‘ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) )
6 simp1 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → 𝑁 ∈ Fin )
7 simp2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → 𝑅 ∈ Ring )
8 eqid ⊢ ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat 𝑅 )
9 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 eqid ⊢ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
11 eqid ⊢ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) = ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) )
12 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
13 eqid ⊢ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) = ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) )
14 simp2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑥 ∈ 𝑁 )
15 simp3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑦 ∈ 𝑁 )
16 eqid ⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
17 1 16 11 13 cpmatpmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → 𝑀 ∈ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) )
18 17 3ad2ant1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑀 ∈ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) )
19 11 12 13 14 15 18 matecld ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( 𝑥 𝑀 𝑦 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
20 0nn0 ⊢ 0 ∈ ℕ0
21 eqid ⊢ ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) = ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) )
22 21 12 16 9 coe1fvalcl ⊢ ( ( ( 𝑥 𝑀 𝑦 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) )
23 19 20 22 sylancl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) )
24 8 9 10 6 7 23 matbas2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
25 eqid ⊢ ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) = ( algSc ‘ ( Poly1 ‘ 𝑅 ) )
26 3 8 10 16 25 mat2pmatval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ) → ( 𝑇 ‘ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) 𝑗 ) ) ) )
27 6 7 24 26 syl3anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → ( 𝑇 ‘ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) 𝑗 ) ) ) )
28 eqidd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) )
29 oveq12 ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( 𝑥 𝑀 𝑦 ) = ( 𝑖 𝑀 𝑗 ) )
30 29 fveq2d ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) = ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) )
31 30 fveq1d ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) = ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) )
32 31 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) ) → ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) = ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) )
33 simp2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
34 simp3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
35 fvexd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ∈ V )
36 28 32 33 34 35 ovmpod ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) 𝑗 ) = ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) )
37 36 fveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) 𝑗 ) ) = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) )
38 37 mpoeq3dva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) 𝑗 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) ) )
39 27 38 eqtrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → ( 𝑇 ‘ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) ) )
40 1 16 m2cpminvid2lem ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) )
41 simpl2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
42 simprl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → 𝑥 ∈ 𝑁 )
43 simprr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → 𝑦 ∈ 𝑁 )
44 17 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → 𝑀 ∈ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) )
45 11 12 13 42 43 44 matecld ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑥 𝑀 𝑦 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
46 45 20 22 sylancl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) )
47 16 25 9 12 ply1sclcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
48 41 46 47 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
49 eqid ⊢ ( coe1 ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) = ( coe1 ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) )
50 16 12 49 21 ply1coe1eq ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ ( 𝑥 𝑀 𝑦 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) ↔ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) = ( 𝑥 𝑀 𝑦 ) ) )
51 50 bicomd ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ ( 𝑥 𝑀 𝑦 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) = ( 𝑥 𝑀 𝑦 ) ↔ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) ) )
52 41 48 45 51 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) = ( 𝑥 𝑀 𝑦 ) ↔ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) ) )
53 40 52 mpbird ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) = ( 𝑥 𝑀 𝑦 ) )
54 53 ralrimivva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) = ( 𝑥 𝑀 𝑦 ) )
55 eqidd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) ∧ 𝑦 ∈ 𝑁 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) ) )
56 oveq12 ⊢ ( ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑦 ) → ( 𝑖 𝑀 𝑗 ) = ( 𝑥 𝑀 𝑦 ) )
57 56 fveq2d ⊢ ( ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑦 ) → ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) = ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) )
58 57 fveq1d ⊢ ( ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑦 ) → ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) = ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) )
59 58 fveq2d ⊢ ( ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑦 ) → ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) )
60 59 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) ∧ 𝑦 ∈ 𝑁 ) ∧ ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑦 ) ) → ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) )
61 simplr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) ∧ 𝑦 ∈ 𝑁 ) → 𝑥 ∈ 𝑁 )
62 simpr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) ∧ 𝑦 ∈ 𝑁 ) → 𝑦 ∈ 𝑁 )
63 fvexd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) ∧ 𝑦 ∈ 𝑁 ) → ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ∈ V )
64 55 60 61 62 63 ovmpod ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) ∧ 𝑦 ∈ 𝑁 ) → ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) ) 𝑦 ) = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) )
65 64 eqeq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) ∧ 𝑦 ∈ 𝑁 ) → ( ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) ) 𝑦 ) = ( 𝑥 𝑀 𝑦 ) ↔ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) = ( 𝑥 𝑀 𝑦 ) ) )
66 65 anasss ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) ) 𝑦 ) = ( 𝑥 𝑀 𝑦 ) ↔ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) = ( 𝑥 𝑀 𝑦 ) ) )
67 66 2ralbidva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) ) 𝑦 ) = ( 𝑥 𝑀 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) = ( 𝑥 𝑀 𝑦 ) ) )
68 54 67 mpbird ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) ) 𝑦 ) = ( 𝑥 𝑀 𝑦 ) )
69 fvexd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → ( Poly1 ‘ 𝑅 ) ∈ V )
70 7 3ad2ant1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
71 17 3ad2ant1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑀 ∈ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) )
72 11 12 13 33 34 71 matecld ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
73 eqid ⊢ ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) = ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) )
74 73 12 16 9 coe1fvalcl ⊢ ( ( ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) )
75 72 20 74 sylancl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) )
76 16 25 9 12 ply1sclcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
77 70 75 76 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
78 11 12 13 6 69 77 matbas2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) ) ∈ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) )
79 11 13 eqmat ⊢ ( ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) ) ∈ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ∧ 𝑀 ∈ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) ) = 𝑀 ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) ) 𝑦 ) = ( 𝑥 𝑀 𝑦 ) ) )
80 78 17 79 syl2anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) ) = 𝑀 ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) ) 𝑦 ) = ( 𝑥 𝑀 𝑦 ) ) )
81 68 80 mpbird ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 0 ) ) ) = 𝑀 )
82 5 39 81 3eqtrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → ( 𝑇 ‘ ( 𝐼 ‘ 𝑀 ) ) = 𝑀 )