chfacfpmmulfsupp

Description: A mapping of values of the "characteristic factor function" multiplied with a constant polynomial matrix is finitely supported. (Contributed by AV, 23-Nov-2019)

	Ref	Expression
Hypotheses	cayhamlem1.a	$⊢ A = N Mat R$
	cayhamlem1.b	$⊢ B = {Base}_{A}$
	cayhamlem1.p	$⊢ P = {Poly}_{1} (R)$
	cayhamlem1.y	$⊢ Y = N Mat P$
	cayhamlem1.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
	cayhamlem1.s	$⊢ \underset{˙}{-} = -_{Y}$
	cayhamlem1.0	$⊢ \underset{˙}{0} = 0_{Y}$
	cayhamlem1.t	$⊢ T = N matToPolyMat R$
	cayhamlem1.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)))))))$
	cayhamlem1.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Y}}$
Assertion	chfacfpmmulfsupp	$⊢ ((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} T (M)) \underset{˙}{\times} G (i)))$

Proof

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

Metamath Proof Explorer

Theorem chfacfpmmulfsupp

Proof