chfacffsupp

Description: The "characteristic factor function" is finitely supported. (Contributed by AV, 20-Nov-2019) (Proof shortened by AV, 23-Dec-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)))))))$
Assertion	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)$

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		fvexd	$⊢ ((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 V$
11		ovex	$⊢ \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))) \in V$
12		fvex	$⊢ T (b (s)) \in V$
13	7	fvexi	$⊢ \underset{˙}{0} \in V$
14		ovex	$⊢ T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n))) \in V$
15	13 14	ifex	$⊢ if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n)))) \in V$
16	12 15	ifex	$⊢ 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))))) \in V$
17	11 16	ifex	$⊢ 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)))))) \in V$
18	17	a1i	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \to 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)))))) \in V$
19		nnnn0	$⊢ s \in ℕ \to s \in ℕ_{0}$
20		peano2nn0	$⊢ s \in ℕ_{0} \to s + 1 \in ℕ_{0}$
21	19 20	syl	$⊢ s \in ℕ \to s + 1 \in ℕ_{0}$
22	21	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}$
23		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}$
24		0red	$⊢ ((((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 0 \in ℝ$
25		nnre	$⊢ s \in ℕ \to s \in ℝ$
26		peano2re	$⊢ s \in ℝ \to s + 1 \in ℝ$
27	25 26	syl	$⊢ s \in ℕ \to s + 1 \in ℝ$
28	27	adantr	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to s + 1 \in ℝ$
29	28	ad3antlr	$⊢ ((((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 \in ℝ$
30		nn0re	$⊢ k \in ℕ_{0} \to k \in ℝ$
31	30	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}) \land s + 1 < k) \to k \in ℝ$
32	19	adantr	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to s \in ℕ_{0}$
33	32	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}$
34		nn0p1gt0	$⊢ s \in ℕ_{0} \to 0 < s + 1$
35	33 34	syl	$⊢ (((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 0 < s + 1$
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 0 < s + 1$
37		simpr	$⊢ ((((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 < k$
38	24 29 31 36 37	lttrd	$⊢ ((((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 0 < k$
39	38	gt0ne0d	$⊢ ((((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 \neq 0$
40	39	neneqd	$⊢ ((((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 \neg k = 0$
41	40	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) \land n = k) \to \neg k = 0$
42		eqeq1	$⊢ n = k \to (n = 0 \leftrightarrow k = 0)$
43	42	notbid	$⊢ n = k \to (\neg n = 0 \leftrightarrow \neg k = 0)$
44	43	adantl	$⊢ (((((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) \land n = k) \to (\neg n = 0 \leftrightarrow \neg k = 0)$
45	41 44	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) \land n = k) \to \neg n = 0$
46	45	iffalsed	$⊢ (((((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) \land n = k) \to 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)))))) = 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)))))$
47	28	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 + 1 \in ℝ$
48		ltne	$⊢ (s + 1 \in ℝ \land s + 1 < k) \to k \neq s + 1$
49	47 48	sylan	$⊢ ((((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 \neq s + 1$
50	49	neneqd	$⊢ ((((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 \neg k = s + 1$
51	50	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) \land n = k) \to \neg k = s + 1$
52		eqeq1	$⊢ n = k \to (n = s + 1 \leftrightarrow k = s + 1)$
53	52	notbid	$⊢ n = k \to (\neg n = s + 1 \leftrightarrow \neg k = s + 1)$
54	53	adantl	$⊢ (((((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) \land n = k) \to (\neg n = s + 1 \leftrightarrow \neg k = s + 1)$
55	51 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) \land n = k) \to \neg n = s + 1$
56	55	iffalsed	$⊢ (((((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) \land n = k) \to 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))))) = if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n))))$
57		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) \land n = k) \to s + 1 < k$
58		breq2	$⊢ n = k \to (s + 1 < n \leftrightarrow s + 1 < k)$
59	58	adantl	$⊢ (((((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) \land n = k) \to (s + 1 < n \leftrightarrow s + 1 < k)$
60	57 59	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) \land n = k) \to s + 1 < n$
61	60	iftrued	$⊢ (((((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) \land n = k) \to if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n)))) = \underset{˙}{0}$
62	61 7	eqtrdi	$⊢ (((((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) \land n = k) \to if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n)))) = 0_{Y}$
63	46 56 62	3eqtrd	$⊢ (((((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) \land n = k) \to 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)))))) = 0_{Y}$
64	23 63	csbied	$⊢ ((((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 / n ⦌ 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)))))) = 0_{Y}$
65	64	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 / n ⦌ 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)))))) = 0_{Y})$
66	65	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 / n ⦌ 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)))))) = 0_{Y})$
67		breq1	$⊢ l = s + 1 \to (l < k \leftrightarrow s + 1 < k)$
68	67	rspceaimv	$⊢ (s + 1 \in ℕ_{0} \land \forall k \in ℕ_{0} (s + 1 < k \to ⦋ k / n ⦌ 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)))))) = 0_{Y})) \to \exists l \in ℕ_{0} \forall k \in ℕ_{0} (l < k \to ⦋ k / n ⦌ 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)))))) = 0_{Y})$
69	22 66 68	syl2anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \exists l \in ℕ_{0} \forall k \in ℕ_{0} (l < k \to ⦋ k / n ⦌ 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)))))) = 0_{Y})$
70	10 18 69	mptnn0fsupp	$⊢ ((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}} ((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))))))))$
71	9 70	eqbrtrid	$⊢ ((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)$

Metamath Proof Explorer

Theorem chfacffsupp

Proof