Theorem pmatcollpwscmatlem2

Description: Lemma 2 for pmatcollpwscmat . (Contributed by AV, 2-Nov-2019) (Revised by AV, 4-Dec-2019)

	Ref	Expression
Hypotheses	pmatcollpwscmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	pmatcollpwscmat.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	pmatcollpwscmat.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	pmatcollpwscmat.m1	⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
	pmatcollpwscmat.e1	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	pmatcollpwscmat.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	pmatcollpwscmat.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	pmatcollpwscmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	pmatcollpwscmat.d	⊢ 𝐷 = ( Base ‘ 𝐴 )
	pmatcollpwscmat.u	⊢ 𝑈 = ( algSc ‘ 𝑃 )
	pmatcollpwscmat.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	pmatcollpwscmat.e2	⊢ 𝐸 = ( Base ‘ 𝑃 )
	pmatcollpwscmat.s	⊢ 𝑆 = ( algSc ‘ 𝑃 )
	pmatcollpwscmat.1	⊢ 1 = ( 1r ‘ 𝐶 )
	pmatcollpwscmat.m2	⊢ 𝑀 = ( 𝑄 ∗ 1 )
Assertion	pmatcollpwscmatlem2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝑇 ‘ ( 𝑀 decompPMat 𝐿 ) ) = ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) ∗ 1 ) )

Proof

Step	Hyp	Ref	Expression
1		pmatcollpwscmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pmatcollpwscmat.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pmatcollpwscmat.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		pmatcollpwscmat.m1	⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
5		pmatcollpwscmat.e1	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
6		pmatcollpwscmat.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
7		pmatcollpwscmat.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
8		pmatcollpwscmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
9		pmatcollpwscmat.d	⊢ 𝐷 = ( Base ‘ 𝐴 )
10		pmatcollpwscmat.u	⊢ 𝑈 = ( algSc ‘ 𝑃 )
11		pmatcollpwscmat.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
12		pmatcollpwscmat.e2	⊢ 𝐸 = ( Base ‘ 𝑃 )
13		pmatcollpwscmat.s	⊢ 𝑆 = ( algSc ‘ 𝑃 )
14		pmatcollpwscmat.1	⊢ 1 = ( 1r ‘ 𝐶 )
15		pmatcollpwscmat.m2	⊢ 𝑀 = ( 𝑄 ∗ 1 )
16		simpl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
17		simpr	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Ring )
18	17	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → 𝑅 ∈ Ring )
19		simpr	⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) → 𝑄 ∈ 𝐸 )
20	19	anim2i	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑄 ∈ 𝐸 ) )
21		df-3an	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝐸 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑄 ∈ 𝐸 ) )
22	20 21	sylibr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝐸 ) )
23	1 2 3 12 4 14	1pmatscmul	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝐸 ) → ( 𝑄 ∗ 1 ) ∈ 𝐵 )
24	15 23	eqeltrid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝐸 ) → 𝑀 ∈ 𝐵 )
25	22 24	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → 𝑀 ∈ 𝐵 )
26		simprl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → 𝐿 ∈ ℕ0 )
27	1 2 3 8 9	decpmatcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝐿 ) ∈ 𝐷 )
28	18 25 26 27	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝑀 decompPMat 𝐿 ) ∈ 𝐷 )
29		df-3an	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑀 decompPMat 𝐿 ) ∈ 𝐷 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 decompPMat 𝐿 ) ∈ 𝐷 ) )
30	16 28 29	sylanbrc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑀 decompPMat 𝐿 ) ∈ 𝐷 ) )
31		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
32	7 8 9 1 31	mat2pmatval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑀 decompPMat 𝐿 ) ∈ 𝐷 ) → ( 𝑇 ‘ ( 𝑀 decompPMat 𝐿 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝐿 ) 𝑗 ) ) ) )
33	30 32	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝑇 ‘ ( 𝑀 decompPMat 𝐿 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝐿 ) 𝑗 ) ) ) )
34	18 25 26	3jca	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝐿 ∈ ℕ0 ) )
35	34	3ad2ant1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝐿 ∈ ℕ0 ) )
36		3simpc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) )
37	1 2 3	decpmate	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑀 decompPMat 𝐿 ) 𝑗 ) = ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) )
38	35 36 37	syl2anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ( 𝑀 decompPMat 𝐿 ) 𝑗 ) = ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) )
39	38	fveq2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝐿 ) 𝑗 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ) )
40	39	mpoeq3dva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑀 decompPMat 𝐿 ) 𝑗 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ) ) )
41		simp1lr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
42		simp2	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
43		simp3	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
44	25	3ad2ant1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑀 ∈ 𝐵 )
45	2 12 3 42 43 44	matecld	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑀 𝑗 ) ∈ 𝐸 )
46	26	3ad2ant1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝐿 ∈ ℕ0 )
47		eqid	⊢ ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) = ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) )
48	47 12 1 11	coe1fvalcl	⊢ ( ( ( 𝑖 𝑀 𝑗 ) ∈ 𝐸 ∧ 𝐿 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ∈ 𝐾 )
49	45 46 48	syl2anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ∈ 𝐾 )
50		eqid	⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
51		eqid	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
52		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
53		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
54	11 1 50 51 52 53 31	ply1scltm	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ∈ 𝐾 ) → ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ) = ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
55	41 49 54	syl2anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ) = ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
56	55	mpoeq3dva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) )
57	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	pmatcollpwscmatlem1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( ( ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = if ( 𝑎 = 𝑏 , ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) , ( 0g ‘ 𝑃 ) ) )
58		eqidd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) )
59		oveq12	⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( 𝑖 𝑀 𝑗 ) = ( 𝑎 𝑀 𝑏 ) )
60	59	fveq2d	⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) = ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) )
61	60	fveq1d	⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) = ( ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) ‘ 𝐿 ) )
62	61	oveq1d	⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( ( ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
63	62	adantl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) ) → ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( ( ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
64		simprl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑎 ∈ 𝑁 )
65		simprr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑏 ∈ 𝑁 )
66		ovexd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( ( ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ V )
67	58 63 64 65 66	ovmpod	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) 𝑏 ) = ( ( ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
68		simpll	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → 𝑁 ∈ Fin )
69	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
70	69	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ Ring )
71	70	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → 𝑃 ∈ Ring )
72		pm3.22	⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) → ( 𝑄 ∈ 𝐸 ∧ 𝐿 ∈ ℕ0 ) )
73	72	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝑄 ∈ 𝐸 ∧ 𝐿 ∈ ℕ0 ) )
74		eqid	⊢ ( coe1 ‘ 𝑄 ) = ( coe1 ‘ 𝑄 )
75	74 12 1 11	coe1fvalcl	⊢ ( ( 𝑄 ∈ 𝐸 ∧ 𝐿 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ∈ 𝐾 )
76	73 75	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ∈ 𝐾 )
77	1 10 11 12	ply1sclcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ∈ 𝐾 ) → ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) ∈ 𝐸 )
78	18 76 77	syl2anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) ∈ 𝐸 )
79	68 71 78	3jca	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) ∈ 𝐸 ) )
80		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
81	2 12 80 14 4	scmatscmide	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) ∈ 𝐸 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) ∗ 1 ) 𝑏 ) = if ( 𝑎 = 𝑏 , ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) , ( 0g ‘ 𝑃 ) ) )
82	79 81	sylan	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) ∗ 1 ) 𝑏 ) = if ( 𝑎 = 𝑏 , ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) , ( 0g ‘ 𝑃 ) ) )
83	57 67 82	3eqtr4d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) 𝑏 ) = ( 𝑎 ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) ∗ 1 ) 𝑏 ) )
84	83	ralrimivva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) 𝑏 ) = ( 𝑎 ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) ∗ 1 ) 𝑏 ) )
85		0nn0	⊢ 0 ∈ ℕ0
86	85	a1i	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 0 ∈ ℕ0 )
87	11 1 50 51 52 53 12	ply1tmcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ∈ 𝐾 ∧ 0 ∈ ℕ0 ) → ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ 𝐸 )
88	41 49 86 87	syl3anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ 𝐸 )
89	2 12 3 68 71 88	matbas2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ∈ 𝐵 )
90	1 2 3 12 4 14	1pmatscmul	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) ∈ 𝐸 ) → ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) ∗ 1 ) ∈ 𝐵 )
91	68 18 78 90	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) ∗ 1 ) ∈ 𝐵 )
92	2 3	eqmat	⊢ ( ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ∈ 𝐵 ∧ ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) ∗ 1 ) ∈ 𝐵 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) = ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) ∗ 1 ) ↔ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) 𝑏 ) = ( 𝑎 ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) ∗ 1 ) 𝑏 ) ) )
93	89 91 92	syl2anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) = ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) ∗ 1 ) ↔ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) 𝑏 ) = ( 𝑎 ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) ∗ 1 ) 𝑏 ) ) )
94	84 93	mpbird	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) = ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) ∗ 1 ) )
95	56 94	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐿 ) ) ) = ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) ∗ 1 ) )
96	33 40 95	3eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝑇 ‘ ( 𝑀 decompPMat 𝐿 ) ) = ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) ∗ 1 ) )