chfacfpmmul0

Description: The value of the "characteristic factor function" multiplied with a constant polynomial matrix is zero almost always. (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	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}$

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		eluz2	$⊢ K \in ℤ_{\geq (s + 2)} \leftrightarrow (s + 2 \in ℤ \land K \in ℤ \land s + 2 \leq K)$
12		simpll	$⊢ ((K \in ℤ \land s \in ℕ) \land s + 2 \leq K) \to K \in ℤ$
13		nngt0	$⊢ s \in ℕ \to 0 < s$
14		nnre	$⊢ s \in ℕ \to s \in ℝ$
15	14	adantl	$⊢ (K \in ℤ \land s \in ℕ) \to s \in ℝ$
16		2rp	$⊢ 2 \in ℝ^{+}$
17	16	a1i	$⊢ (K \in ℤ \land s \in ℕ) \to 2 \in ℝ^{+}$
18	15 17	ltaddrpd	$⊢ (K \in ℤ \land s \in ℕ) \to s < s + 2$
19		0red	$⊢ (K \in ℤ \land s \in ℕ) \to 0 \in ℝ$
20		2re	$⊢ 2 \in ℝ$
21	20	a1i	$⊢ (K \in ℤ \land s \in ℕ) \to 2 \in ℝ$
22	15 21	readdcld	$⊢ (K \in ℤ \land s \in ℕ) \to s + 2 \in ℝ$
23		lttr	$⊢ (0 \in ℝ \land s \in ℝ \land s + 2 \in ℝ) \to ((0 < s \land s < s + 2) \to 0 < s + 2)$
24	19 15 22 23	syl3anc	$⊢ (K \in ℤ \land s \in ℕ) \to ((0 < s \land s < s + 2) \to 0 < s + 2)$
25	18 24	mpan2d	$⊢ (K \in ℤ \land s \in ℕ) \to (0 < s \to 0 < s + 2)$
26	25	ex	$⊢ K \in ℤ \to (s \in ℕ \to (0 < s \to 0 < s + 2))$
27	26	com13	$⊢ 0 < s \to (s \in ℕ \to (K \in ℤ \to 0 < s + 2))$
28	13 27	mpcom	$⊢ s \in ℕ \to (K \in ℤ \to 0 < s + 2)$
29	28	impcom	$⊢ (K \in ℤ \land s \in ℕ) \to 0 < s + 2$
30		zre	$⊢ K \in ℤ \to K \in ℝ$
31	30	adantr	$⊢ (K \in ℤ \land s \in ℕ) \to K \in ℝ$
32		ltleletr	$⊢ (0 \in ℝ \land s + 2 \in ℝ \land K \in ℝ) \to ((0 < s + 2 \land s + 2 \leq K) \to 0 \leq K)$
33	19 22 31 32	syl3anc	$⊢ (K \in ℤ \land s \in ℕ) \to ((0 < s + 2 \land s + 2 \leq K) \to 0 \leq K)$
34	29 33	mpand	$⊢ (K \in ℤ \land s \in ℕ) \to (s + 2 \leq K \to 0 \leq K)$
35	34	imp	$⊢ ((K \in ℤ \land s \in ℕ) \land s + 2 \leq K) \to 0 \leq K$
36		elnn0z	$⊢ K \in ℕ_{0} \leftrightarrow (K \in ℤ \land 0 \leq K)$
37	12 35 36	sylanbrc	$⊢ ((K \in ℤ \land s \in ℕ) \land s + 2 \leq K) \to K \in ℕ_{0}$
38		nncn	$⊢ s \in ℕ \to s \in ℂ$
39		add1p1	$⊢ s \in ℂ \to s + 1 + 1 = s + 2$
40	38 39	syl	$⊢ s \in ℕ \to s + 1 + 1 = s + 2$
41	40	adantl	$⊢ (K \in ℤ \land s \in ℕ) \to s + 1 + 1 = s + 2$
42	41	eqcomd	$⊢ (K \in ℤ \land s \in ℕ) \to s + 2 = s + 1 + 1$
43	42	breq1d	$⊢ (K \in ℤ \land s \in ℕ) \to (s + 2 \leq K \leftrightarrow s + 1 + 1 \leq K)$
44		nnz	$⊢ s \in ℕ \to s \in ℤ$
45	44	peano2zd	$⊢ s \in ℕ \to s + 1 \in ℤ$
46	45	anim2i	$⊢ (K \in ℤ \land s \in ℕ) \to (K \in ℤ \land s + 1 \in ℤ)$
47	46	ancomd	$⊢ (K \in ℤ \land s \in ℕ) \to (s + 1 \in ℤ \land K \in ℤ)$
48		zltp1le	$⊢ (s + 1 \in ℤ \land K \in ℤ) \to (s + 1 < K \leftrightarrow s + 1 + 1 \leq K)$
49	48	bicomd	$⊢ (s + 1 \in ℤ \land K \in ℤ) \to (s + 1 + 1 \leq K \leftrightarrow s + 1 < K)$
50	47 49	syl	$⊢ (K \in ℤ \land s \in ℕ) \to (s + 1 + 1 \leq K \leftrightarrow s + 1 < K)$
51	43 50	bitrd	$⊢ (K \in ℤ \land s \in ℕ) \to (s + 2 \leq K \leftrightarrow s + 1 < K)$
52	51	biimpa	$⊢ ((K \in ℤ \land s \in ℕ) \land s + 2 \leq K) \to s + 1 < K$
53	37 52	jca	$⊢ ((K \in ℤ \land s \in ℕ) \land s + 2 \leq K) \to (K \in ℕ_{0} \land s + 1 < K)$
54	53	ex	$⊢ (K \in ℤ \land s \in ℕ) \to (s + 2 \leq K \to (K \in ℕ_{0} \land s + 1 < K))$
55	54	impancom	$⊢ (K \in ℤ \land s + 2 \leq K) \to (s \in ℕ \to (K \in ℕ_{0} \land s + 1 < K))$
56	55	3adant1	$⊢ (s + 2 \in ℤ \land K \in ℤ \land s + 2 \leq K) \to (s \in ℕ \to (K \in ℕ_{0} \land s + 1 < K))$
57	56	com12	$⊢ s \in ℕ \to ((s + 2 \in ℤ \land K \in ℤ \land s + 2 \leq K) \to (K \in ℕ_{0} \land s + 1 < K))$
58	11 57	syl5bi	$⊢ s \in ℕ \to (K \in ℤ_{\geq (s + 2)} \to (K \in ℕ_{0} \land s + 1 < K))$
59	58	adantr	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to (K \in ℤ_{\geq (s + 2)} \to (K \in ℕ_{0} \land s + 1 < K))$
60	59	adantl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (K \in ℤ_{\geq (s + 2)} \to (K \in ℕ_{0} \land s + 1 < K))$
61		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 ℝ$
62		peano2re	$⊢ s \in ℝ \to s + 1 \in ℝ$
63	14 62	syl	$⊢ s \in ℕ \to s + 1 \in ℝ$
64	63	adantr	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to s + 1 \in ℝ$
65	64	adantl	$⊢ ((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 ℝ$
66	65	ad2antrr	$⊢ ((((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 ℝ$
67		nn0re	$⊢ K \in ℕ_{0} \to K \in ℝ$
68	67	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 ℝ$
69		nnnn0	$⊢ s \in ℕ \to s \in ℕ_{0}$
70	69	adantr	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to s \in ℕ_{0}$
71	70	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}$
72		nn0p1gt0	$⊢ s \in ℕ_{0} \to 0 < s + 1$
73	71 72	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$
74	73	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$
75		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$
76	61 66 68 74 75	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$
77	76	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$
78	77	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$
79	78	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$
80		eqeq1	$⊢ n = K \to (n = 0 \leftrightarrow K = 0)$
81	80	notbid	$⊢ n = K \to (\neg n = 0 \leftrightarrow \neg K = 0)$
82	81	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)$
83	79 82	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$
84	83	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)))))$
85	64	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 ℝ$
86		ltne	$⊢ (s + 1 \in ℝ \land s + 1 < K) \to K \neq s + 1$
87	85 86	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$
88	87	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$
89	88	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$
90		eqeq1	$⊢ n = K \to (n = s + 1 \leftrightarrow K = s + 1)$
91	90	notbid	$⊢ n = K \to (\neg n = s + 1 \leftrightarrow \neg K = s + 1)$
92	91	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)$
93	89 92	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$
94	93	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))))$
95		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$
96		breq2	$⊢ n = K \to (s + 1 < n \leftrightarrow s + 1 < K)$
97	96	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)$
98	95 97	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$
99	98	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}$
100	84 94 99	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)))))) = \underset{˙}{0}$
101		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}$
102	7	fvexi	$⊢ \underset{˙}{0} \in V$
103	102	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 \underset{˙}{0} \in V$
104	9 100 101 103	fvmptd2	$⊢ ((((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 G (K) = \underset{˙}{0}$
105	104	oveq2d	$⊢ ((((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) = (K \underset{˙}{\times} T (M)) \underset{˙}{\times} \underset{˙}{0}$
106		crngring	$⊢ R \in CRing \to R \in Ring$
107	3 4	pmatring	$⊢ (N \in Fin \land R \in Ring) \to Y \in Ring$
108	106 107	sylan2	$⊢ (N \in Fin \land R \in CRing) \to Y \in Ring$
109	108	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Ring$
110	109	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to Y \in Ring$
111	110	ad2antrr	$⊢ ((((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 Y \in Ring$
112		eqid	$⊢ {mulGrp}_{Y} = {mulGrp}_{Y}$
113	112	ringmgp	$⊢ Y \in Ring \to {mulGrp}_{Y} \in Mnd$
114	109 113	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {mulGrp}_{Y} \in Mnd$
115	114	ad2antrr	$⊢ (((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 {mulGrp}_{Y} \in Mnd$
116		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}) \to K \in ℕ_{0}$
117	8 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in {Base}_{Y}$
118	106 117	syl3an2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to T (M) \in {Base}_{Y}$
119	118	ad2antrr	$⊢ (((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 T (M) \in {Base}_{Y}$
120		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
121	112 120	mgpbas	$⊢ {Base}_{Y} = {Base}_{{mulGrp}_{Y}}$
122	121 10	mulgnn0cl	$⊢ ({mulGrp}_{Y} \in Mnd \land K \in ℕ_{0} \land T (M) \in {Base}_{Y}) \to K \underset{˙}{\times} T (M) \in {Base}_{Y}$
123	115 116 119 122	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}) \to K \underset{˙}{\times} T (M) \in {Base}_{Y}$
124	123	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 K \underset{˙}{\times} T (M) \in {Base}_{Y}$
125	120 5 7	ringrz	$⊢ (Y \in Ring \land K \underset{˙}{\times} T (M) \in {Base}_{Y}) \to (K \underset{˙}{\times} T (M)) \underset{˙}{\times} \underset{˙}{0} = \underset{˙}{0}$
126	111 124 125	syl2anc	$⊢ ((((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} \underset{˙}{0} = \underset{˙}{0}$
127	105 126	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 \underset{˙}{\times} T (M)) \underset{˙}{\times} G (K) = \underset{˙}{0}$
128	127	expl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to ((K \in ℕ_{0} \land s + 1 < K) \to (K \underset{˙}{\times} T (M)) \underset{˙}{\times} G (K) = \underset{˙}{0})$
129	60 128	syld	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (K \in ℤ_{\geq (s + 2)} \to (K \underset{˙}{\times} T (M)) \underset{˙}{\times} G (K) = \underset{˙}{0})$
130	129	3impia	$⊢ ((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}$

Metamath Proof Explorer

Theorem chfacfpmmul0

Proof