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