Metamath Proof Explorer

Theorem monmatcollpw

Description: The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix having scaled monomials with the same power as entries is the matrix of the coefficients of the monomials or a zero matrix. Generalization of decpmatid (but requires R to be commutative!). (Contributed by AV, 11-Nov-2019) (Revised by AV, 4-Dec-2019)

Ref Expression
Hypotheses monmatcollpw.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
monmatcollpw.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
monmatcollpw.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
monmatcollpw.k ⊢ 𝐾 = ( Base ‘ 𝐴 )
monmatcollpw.0 ⊢ 0 = ( 0g ‘ 𝐴 )
monmatcollpw.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
monmatcollpw.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
monmatcollpw.m ⊢ · = ( ·𝑠 ‘ 𝐶 )
monmatcollpw.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
Assertion monmatcollpw ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → ( ( ( 𝐿 ↑ 𝑋 ) · ( 𝑇 ‘ 𝑀 ) ) decompPMat 𝐼 ) = if ( 𝐼 = 𝐿 , 𝑀 , 0 ) )

Proof

Step Hyp Ref Expression
1 monmatcollpw.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 monmatcollpw.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3 monmatcollpw.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4 monmatcollpw.k ⊢ 𝐾 = ( Base ‘ 𝐴 )
5 monmatcollpw.0 ⊢ 0 = ( 0g ‘ 𝐴 )
6 monmatcollpw.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
7 monmatcollpw.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
8 monmatcollpw.m ⊢ · = ( ·𝑠 ‘ 𝐶 )
9 monmatcollpw.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
10 simpll ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → 𝑁 ∈ Fin )
11 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
12 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
13 11 12 syl ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
14 13 ad2antlr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → 𝑃 ∈ Ring )
15 11 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
16 simp2 ⊢ ( ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → 𝐿 ∈ ℕ0 )
17 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
18 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
19 1 7 17 6 18 ply1moncl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐿 ∈ ℕ0 ) → ( 𝐿 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
20 15 16 19 syl2an ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → ( 𝐿 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
21 11 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
22 simp1 ⊢ ( ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → 𝑀 ∈ 𝐾 )
23 21 22 anim12i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑀 ∈ 𝐾 ) )
24 df-3an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑀 ∈ 𝐾 ) )
25 23 24 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) )
26 9 3 4 1 2 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝐶 ) )
27 25 26 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝐶 ) )
28 20 27 jca ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → ( ( 𝐿 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝐶 ) ) )
29 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
30 18 2 29 8 matvscl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) ∧ ( ( 𝐿 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 𝐿 ↑ 𝑋 ) · ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝐶 ) )
31 10 14 28 30 syl21anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → ( ( 𝐿 ↑ 𝑋 ) · ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝐶 ) )
32 simpr3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → 𝐼 ∈ ℕ0 )
33 2 29 decpmatval ⊢ ( ( ( ( 𝐿 ↑ 𝑋 ) · ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝐶 ) ∧ 𝐼 ∈ ℕ0 ) → ( ( ( 𝐿 ↑ 𝑋 ) · ( 𝑇 ‘ 𝑀 ) ) decompPMat 𝐼 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( ( 𝐿 ↑ 𝑋 ) · ( 𝑇 ‘ 𝑀 ) ) 𝑗 ) ) ‘ 𝐼 ) ) )
34 31 32 33 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → ( ( ( 𝐿 ↑ 𝑋 ) · ( 𝑇 ‘ 𝑀 ) ) decompPMat 𝐼 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( ( 𝐿 ↑ 𝑋 ) · ( 𝑇 ‘ 𝑀 ) ) 𝑗 ) ) ‘ 𝐼 ) ) )
35 14 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑃 ∈ Ring )
36 28 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝐿 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝐶 ) ) )
37 3simpc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) )
38 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
39 2 29 18 8 38 matvscacell ⊢ ( ( 𝑃 ∈ Ring ∧ ( ( 𝐿 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( ( 𝐿 ↑ 𝑋 ) · ( 𝑇 ‘ 𝑀 ) ) 𝑗 ) = ( ( 𝐿 ↑ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑖 ( 𝑇 ‘ 𝑀 ) 𝑗 ) ) )
40 35 36 37 39 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ( ( 𝐿 ↑ 𝑋 ) · ( 𝑇 ‘ 𝑀 ) ) 𝑗 ) = ( ( 𝐿 ↑ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑖 ( 𝑇 ‘ 𝑀 ) 𝑗 ) ) )
41 40 fveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( coe1 ‘ ( 𝑖 ( ( 𝐿 ↑ 𝑋 ) · ( 𝑇 ‘ 𝑀 ) ) 𝑗 ) ) = ( coe1 ‘ ( ( 𝐿 ↑ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑖 ( 𝑇 ‘ 𝑀 ) 𝑗 ) ) ) )
42 41 fveq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 ( ( 𝐿 ↑ 𝑋 ) · ( 𝑇 ‘ 𝑀 ) ) 𝑗 ) ) ‘ 𝐼 ) = ( ( coe1 ‘ ( ( 𝐿 ↑ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑖 ( 𝑇 ‘ 𝑀 ) 𝑗 ) ) ) ‘ 𝐼 ) )
43 22 anim2i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ 𝐾 ) )
44 df-3an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐾 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ 𝐾 ) )
45 43 44 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐾 ) )
46 45 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐾 ) )
47 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
48 9 3 4 1 47 mat2pmatvalel ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐾 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ 𝑀 ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑀 𝑗 ) ) )
49 46 37 48 syl2anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ( 𝑇 ‘ 𝑀 ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑀 𝑗 ) ) )
50 49 oveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝐿 ↑ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑖 ( 𝑇 ‘ 𝑀 ) 𝑗 ) ) = ( ( 𝐿 ↑ 𝑋 ) ( .r ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑀 𝑗 ) ) ) )
51 1 ply1assa ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ AssAlg )
52 51 ad2antlr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → 𝑃 ∈ AssAlg )
53 52 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑃 ∈ AssAlg )
54 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
55 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
56 simp2 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
57 simp3 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
58 4 eleq2i ⊢ ( 𝑀 ∈ 𝐾 ↔ 𝑀 ∈ ( Base ‘ 𝐴 ) )
59 58 biimpi ⊢ ( 𝑀 ∈ 𝐾 → 𝑀 ∈ ( Base ‘ 𝐴 ) )
60 59 3ad2ant1 ⊢ ( ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
61 60 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
62 61 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
63 3 54 55 56 57 62 matecld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
64 1 ply1sca ⊢ ( 𝑅 ∈ CRing → 𝑅 = ( Scalar ‘ 𝑃 ) )
65 64 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
66 65 eqcomd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( Scalar ‘ 𝑃 ) = 𝑅 )
67 66 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
68 67 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
69 68 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
70 63 69 eleqtrrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
71 20 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝐿 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
72 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
73 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
74 eqid ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
75 47 72 73 18 38 74 asclmul2 ⊢ ( ( 𝑃 ∈ AssAlg ∧ ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝐿 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝐿 ↑ 𝑋 ) ( .r ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑀 𝑗 ) ) ) = ( ( 𝑖 𝑀 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝐿 ↑ 𝑋 ) ) )
76 53 70 71 75 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝐿 ↑ 𝑋 ) ( .r ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑀 𝑗 ) ) ) = ( ( 𝑖 𝑀 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝐿 ↑ 𝑋 ) ) )
77 50 76 eqtrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝐿 ↑ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑖 ( 𝑇 ‘ 𝑀 ) 𝑗 ) ) = ( ( 𝑖 𝑀 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝐿 ↑ 𝑋 ) ) )
78 77 fveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( coe1 ‘ ( ( 𝐿 ↑ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑖 ( 𝑇 ‘ 𝑀 ) 𝑗 ) ) ) = ( coe1 ‘ ( ( 𝑖 𝑀 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝐿 ↑ 𝑋 ) ) ) )
79 78 fveq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( ( 𝐿 ↑ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑖 ( 𝑇 ‘ 𝑀 ) 𝑗 ) ) ) ‘ 𝐼 ) = ( ( coe1 ‘ ( ( 𝑖 𝑀 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝐿 ↑ 𝑋 ) ) ) ‘ 𝐼 ) )
80 11 ad2antlr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → 𝑅 ∈ Ring )
81 80 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
82 simp1r2 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝐿 ∈ ℕ0 )
83 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
84 83 54 1 7 74 17 6 coe1tm ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝐿 ∈ ℕ0 ) → ( coe1 ‘ ( ( 𝑖 𝑀 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝐿 ↑ 𝑋 ) ) ) = ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) )
85 81 63 82 84 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( coe1 ‘ ( ( 𝑖 𝑀 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝐿 ↑ 𝑋 ) ) ) = ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) )
86 85 fveq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( ( 𝑖 𝑀 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝐿 ↑ 𝑋 ) ) ) ‘ 𝐼 ) = ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) )
87 42 79 86 3eqtrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 ( ( 𝐿 ↑ 𝑋 ) · ( 𝑇 ‘ 𝑀 ) ) 𝑗 ) ) ‘ 𝐼 ) = ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) )
88 87 mpoeq3dva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( ( 𝐿 ↑ 𝑋 ) · ( 𝑇 ‘ 𝑀 ) ) 𝑗 ) ) ‘ 𝐼 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) ) )
89 21 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
90 89 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
91 3 83 mat0op ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝐴 ) = ( 𝑧 ∈ 𝑁 , 𝑤 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
92 90 91 syl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 0g ‘ 𝐴 ) = ( 𝑧 ∈ 𝑁 , 𝑤 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
93 5 92 eqtrid ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → 0 = ( 𝑧 ∈ 𝑁 , 𝑤 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
94 eqidd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) )
95 simprl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → 𝑥 ∈ 𝑁 )
96 simprr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → 𝑦 ∈ 𝑁 )
97 fvexd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 0g ‘ 𝑅 ) ∈ V )
98 93 94 95 96 97 ovmpod ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑥 0 𝑦 ) = ( 0g ‘ 𝑅 ) )
99 98 eqcomd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 0g ‘ 𝑅 ) = ( 𝑥 0 𝑦 ) )
100 99 ifeq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → if ( 𝐼 = 𝐿 , ( 𝑥 𝑀 𝑦 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝐼 = 𝐿 , ( 𝑥 𝑀 𝑦 ) , ( 𝑥 0 𝑦 ) ) )
101 eqidd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) ) )
102 oveq12 ⊢ ( ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑦 ) → ( 𝑖 𝑀 𝑗 ) = ( 𝑥 𝑀 𝑦 ) )
103 102 ifeq1d ⊢ ( ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑦 ) → if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑙 = 𝐿 , ( 𝑥 𝑀 𝑦 ) , ( 0g ‘ 𝑅 ) ) )
104 103 mpteq2dv ⊢ ( ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑦 ) → ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑥 𝑀 𝑦 ) , ( 0g ‘ 𝑅 ) ) ) )
105 104 fveq1d ⊢ ( ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑦 ) → ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) = ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑥 𝑀 𝑦 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) )
106 eqidd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑥 𝑀 𝑦 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑥 𝑀 𝑦 ) , ( 0g ‘ 𝑅 ) ) ) )
107 eqeq1 ⊢ ( 𝑙 = 𝐼 → ( 𝑙 = 𝐿 ↔ 𝐼 = 𝐿 ) )
108 107 ifbid ⊢ ( 𝑙 = 𝐼 → if ( 𝑙 = 𝐿 , ( 𝑥 𝑀 𝑦 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝐼 = 𝐿 , ( 𝑥 𝑀 𝑦 ) , ( 0g ‘ 𝑅 ) ) )
109 108 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑙 = 𝐼 ) → if ( 𝑙 = 𝐿 , ( 𝑥 𝑀 𝑦 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝐼 = 𝐿 , ( 𝑥 𝑀 𝑦 ) , ( 0g ‘ 𝑅 ) ) )
110 32 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → 𝐼 ∈ ℕ0 )
111 ovex ⊢ ( 𝑥 𝑀 𝑦 ) ∈ V
112 fvex ⊢ ( 0g ‘ 𝑅 ) ∈ V
113 111 112 ifex ⊢ if ( 𝐼 = 𝐿 , ( 𝑥 𝑀 𝑦 ) , ( 0g ‘ 𝑅 ) ) ∈ V
114 113 a1i ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → if ( 𝐼 = 𝐿 , ( 𝑥 𝑀 𝑦 ) , ( 0g ‘ 𝑅 ) ) ∈ V )
115 106 109 110 114 fvmptd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑥 𝑀 𝑦 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) = if ( 𝐼 = 𝐿 , ( 𝑥 𝑀 𝑦 ) , ( 0g ‘ 𝑅 ) ) )
116 105 115 sylan9eqr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑦 ) ) → ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) = if ( 𝐼 = 𝐿 , ( 𝑥 𝑀 𝑦 ) , ( 0g ‘ 𝑅 ) ) )
117 101 116 95 96 114 ovmpod ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) ) 𝑦 ) = if ( 𝐼 = 𝐿 , ( 𝑥 𝑀 𝑦 ) , ( 0g ‘ 𝑅 ) ) )
118 ifov ⊢ ( 𝑥 if ( 𝐼 = 𝐿 , 𝑀 , 0 ) 𝑦 ) = if ( 𝐼 = 𝐿 , ( 𝑥 𝑀 𝑦 ) , ( 𝑥 0 𝑦 ) )
119 118 a1i ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑥 if ( 𝐼 = 𝐿 , 𝑀 , 0 ) 𝑦 ) = if ( 𝐼 = 𝐿 , ( 𝑥 𝑀 𝑦 ) , ( 𝑥 0 𝑦 ) ) )
120 100 117 119 3eqtr4d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) ) 𝑦 ) = ( 𝑥 if ( 𝐼 = 𝐿 , 𝑀 , 0 ) 𝑦 ) )
121 120 ralrimivva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) ) 𝑦 ) = ( 𝑥 if ( 𝐼 = 𝐿 , 𝑀 , 0 ) 𝑦 ) )
122 simplr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → 𝑅 ∈ CRing )
123 eqidd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) )
124 107 ifbid ⊢ ( 𝑙 = 𝐼 → if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝐼 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) )
125 124 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑙 = 𝐼 ) → if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝐼 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) )
126 32 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝐼 ∈ ℕ0 )
127 54 83 ring0cl ⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
128 15 127 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
129 128 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
130 129 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
131 63 130 ifcld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → if ( 𝐼 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
132 123 125 126 131 fvmptd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) = if ( 𝐼 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) )
133 132 131 eqeltrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) ∈ ( Base ‘ 𝑅 ) )
134 3 54 4 10 122 133 matbas2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) ) ∈ 𝐾 )
135 61 58 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → 𝑀 ∈ 𝐾 )
136 3 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
137 4 5 ring0cl ⊢ ( 𝐴 ∈ Ring → 0 ∈ 𝐾 )
138 21 136 137 3syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 0 ∈ 𝐾 )
139 138 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → 0 ∈ 𝐾 )
140 135 139 ifcld ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → if ( 𝐼 = 𝐿 , 𝑀 , 0 ) ∈ 𝐾 )
141 3 4 eqmat ⊢ ( ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) ) ∈ 𝐾 ∧ if ( 𝐼 = 𝐿 , 𝑀 , 0 ) ∈ 𝐾 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) ) = if ( 𝐼 = 𝐿 , 𝑀 , 0 ) ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) ) 𝑦 ) = ( 𝑥 if ( 𝐼 = 𝐿 , 𝑀 , 0 ) 𝑦 ) ) )
142 134 140 141 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) ) = if ( 𝐼 = 𝐿 , 𝑀 , 0 ) ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) ) 𝑦 ) = ( 𝑥 if ( 𝐼 = 𝐿 , 𝑀 , 0 ) 𝑦 ) ) )
143 121 142 mpbird ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝐿 , ( 𝑖 𝑀 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 𝐼 ) ) = if ( 𝐼 = 𝐿 , 𝑀 , 0 ) )
144 34 88 143 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) → ( ( ( 𝐿 ↑ 𝑋 ) · ( 𝑇 ‘ 𝑀 ) ) decompPMat 𝐼 ) = if ( 𝐼 = 𝐿 , 𝑀 , 0 ) )