cpmadumatpolylem2

Description: Lemma 2 for cpmadumatpoly . (Contributed by AV, 20-Nov-2019) (Revised by AV, 15-Dec-2019)

	Ref	Expression
Hypotheses	cpmadumatpoly.a	$⊢ A = N Mat R$
	cpmadumatpoly.b	$⊢ B = {Base}_{A}$
	cpmadumatpoly.p	$⊢ P = {Poly}_{1} (R)$
	cpmadumatpoly.y	$⊢ Y = N Mat P$
	cpmadumatpoly.t	$⊢ T = N matToPolyMat R$
	cpmadumatpoly.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
	cpmadumatpoly.m0	$⊢ \underset{˙}{-} = -_{Y}$
	cpmadumatpoly.0	$⊢ \underset{˙}{0} = 0_{Y}$
	cpmadumatpoly.g	$⊢ G = (n \in ℕ_{0} ⟼ if (n = 0, \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))), if (n = s + 1, T (b (s)), if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n)))))))$
	cpmadumatpoly.s	$⊢ S = N ConstPolyMat R$
	cpmadumatpoly.m1	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
	cpmadumatpoly.1	$⊢ \underset{˙}{1} = 1_{Y}$
	cpmadumatpoly.z	$⊢ Z = {var}_{1} (R)$
	cpmadumatpoly.d	$⊢ D = (Z \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)$
	cpmadumatpoly.j	$⊢ J = N maAdju P$
	cpmadumatpoly.w	$⊢ W = {Base}_{Y}$
	cpmadumatpoly.q	$⊢ Q = {Poly}_{1} (A)$
	cpmadumatpoly.x	$⊢ X = {var}_{1} (A)$
	cpmadumatpoly.m2	$⊢ \underset{˙}{*} = \cdot_{Q}$
	cpmadumatpoly.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Q}}$
	cpmadumatpoly.u	$⊢ U = N cPolyMatToMat R$
Assertion	cpmadumatpolylem2	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to {finSupp}_{0_{A}} ((U \circ G))$

Proof

Step	Hyp	Ref	Expression
1		cpmadumatpoly.a	$⊢ A = N Mat R$
2		cpmadumatpoly.b	$⊢ B = {Base}_{A}$
3		cpmadumatpoly.p	$⊢ P = {Poly}_{1} (R)$
4		cpmadumatpoly.y	$⊢ Y = N Mat P$
5		cpmadumatpoly.t	$⊢ T = N matToPolyMat R$
6		cpmadumatpoly.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
7		cpmadumatpoly.m0	$⊢ \underset{˙}{-} = -_{Y}$
8		cpmadumatpoly.0	$⊢ \underset{˙}{0} = 0_{Y}$
9		cpmadumatpoly.g	$⊢ G = (n \in ℕ_{0} ⟼ if (n = 0, \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))), if (n = s + 1, T (b (s)), if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n)))))))$
10		cpmadumatpoly.s	$⊢ S = N ConstPolyMat R$
11		cpmadumatpoly.m1	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
12		cpmadumatpoly.1	$⊢ \underset{˙}{1} = 1_{Y}$
13		cpmadumatpoly.z	$⊢ Z = {var}_{1} (R)$
14		cpmadumatpoly.d	$⊢ D = (Z \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)$
15		cpmadumatpoly.j	$⊢ J = N maAdju P$
16		cpmadumatpoly.w	$⊢ W = {Base}_{Y}$
17		cpmadumatpoly.q	$⊢ Q = {Poly}_{1} (A)$
18		cpmadumatpoly.x	$⊢ X = {var}_{1} (A)$
19		cpmadumatpoly.m2	$⊢ \underset{˙}{*} = \cdot_{Q}$
20		cpmadumatpoly.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Q}}$
21		cpmadumatpoly.u	$⊢ U = N cPolyMatToMat R$
22		fvexd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to 0_{A} \in V$
23		crngring	$⊢ R \in CRing \to R \in Ring$
24	23	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring)$
25	24	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land R \in Ring)$
26	25	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to (N \in Fin \land R \in Ring)$
27	10 3 4	0elcpmat	$⊢ (N \in Fin \land R \in Ring) \to 0_{Y} \in S$
28	26 27	syl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to 0_{Y} \in S$
29	1 2 3 4 6 7 8 5 9 10	chfacfisfcpmat	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to G : ℕ_{0} ⟶ S$
30	23 29	syl3anl2	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to G : ℕ_{0} ⟶ S$
31	30	anassrs	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to G : ℕ_{0} ⟶ S$
32	1 2 10 21	cpm2mf	$⊢ (N \in Fin \land R \in Ring) \to U : S ⟶ B$
33	26 32	syl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to U : S ⟶ B$
34		ssidd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to S \subseteq S$
35		nn0ex	$⊢ ℕ_{0} \in V$
36	35	a1i	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to ℕ_{0} \in V$
37	10	ovexi	$⊢ S \in V$
38	37	a1i	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to S \in V$
39	1 2 3 4 6 7 8 5 9	chfacffsupp	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to {finSupp}_{0_{Y}} (G)$
40	39	anassrs	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to {finSupp}_{0_{Y}} (G)$
41		eqid	$⊢ 0_{A} = 0_{A}$
42		eqid	$⊢ 0_{Y} = 0_{Y}$
43	1 21 3 4 41 42	m2cpminv0	$⊢ (N \in Fin \land R \in Ring) \to U (0_{Y}) = 0_{A}$
44	23 43	sylan2	$⊢ (N \in Fin \land R \in CRing) \to U (0_{Y}) = 0_{A}$
45	44	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to U (0_{Y}) = 0_{A}$
46	45	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to U (0_{Y}) = 0_{A}$
47	22 28 31 33 34 36 38 40 46	fsuppcor	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to {finSupp}_{0_{A}} ((U \circ G))$

Metamath Proof Explorer

Theorem cpmadumatpolylem2

Proof