cpmadumatpolylem1

Description: Lemma 1 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	cpmadumatpolylem1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to U \circ G \in (B^{ℕ_{0}})$

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		simp1	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to N \in Fin$
23		crngring	$⊢ R \in CRing \to R \in Ring$
24	23	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in Ring$
25	22 24	jca	$⊢ (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	1 2 10 21	cpm2mf	$⊢ (N \in Fin \land R \in Ring) \to U : S ⟶ B$
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 U : S ⟶ B$
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		fco	$⊢ (U : S ⟶ B \land G : ℕ_{0} ⟶ S) \to (U \circ G) : ℕ_{0} ⟶ B$
33	28 31 32	syl2anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to (U \circ G) : ℕ_{0} ⟶ B$
34	2	fvexi	$⊢ B \in V$
35		nn0ex	$⊢ ℕ_{0} \in V$
36	34 35	pm3.2i	$⊢ (B \in V \land ℕ_{0} \in V)$
37		elmapg	$⊢ (B \in V \land ℕ_{0} \in V) \to (U \circ G \in (B^{ℕ_{0}}) \leftrightarrow (U \circ G) : ℕ_{0} ⟶ B)$
38	36 37	mp1i	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to (U \circ G \in (B^{ℕ_{0}}) \leftrightarrow (U \circ G) : ℕ_{0} ⟶ B)$
39	33 38	mpbird	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to U \circ G \in (B^{ℕ_{0}})$

Metamath Proof Explorer

Theorem cpmadumatpolylem1

Proof