chfacfscmulfsupp

Description: A mapping of scaled values of the "characteristic factor function" is finitely supported. (Contributed by AV, 8-Nov-2019)

	Ref	Expression
Hypotheses	chfacfisf.a	$⊢ A = N Mat R$
	chfacfisf.b	$⊢ B = {Base}_{A}$
	chfacfisf.p	$⊢ P = {Poly}_{1} (R)$
	chfacfisf.y	$⊢ Y = N Mat P$
	chfacfisf.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
	chfacfisf.s	$⊢ \underset{˙}{-} = -_{Y}$
	chfacfisf.0	$⊢ \underset{˙}{0} = 0_{Y}$
	chfacfisf.t	$⊢ T = N matToPolyMat R$
	chfacfisf.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)))))))$
	chfacfscmulcl.x	$⊢ X = {var}_{1} (R)$
	chfacfscmulcl.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
	chfacfscmulcl.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
Assertion	chfacfscmulfsupp	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to {finSupp}_{\underset{˙}{0}} ((i \in ℕ_{0} ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)))$

Proof

Step	Hyp	Ref	Expression
1		chfacfisf.a	$⊢ A = N Mat R$
2		chfacfisf.b	$⊢ B = {Base}_{A}$
3		chfacfisf.p	$⊢ P = {Poly}_{1} (R)$
4		chfacfisf.y	$⊢ Y = N Mat P$
5		chfacfisf.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
6		chfacfisf.s	$⊢ \underset{˙}{-} = -_{Y}$
7		chfacfisf.0	$⊢ \underset{˙}{0} = 0_{Y}$
8		chfacfisf.t	$⊢ T = N matToPolyMat R$
9		chfacfisf.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		chfacfscmulcl.x	$⊢ X = {var}_{1} (R)$
11		chfacfscmulcl.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
12		chfacfscmulcl.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
13	7	fvexi	$⊢ \underset{˙}{0} \in V$
14	13	a1i	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \underset{˙}{0} \in V$
15		ovexd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in ℕ_{0}) \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i) \in V$
16		nnnn0	$⊢ s \in ℕ \to s \in ℕ_{0}$
17		peano2nn0	$⊢ s \in ℕ_{0} \to s + 1 \in ℕ_{0}$
18	16 17	syl	$⊢ s \in ℕ \to s + 1 \in ℕ_{0}$
19	18	ad2antrl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to s + 1 \in ℕ_{0}$
20		vex	$⊢ k \in V$
21		csbov12g	$⊢ k \in V \to ⦋ k / i ⦌ ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) = ⦋ k / i ⦌ (i \underset{˙}{\times} X) \underset{˙}{\cdot} ⦋ k / i ⦌ G (i)$
22		csbov1g	$⊢ k \in V \to ⦋ k / i ⦌ (i \underset{˙}{\times} X) = ⦋ k / i ⦌ i \underset{˙}{\times} X$
23		csbvarg	$⊢ k \in V \to ⦋ k / i ⦌ i = k$
24	23	oveq1d	$⊢ k \in V \to ⦋ k / i ⦌ i \underset{˙}{\times} X = k \underset{˙}{\times} X$
25	22 24	eqtrd	$⊢ k \in V \to ⦋ k / i ⦌ (i \underset{˙}{\times} X) = k \underset{˙}{\times} X$
26		csbfv	$⊢ ⦋ k / i ⦌ G (i) = G (k)$
27	26	a1i	$⊢ k \in V \to ⦋ k / i ⦌ G (i) = G (k)$
28	25 27	oveq12d	$⊢ k \in V \to ⦋ k / i ⦌ (i \underset{˙}{\times} X) \underset{˙}{\cdot} ⦋ k / i ⦌ G (i) = (k \underset{˙}{\times} X) \underset{˙}{\cdot} G (k)$
29	21 28	eqtrd	$⊢ k \in V \to ⦋ k / i ⦌ ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) = (k \underset{˙}{\times} X) \underset{˙}{\cdot} G (k)$
30	20 29	mp1i	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in ℕ_{0}) \land s + 1 < k) \to ⦋ k / i ⦌ ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) = (k \underset{˙}{\times} X) \underset{˙}{\cdot} G (k)$
31		simplll	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in ℕ_{0}) \land s + 1 < k) \to (N \in Fin \land R \in CRing \land M \in B)$
32		simpllr	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in ℕ_{0}) \land s + 1 < k) \to (s \in ℕ \land b \in (B^{(0 \dots s)}))$
33	16	adantr	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to s \in ℕ_{0}$
34	33	ad2antlr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in ℕ_{0}) \to s \in ℕ_{0}$
35	34	nn0zd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in ℕ_{0}) \to s \in ℤ$
36	35	adantr	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in ℕ_{0}) \land s + 1 < k) \to s \in ℤ$
37		2z	$⊢ 2 \in ℤ$
38	37	a1i	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in ℕ_{0}) \land s + 1 < k) \to 2 \in ℤ$
39	36 38	zaddcld	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in ℕ_{0}) \land s + 1 < k) \to s + 2 \in ℤ$
40		simplr	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in ℕ_{0}) \land s + 1 < k) \to k \in ℕ_{0}$
41	40	nn0zd	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in ℕ_{0}) \land s + 1 < k) \to k \in ℤ$
42	19	nn0zd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to s + 1 \in ℤ$
43		nn0z	$⊢ k \in ℕ_{0} \to k \in ℤ$
44		zltp1le	$⊢ (s + 1 \in ℤ \land k \in ℤ) \to (s + 1 < k \leftrightarrow s + 1 + 1 \leq k)$
45	42 43 44	syl2an	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in ℕ_{0}) \to (s + 1 < k \leftrightarrow s + 1 + 1 \leq k)$
46	45	biimpa	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in ℕ_{0}) \land s + 1 < k) \to s + 1 + 1 \leq k$
47		nncn	$⊢ s \in ℕ \to s \in ℂ$
48		add1p1	$⊢ s \in ℂ \to s + 1 + 1 = s + 2$
49	47 48	syl	$⊢ s \in ℕ \to s + 1 + 1 = s + 2$
50	49	breq1d	$⊢ s \in ℕ \to (s + 1 + 1 \leq k \leftrightarrow s + 2 \leq k)$
51	50	bicomd	$⊢ s \in ℕ \to (s + 2 \leq k \leftrightarrow s + 1 + 1 \leq k)$
52	51	adantr	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to (s + 2 \leq k \leftrightarrow s + 1 + 1 \leq k)$
53	52	ad2antlr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in ℕ_{0}) \to (s + 2 \leq k \leftrightarrow s + 1 + 1 \leq k)$
54	53	adantr	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in ℕ_{0}) \land s + 1 < k) \to (s + 2 \leq k \leftrightarrow s + 1 + 1 \leq k)$
55	46 54	mpbird	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in ℕ_{0}) \land s + 1 < k) \to s + 2 \leq k$
56		eluz2	$⊢ k \in ℤ_{\geq (s + 2)} \leftrightarrow (s + 2 \in ℤ \land k \in ℤ \land s + 2 \leq k)$
57	39 41 55 56	syl3anbrc	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in ℕ_{0}) \land s + 1 < k) \to k \in ℤ_{\geq (s + 2)}$
58	1 2 3 4 5 6 7 8 9 10 11 12	chfacfscmul0	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)})) \land k \in ℤ_{\geq (s + 2)}) \to (k \underset{˙}{\times} X) \underset{˙}{\cdot} G (k) = \underset{˙}{0}$
59	31 32 57 58	syl3anc	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in ℕ_{0}) \land s + 1 < k) \to (k \underset{˙}{\times} X) \underset{˙}{\cdot} G (k) = \underset{˙}{0}$
60	30 59	eqtrd	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in ℕ_{0}) \land s + 1 < k) \to ⦋ k / i ⦌ ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) = \underset{˙}{0}$
61	60	ex	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in ℕ_{0}) \to (s + 1 < k \to ⦋ k / i ⦌ ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) = \underset{˙}{0})$
62	61	ralrimiva	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \forall k \in ℕ_{0} (s + 1 < k \to ⦋ k / i ⦌ ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) = \underset{˙}{0})$
63		breq1	$⊢ z = s + 1 \to (z < k \leftrightarrow s + 1 < k)$
64	63	rspceaimv	$⊢ (s + 1 \in ℕ_{0} \land \forall k \in ℕ_{0} (s + 1 < k \to ⦋ k / i ⦌ ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) = \underset{˙}{0})) \to \exists z \in ℕ_{0} \forall k \in ℕ_{0} (z < k \to ⦋ k / i ⦌ ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) = \underset{˙}{0})$
65	19 62 64	syl2anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \exists z \in ℕ_{0} \forall k \in ℕ_{0} (z < k \to ⦋ k / i ⦌ ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) = \underset{˙}{0})$
66	14 15 65	mptnn0fsupp	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to {finSupp}_{\underset{˙}{0}} ((i \in ℕ_{0} ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)))$

Metamath Proof Explorer

Theorem chfacfscmulfsupp

Proof