Theorem 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	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	chfacfisf.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	chfacfisf.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	chfacfisf.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
	chfacfisf.r	⊢ × = ( .r ‘ 𝑌 )
	chfacfisf.s	⊢ − = ( -g ‘ 𝑌 )
	chfacfisf.0	⊢ 0 = ( 0g ‘ 𝑌 )
	chfacfisf.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	chfacfisf.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
	chfacfscmulcl.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	chfacfscmulcl.m	⊢ · = ( ·𝑠 ‘ 𝑌 )
	chfacfscmulcl.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
Assertion	chfacfscmul0	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) ) → ( ( 𝐾 ↑ 𝑋 ) · ( 𝐺 ‘ 𝐾 ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		chfacfisf.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		chfacfisf.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		chfacfisf.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4		chfacfisf.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5		chfacfisf.r	⊢ × = ( .r ‘ 𝑌 )
6		chfacfisf.s	⊢ − = ( -g ‘ 𝑌 )
7		chfacfisf.0	⊢ 0 = ( 0g ‘ 𝑌 )
8		chfacfisf.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
9		chfacfisf.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
10		chfacfscmulcl.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
11		chfacfscmulcl.m	⊢ · = ( ·𝑠 ‘ 𝑌 )
12		chfacfscmulcl.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
13		eluz2	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) ↔ ( ( 𝑠 + 2 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) )
14		simpll	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → 𝐾 ∈ ℤ )
15		nngt0	⊢ ( 𝑠 ∈ ℕ → 0 < 𝑠 )
16		nnre	⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℝ )
17	16	adantl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 𝑠 ∈ ℝ )
18		2rp	⊢ 2 ∈ ℝ+
19	18	a1i	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 2 ∈ ℝ+ )
20	17 19	ltaddrpd	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 𝑠 < ( 𝑠 + 2 ) )
21		0red	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 0 ∈ ℝ )
22		2re	⊢ 2 ∈ ℝ
23	22	a1i	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 2 ∈ ℝ )
24	17 23	readdcld	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( 𝑠 + 2 ) ∈ ℝ )
25		lttr	⊢ ( ( 0 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ ( 𝑠 + 2 ) ∈ ℝ ) → ( ( 0 < 𝑠 ∧ 𝑠 < ( 𝑠 + 2 ) ) → 0 < ( 𝑠 + 2 ) ) )
26	21 17 24 25	syl3anc	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 0 < 𝑠 ∧ 𝑠 < ( 𝑠 + 2 ) ) → 0 < ( 𝑠 + 2 ) ) )
27	20 26	mpan2d	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( 0 < 𝑠 → 0 < ( 𝑠 + 2 ) ) )
28	27	ex	⊢ ( 𝐾 ∈ ℤ → ( 𝑠 ∈ ℕ → ( 0 < 𝑠 → 0 < ( 𝑠 + 2 ) ) ) )
29	28	com13	⊢ ( 0 < 𝑠 → ( 𝑠 ∈ ℕ → ( 𝐾 ∈ ℤ → 0 < ( 𝑠 + 2 ) ) ) )
30	15 29	mpcom	⊢ ( 𝑠 ∈ ℕ → ( 𝐾 ∈ ℤ → 0 < ( 𝑠 + 2 ) ) )
31	30	impcom	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 0 < ( 𝑠 + 2 ) )
32		zre	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
33	32	adantr	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 𝐾 ∈ ℝ )
34		ltleletr	⊢ ( ( 0 ∈ ℝ ∧ ( 𝑠 + 2 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( ( 0 < ( 𝑠 + 2 ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → 0 ≤ 𝐾 ) )
35	21 24 33 34	syl3anc	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 0 < ( 𝑠 + 2 ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → 0 ≤ 𝐾 ) )
36	31 35	mpand	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑠 + 2 ) ≤ 𝐾 → 0 ≤ 𝐾 ) )
37	36	imp	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → 0 ≤ 𝐾 )
38		elnn0z	⊢ ( 𝐾 ∈ ℕ0 ↔ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) )
39	14 37 38	sylanbrc	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → 𝐾 ∈ ℕ0 )
40		nncn	⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℂ )
41		add1p1	⊢ ( 𝑠 ∈ ℂ → ( ( 𝑠 + 1 ) + 1 ) = ( 𝑠 + 2 ) )
42	40 41	syl	⊢ ( 𝑠 ∈ ℕ → ( ( 𝑠 + 1 ) + 1 ) = ( 𝑠 + 2 ) )
43	42	adantl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑠 + 1 ) + 1 ) = ( 𝑠 + 2 ) )
44	43	eqcomd	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( 𝑠 + 2 ) = ( ( 𝑠 + 1 ) + 1 ) )
45	44	breq1d	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑠 + 2 ) ≤ 𝐾 ↔ ( ( 𝑠 + 1 ) + 1 ) ≤ 𝐾 ) )
46		nnz	⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℤ )
47	46	peano2zd	⊢ ( 𝑠 ∈ ℕ → ( 𝑠 + 1 ) ∈ ℤ )
48	47	anim2i	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( 𝐾 ∈ ℤ ∧ ( 𝑠 + 1 ) ∈ ℤ ) )
49	48	ancomd	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑠 + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) )
50		zltp1le	⊢ ( ( ( 𝑠 + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑠 + 1 ) < 𝐾 ↔ ( ( 𝑠 + 1 ) + 1 ) ≤ 𝐾 ) )
51	50	bicomd	⊢ ( ( ( 𝑠 + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝑠 + 1 ) + 1 ) ≤ 𝐾 ↔ ( 𝑠 + 1 ) < 𝐾 ) )
52	49 51	syl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( ( 𝑠 + 1 ) + 1 ) ≤ 𝐾 ↔ ( 𝑠 + 1 ) < 𝐾 ) )
53	45 52	bitrd	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑠 + 2 ) ≤ 𝐾 ↔ ( 𝑠 + 1 ) < 𝐾 ) )
54	53	biimpa	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → ( 𝑠 + 1 ) < 𝐾 )
55	39 54	jca	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) )
56	55	ex	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑠 + 2 ) ≤ 𝐾 → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
57	56	impancom	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → ( 𝑠 ∈ ℕ → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
58	57	3adant1	⊢ ( ( ( 𝑠 + 2 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → ( 𝑠 ∈ ℕ → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
59	58	com12	⊢ ( 𝑠 ∈ ℕ → ( ( ( 𝑠 + 2 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
60	13 59	biimtrid	⊢ ( 𝑠 ∈ ℕ → ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
61	60	adantr	⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
62	61	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
63		0red	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 0 ∈ ℝ )
64		peano2re	⊢ ( 𝑠 ∈ ℝ → ( 𝑠 + 1 ) ∈ ℝ )
65	16 64	syl	⊢ ( 𝑠 ∈ ℕ → ( 𝑠 + 1 ) ∈ ℝ )
66	65	adantr	⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑠 + 1 ) ∈ ℝ )
67	66	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑠 + 1 ) ∈ ℝ )
68	67	ad2antrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( 𝑠 + 1 ) ∈ ℝ )
69		nn0re	⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
70	69	ad2antlr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 𝐾 ∈ ℝ )
71		nnnn0	⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℕ0 )
72	71	adantr	⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑠 ∈ ℕ0 )
73	72	ad2antlr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 𝑠 ∈ ℕ0 )
74		nn0p1gt0	⊢ ( 𝑠 ∈ ℕ0 → 0 < ( 𝑠 + 1 ) )
75	73 74	syl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 0 < ( 𝑠 + 1 ) )
76	75	adantr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 0 < ( 𝑠 + 1 ) )
77		simpr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( 𝑠 + 1 ) < 𝐾 )
78	63 68 70 76 77	lttrd	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 0 < 𝐾 )
79	78	gt0ne0d	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 𝐾 ≠ 0 )
80	79	neneqd	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ¬ 𝐾 = 0 )
81	80	adantr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ¬ 𝐾 = 0 )
82		eqeq1	⊢ ( 𝑛 = 𝐾 → ( 𝑛 = 0 ↔ 𝐾 = 0 ) )
83	82	notbid	⊢ ( 𝑛 = 𝐾 → ( ¬ 𝑛 = 0 ↔ ¬ 𝐾 = 0 ) )
84	83	adantl	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ( ¬ 𝑛 = 0 ↔ ¬ 𝐾 = 0 ) )
85	81 84	mpbird	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ¬ 𝑛 = 0 )
86	85	iffalsed	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) = if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) )
87	66	ad2antlr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑠 + 1 ) ∈ ℝ )
88		ltne	⊢ ( ( ( 𝑠 + 1 ) ∈ ℝ ∧ ( 𝑠 + 1 ) < 𝐾 ) → 𝐾 ≠ ( 𝑠 + 1 ) )
89	87 88	sylan	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 𝐾 ≠ ( 𝑠 + 1 ) )
90	89	neneqd	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ¬ 𝐾 = ( 𝑠 + 1 ) )
91	90	adantr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ¬ 𝐾 = ( 𝑠 + 1 ) )
92		eqeq1	⊢ ( 𝑛 = 𝐾 → ( 𝑛 = ( 𝑠 + 1 ) ↔ 𝐾 = ( 𝑠 + 1 ) ) )
93	92	notbid	⊢ ( 𝑛 = 𝐾 → ( ¬ 𝑛 = ( 𝑠 + 1 ) ↔ ¬ 𝐾 = ( 𝑠 + 1 ) ) )
94	93	adantl	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ( ¬ 𝑛 = ( 𝑠 + 1 ) ↔ ¬ 𝐾 = ( 𝑠 + 1 ) ) )
95	91 94	mpbird	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ¬ 𝑛 = ( 𝑠 + 1 ) )
96	95	iffalsed	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) = if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) )
97		simplr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ( 𝑠 + 1 ) < 𝐾 )
98		breq2	⊢ ( 𝑛 = 𝐾 → ( ( 𝑠 + 1 ) < 𝑛 ↔ ( 𝑠 + 1 ) < 𝐾 ) )
99	98	adantl	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ( ( 𝑠 + 1 ) < 𝑛 ↔ ( 𝑠 + 1 ) < 𝐾 ) )
100	97 99	mpbird	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ( 𝑠 + 1 ) < 𝑛 )
101	100	iftrued	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) = 0 )
102	86 96 101	3eqtrd	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) = 0 )
103		simplr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 𝐾 ∈ ℕ0 )
104	7	fvexi	⊢ 0 ∈ V
105	104	a1i	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 0 ∈ V )
106	9 102 103 105	fvmptd2	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( 𝐺 ‘ 𝐾 ) = 0 )
107	106	oveq2d	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( ( 𝐾 ↑ 𝑋 ) · ( 𝐺 ‘ 𝐾 ) ) = ( ( 𝐾 ↑ 𝑋 ) · 0 ) )
108		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
109	3 4	pmatlmod	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ LMod )
110	108 109	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ LMod )
111	110	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ LMod )
112	111	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 𝑌 ∈ LMod )
113		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
114		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
115	113 114	mgpbas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
116	3	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
117	108 116	syl	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
118	117	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ Ring )
119	113	ringmgp	⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
120	118 119	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
121	120	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
122		simpr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℕ0 )
123	108	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
124	10 3 114	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
125	123 124	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
126	125	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
127	115 12 121 122 126	mulgnn0cld	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
128	3	ply1crng	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
129	128	anim2i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) )
130	129	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) )
131	4	matsca2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
132	130 131	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
133	132	eqcomd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Scalar ‘ 𝑌 ) = 𝑃 )
134	133	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ 𝑃 ) )
135	134	eleq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ↔ ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) )
136	135	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ↔ ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) )
137	127 136	mpbird	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
138	112 137	jca	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑌 ∈ LMod ∧ ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ) )
139	138	adantr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( 𝑌 ∈ LMod ∧ ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ) )
140		eqid	⊢ ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑌 )
141		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ ( Scalar ‘ 𝑌 ) )
142	140 11 141 7	lmodvs0	⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ) → ( ( 𝐾 ↑ 𝑋 ) · 0 ) = 0 )
143	139 142	syl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( ( 𝐾 ↑ 𝑋 ) · 0 ) = 0 )
144	107 143	eqtrd	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( ( 𝐾 ↑ 𝑋 ) · ( 𝐺 ‘ 𝐾 ) ) = 0 )
145	144	expl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( ( 𝐾 ↑ 𝑋 ) · ( 𝐺 ‘ 𝐾 ) ) = 0 ) )
146	62 145	syld	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) → ( ( 𝐾 ↑ 𝑋 ) · ( 𝐺 ‘ 𝐾 ) ) = 0 ) )
147	146	3impia	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) ) → ( ( 𝐾 ↑ 𝑋 ) · ( 𝐺 ‘ 𝐾 ) ) = 0 )