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	$⊢ A = N Mat R$
	mply1topmat.q	$⊢ Q = {Poly}_{1} (A)$
	mply1topmat.l	$⊢ L = {Base}_{Q}$
	mply1topmat.p	$⊢ P = {Poly}_{1} (R)$
	mply1topmat.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	mply1topmat.e	$⊢ E = \cdot_{{mulGrp}_{P}}$
	mply1topmat.y	$⊢ Y = {var}_{1} (R)$
	mply1topmat.i	$⊢ I = (p \in L ⟼ (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y))))$
	mply1topmatcl.c	$⊢ C = N Mat P$
	mply1topmatcl.b	$⊢ B = {Base}_{C}$
Assertion	mply1topmatcl	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to I (O) \in B$

Proof

Step	Hyp	Ref	Expression
1		mply1topmat.a	$⊢ A = N Mat R$
2		mply1topmat.q	$⊢ Q = {Poly}_{1} (A)$
3		mply1topmat.l	$⊢ L = {Base}_{Q}$
4		mply1topmat.p	$⊢ P = {Poly}_{1} (R)$
5		mply1topmat.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
6		mply1topmat.e	$⊢ E = \cdot_{{mulGrp}_{P}}$
7		mply1topmat.y	$⊢ Y = {var}_{1} (R)$
8		mply1topmat.i	$⊢ I = (p \in L ⟼ (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y))))$
9		mply1topmatcl.c	$⊢ C = N Mat P$
10		mply1topmatcl.b	$⊢ B = {Base}_{C}$
11	1 2 3 4 5 6 7 8	mply1topmatval	$⊢ (N \in Fin \land O \in L) \to I (O) = (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)))$
12	11	3adant2	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to I (O) = (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)))$
13		eqid	$⊢ {Base}_{P} = {Base}_{P}$
14		simp1	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to N \in Fin$
15	4	fvexi	$⊢ P \in V$
16	15	a1i	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to P \in V$
17		eqid	$⊢ 0_{P} = 0_{P}$
18	4	ply1ring	$⊢ R \in Ring \to P \in Ring$
19		ringcmn	$⊢ P \in Ring \to P \in CMnd$
20	18 19	syl	$⊢ R \in Ring \to P \in CMnd$
21	20	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to P \in CMnd$
22	21	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \to P \in CMnd$
23		nn0ex	$⊢ ℕ_{0} \in V$
24	23	a1i	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \to ℕ_{0} \in V$
25	4	ply1lmod	$⊢ R \in Ring \to P \in LMod$
26	25	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to P \in LMod$
27	26	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \to P \in LMod$
28	27	adantr	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to P \in LMod$
29		eqid	$⊢ {Base}_{R} = {Base}_{R}$
30		eqid	$⊢ {Base}_{A} = {Base}_{A}$
31		simpl2	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to i \in N$
32		simpl3	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to j \in N$
33		simpl13	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to O \in L$
34		eqid	$⊢ {coe}_{1} (O) = {coe}_{1} (O)$
35	34 3 2 30	coe1f	$⊢ O \in L \to {coe}_{1} (O) : ℕ_{0} ⟶ {Base}_{A}$
36	33 35	syl	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to {coe}_{1} (O) : ℕ_{0} ⟶ {Base}_{A}$
37		simpr	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
38	36 37	ffvelcdmd	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to {coe}_{1} (O) (k) \in {Base}_{A}$
39	1 29 30 31 32 38	matecld	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to i {coe}_{1} (O) (k) j \in {Base}_{R}$
40	4	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
41	40	eqcomd	$⊢ R \in Ring \to Scalar (P) = R$
42	41	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to Scalar (P) = R$
43	42	fveq2d	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to {Base}_{Scalar (P)} = {Base}_{R}$
44	43	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \to {Base}_{Scalar (P)} = {Base}_{R}$
45	44	adantr	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to {Base}_{Scalar (P)} = {Base}_{R}$
46	39 45	eleqtrrd	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to i {coe}_{1} (O) (k) j \in {Base}_{Scalar (P)}$
47		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
48	47 13	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{P}}$
49	18	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to P \in Ring$
50	47	ringmgp	$⊢ P \in Ring \to {mulGrp}_{P} \in Mnd$
51	49 50	syl	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to {mulGrp}_{P} \in Mnd$
52	51	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \to {mulGrp}_{P} \in Mnd$
53	52	adantr	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to {mulGrp}_{P} \in Mnd$
54	7 4 13	vr1cl	$⊢ R \in Ring \to Y \in {Base}_{P}$
55	54	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to Y \in {Base}_{P}$
56	55	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \to Y \in {Base}_{P}$
57	56	adantr	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to Y \in {Base}_{P}$
58	48 6 53 37 57	mulgnn0cld	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to k E Y \in {Base}_{P}$
59		eqid	$⊢ Scalar (P) = Scalar (P)$
60		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
61	13 59 5 60	lmodvscl	$⊢ (P \in LMod \land i {coe}_{1} (O) (k) j \in {Base}_{Scalar (P)} \land k E Y \in {Base}_{P}) \to (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y) \in {Base}_{P}$
62	28 46 58 61	syl3anc	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y) \in {Base}_{P}$
63	62	fmpttd	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \to (k \in ℕ_{0} ⟼ (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)) : ℕ_{0} ⟶ {Base}_{P}$
64	1 2 3 4 5 6 7	mply1topmatcllem	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \to {finSupp}_{0_{P}} ((k \in ℕ_{0} ⟼ (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)))$
65	13 17 22 24 63 64	gsumcl	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \to \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)) \in {Base}_{P}$
66	9 13 10 14 16 65	matbas2d	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) \in B$
67	12 66	eqeltrd	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to I (O) \in B$

Metamath Proof Explorer

Theorem mply1topmatcl

Proof