Theorem mply1topmatcl

Description: A polynomial over matrices transformed into a polynomial matrix is a polynomial matrix. (Contributed by AV, 6-Oct-2019)

	Ref	Expression
Hypotheses	mply1topmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mply1topmat.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
	mply1topmat.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
	mply1topmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	mply1topmat.m	⊢ · = ( ·𝑠 ‘ 𝑃 )
	mply1topmat.e	⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	mply1topmat.y	⊢ 𝑌 = ( var1 ‘ 𝑅 )
	mply1topmat.i	⊢ 𝐼 = ( 𝑝 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
	mply1topmatcl.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	mply1topmatcl.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	mply1topmatcl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝐼 ‘ 𝑂 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mply1topmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		mply1topmat.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
3		mply1topmat.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
4		mply1topmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
5		mply1topmat.m	⊢ · = ( ·𝑠 ‘ 𝑃 )
6		mply1topmat.e	⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
7		mply1topmat.y	⊢ 𝑌 = ( var1 ‘ 𝑅 )
8		mply1topmat.i	⊢ 𝐼 = ( 𝑝 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
9		mply1topmatcl.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
10		mply1topmatcl.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
11	1 2 3 4 5 6 7 8	mply1topmatval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑂 ∈ 𝐿 ) → ( 𝐼 ‘ 𝑂 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
12	11	3adant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝐼 ‘ 𝑂 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
13		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
14		simp1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑁 ∈ Fin )
15	4	fvexi	⊢ 𝑃 ∈ V
16	15	a1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑃 ∈ V )
17		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
18	4	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
19		ringcmn	⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ CMnd )
20	18 19	syl	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ CMnd )
21	20	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑃 ∈ CMnd )
22	21	3ad2ant1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑃 ∈ CMnd )
23		nn0ex	⊢ ℕ0 ∈ V
24	23	a1i	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ℕ0 ∈ V )
25	4	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
26	25	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑃 ∈ LMod )
27	26	3ad2ant1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑃 ∈ LMod )
28	27	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑃 ∈ LMod )
29		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
30		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
31		simpl2	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑖 ∈ 𝑁 )
32		simpl3	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑗 ∈ 𝑁 )
33		simpl13	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑂 ∈ 𝐿 )
34		eqid	⊢ ( coe1 ‘ 𝑂 ) = ( coe1 ‘ 𝑂 )
35	34 3 2 30	coe1f	⊢ ( 𝑂 ∈ 𝐿 → ( coe1 ‘ 𝑂 ) : ℕ0 ⟶ ( Base ‘ 𝐴 ) )
36	33 35	syl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( coe1 ‘ 𝑂 ) : ℕ0 ⟶ ( Base ‘ 𝐴 ) )
37		simpr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
38	36 37	ffvelrnd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
39	1 29 30 31 32 38	matecld	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
40	4	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
41	40	eqcomd	⊢ ( 𝑅 ∈ Ring → ( Scalar ‘ 𝑃 ) = 𝑅 )
42	41	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( Scalar ‘ 𝑃 ) = 𝑅 )
43	42	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
44	43	3ad2ant1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
45	44	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
46	39 45	eleqtrrd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
47	18	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑃 ∈ Ring )
48		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
49	48	ringmgp	⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
50	47 49	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
51	50	3ad2ant1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
52	51	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
53	7 4 13	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑌 ∈ ( Base ‘ 𝑃 ) )
54	53	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑌 ∈ ( Base ‘ 𝑃 ) )
55	54	3ad2ant1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑌 ∈ ( Base ‘ 𝑃 ) )
56	55	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑌 ∈ ( Base ‘ 𝑃 ) )
57	48 13	mgpbas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
58	57 6	mulgnn0cl	⊢ ( ( ( mulGrp ‘ 𝑃 ) ∈ Mnd ∧ 𝑘 ∈ ℕ0 ∧ 𝑌 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑘 𝐸 𝑌 ) ∈ ( Base ‘ 𝑃 ) )
59	52 37 56 58	syl3anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 𝐸 𝑌 ) ∈ ( Base ‘ 𝑃 ) )
60		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
61		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
62	13 60 5 61	lmodvscl	⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑘 𝐸 𝑌 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ∈ ( Base ‘ 𝑃 ) )
63	28 46 59 62	syl3anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ∈ ( Base ‘ 𝑃 ) )
64	63	fmpttd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) : ℕ0 ⟶ ( Base ‘ 𝑃 ) )
65	1 2 3 4 5 6 7	mply1topmatcllem	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) finSupp ( 0g ‘ 𝑃 ) )
66	13 17 22 24 64 65	gsumcl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ∈ ( Base ‘ 𝑃 ) )
67	9 13 10 14 16 66	matbas2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ∈ 𝐵 )
68	12 67	eqeltrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝐼 ‘ 𝑂 ) ∈ 𝐵 )