chfacfscmul0

Description: A scaled value of the "characteristic factor function" is zero almost always. (Contributed by AV, 9-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	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}$

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

Metamath Proof Explorer

Theorem chfacfscmul0

Proof