chfacfisf

Description: The "characteristic factor function" is a function from the nonnegative integers to polynomial matrices. (Contributed by AV, 8-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)))))))$
Assertion	chfacfisf	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to G : ℕ_{0} ⟶ {Base}_{Y}$

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	3 4	pmatring	$⊢ (N \in Fin \land R \in Ring) \to Y \in Ring$
11	10	3adant3	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to Y \in Ring$
12		ringgrp	$⊢ Y \in Ring \to Y \in Grp$
13	11 12	syl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to Y \in Grp$
14	13	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to Y \in Grp$
15		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
16	15 7	ring0cl	$⊢ Y \in Ring \to \underset{˙}{0} \in {Base}_{Y}$
17	11 16	syl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \underset{˙}{0} \in {Base}_{Y}$
18	17	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \underset{˙}{0} \in {Base}_{Y}$
19	11	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to Y \in Ring$
20	8 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in {Base}_{Y}$
21	20	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to T (M) \in {Base}_{Y}$
22		3simpa	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (N \in Fin \land R \in Ring)$
23		elmapi	$⊢ b \in (B^{(0 \dots s)}) \to b : (0 \dots s) ⟶ B$
24	23	adantl	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to b : (0 \dots s) ⟶ B$
25		nnnn0	$⊢ s \in ℕ \to s \in ℕ_{0}$
26		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
27	25 26	eleqtrdi	$⊢ s \in ℕ \to s \in ℤ_{\geq 0}$
28		eluzfz1	$⊢ s \in ℤ_{\geq 0} \to 0 \in (0 \dots s)$
29	27 28	syl	$⊢ s \in ℕ \to 0 \in (0 \dots s)$
30	29	adantr	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to 0 \in (0 \dots s)$
31	24 30	ffvelcdmd	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to b (0) \in B$
32	22 31	anim12i	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to ((N \in Fin \land R \in Ring) \land b (0) \in B)$
33		df-3an	$⊢ (N \in Fin \land R \in Ring \land b (0) \in B) \leftrightarrow ((N \in Fin \land R \in Ring) \land b (0) \in B)$
34	32 33	sylibr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (N \in Fin \land R \in Ring \land b (0) \in B)$
35	8 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land b (0) \in B) \to T (b (0)) \in {Base}_{Y}$
36	34 35	syl	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to T (b (0)) \in {Base}_{Y}$
37	15 5	ringcl	$⊢ (Y \in Ring \land T (M) \in {Base}_{Y} \land T (b (0)) \in {Base}_{Y}) \to T (M) \underset{˙}{\times} T (b (0)) \in {Base}_{Y}$
38	19 21 36 37	syl3anc	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to T (M) \underset{˙}{\times} T (b (0)) \in {Base}_{Y}$
39	15 6	grpsubcl	$⊢ (Y \in Grp \land \underset{˙}{0} \in {Base}_{Y} \land T (M) \underset{˙}{\times} T (b (0)) \in {Base}_{Y}) \to \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))) \in {Base}_{Y}$
40	14 18 38 39	syl3anc	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))) \in {Base}_{Y}$
41	40	ad2antrr	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land n = 0) \to \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))) \in {Base}_{Y}$
42	25	adantr	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to s \in ℕ_{0}$
43	22 42	anim12i	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to ((N \in Fin \land R \in Ring) \land s \in ℕ_{0})$
44		df-3an	$⊢ (N \in Fin \land R \in Ring \land s \in ℕ_{0}) \leftrightarrow ((N \in Fin \land R \in Ring) \land s \in ℕ_{0})$
45	43 44	sylibr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (N \in Fin \land R \in Ring \land s \in ℕ_{0})$
46		eluzfz2	$⊢ s \in ℤ_{\geq 0} \to s \in (0 \dots s)$
47	27 46	syl	$⊢ s \in ℕ \to s \in (0 \dots s)$
48	47	anim1ci	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to (b \in (B^{(0 \dots s)}) \land s \in (0 \dots s))$
49	48	adantl	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (b \in (B^{(0 \dots s)}) \land s \in (0 \dots s))$
50	1 2 3 4 8	m2pmfzmap	$⊢ ((N \in Fin \land R \in Ring \land s \in ℕ_{0}) \land (b \in (B^{(0 \dots s)}) \land s \in (0 \dots s))) \to T (b (s)) \in {Base}_{Y}$
51	45 49 50	syl2anc	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to T (b (s)) \in {Base}_{Y}$
52	51	adantr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \to T (b (s)) \in {Base}_{Y}$
53	52	ad2antrr	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \land n = s + 1) \to T (b (s)) \in {Base}_{Y}$
54	18	ad4antr	$⊢ ((((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \land \neg n = s + 1) \land s + 1 < n) \to \underset{˙}{0} \in {Base}_{Y}$
55		nn0re	$⊢ n \in ℕ_{0} \to n \in ℝ$
56	55	adantl	$⊢ (s \in ℕ \land n \in ℕ_{0}) \to n \in ℝ$
57		peano2nn	$⊢ s \in ℕ \to s + 1 \in ℕ$
58	57	nnred	$⊢ s \in ℕ \to s + 1 \in ℝ$
59	58	adantr	$⊢ (s \in ℕ \land n \in ℕ_{0}) \to s + 1 \in ℝ$
60	56 59	lenltd	$⊢ (s \in ℕ \land n \in ℕ_{0}) \to (n \leq s + 1 \leftrightarrow \neg s + 1 < n)$
61		nesym	$⊢ s + 1 \neq n \leftrightarrow \neg n = s + 1$
62		ltlen	$⊢ (n \in ℝ \land s + 1 \in ℝ) \to (n < s + 1 \leftrightarrow (n \leq s + 1 \land s + 1 \neq n))$
63	55 58 62	syl2anr	$⊢ (s \in ℕ \land n \in ℕ_{0}) \to (n < s + 1 \leftrightarrow (n \leq s + 1 \land s + 1 \neq n))$
64	63	biimprd	$⊢ (s \in ℕ \land n \in ℕ_{0}) \to ((n \leq s + 1 \land s + 1 \neq n) \to n < s + 1)$
65	64	expcomd	$⊢ (s \in ℕ \land n \in ℕ_{0}) \to (s + 1 \neq n \to (n \leq s + 1 \to n < s + 1))$
66	61 65	biimtrrid	$⊢ (s \in ℕ \land n \in ℕ_{0}) \to (\neg n = s + 1 \to (n \leq s + 1 \to n < s + 1))$
67	66	com23	$⊢ (s \in ℕ \land n \in ℕ_{0}) \to (n \leq s + 1 \to (\neg n = s + 1 \to n < s + 1))$
68	60 67	sylbird	$⊢ (s \in ℕ \land n \in ℕ_{0}) \to (\neg s + 1 < n \to (\neg n = s + 1 \to n < s + 1))$
69	68	impcomd	$⊢ (s \in ℕ \land n \in ℕ_{0}) \to ((\neg n = s + 1 \land \neg s + 1 < n) \to n < s + 1)$
70	69	ex	$⊢ s \in ℕ \to (n \in ℕ_{0} \to ((\neg n = s + 1 \land \neg s + 1 < n) \to n < s + 1))$
71	70	ad2antrl	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (n \in ℕ_{0} \to ((\neg n = s + 1 \land \neg s + 1 < n) \to n < s + 1))$
72	71	imp	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \to ((\neg n = s + 1 \land \neg s + 1 < n) \to n < s + 1)$
73	72	adantr	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \to ((\neg n = s + 1 \land \neg s + 1 < n) \to n < s + 1)$
74	10 12	syl	$⊢ (N \in Fin \land R \in Ring) \to Y \in Grp$
75	74	3adant3	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to Y \in Grp$
76	75	ad4antr	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \land n < s + 1) \to Y \in Grp$
77	22	ad4antr	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \land n < s + 1) \to (N \in Fin \land R \in Ring)$
78	24	ad4antlr	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \land n < s + 1) \to b : (0 \dots s) ⟶ B$
79		neqne	$⊢ \neg n = 0 \to n \neq 0$
80	79	anim2i	$⊢ (n \in ℕ_{0} \land \neg n = 0) \to (n \in ℕ_{0} \land n \neq 0)$
81		elnnne0	$⊢ n \in ℕ \leftrightarrow (n \in ℕ_{0} \land n \neq 0)$
82	80 81	sylibr	$⊢ (n \in ℕ_{0} \land \neg n = 0) \to n \in ℕ$
83		nnm1nn0	$⊢ n \in ℕ \to n - 1 \in ℕ_{0}$
84	82 83	syl	$⊢ (n \in ℕ_{0} \land \neg n = 0) \to n - 1 \in ℕ_{0}$
85	84	ad4ant23	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \land n < s + 1) \to n - 1 \in ℕ_{0}$
86	42	ad4antlr	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \land n < s + 1) \to s \in ℕ_{0}$
87	63	simprbda	$⊢ ((s \in ℕ \land n \in ℕ_{0}) \land n < s + 1) \to n \leq s + 1$
88	56	adantr	$⊢ ((s \in ℕ \land n \in ℕ_{0}) \land n < s + 1) \to n \in ℝ$
89		1red	$⊢ ((s \in ℕ \land n \in ℕ_{0}) \land n < s + 1) \to 1 \in ℝ$
90		nnre	$⊢ s \in ℕ \to s \in ℝ$
91	90	ad2antrr	$⊢ ((s \in ℕ \land n \in ℕ_{0}) \land n < s + 1) \to s \in ℝ$
92	88 89 91	lesubaddd	$⊢ ((s \in ℕ \land n \in ℕ_{0}) \land n < s + 1) \to (n - 1 \leq s \leftrightarrow n \leq s + 1)$
93	87 92	mpbird	$⊢ ((s \in ℕ \land n \in ℕ_{0}) \land n < s + 1) \to n - 1 \leq s$
94	93	exp31	$⊢ s \in ℕ \to (n \in ℕ_{0} \to (n < s + 1 \to n - 1 \leq s))$
95	94	ad2antrl	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (n \in ℕ_{0} \to (n < s + 1 \to n - 1 \leq s))$
96	95	imp	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \to (n < s + 1 \to n - 1 \leq s)$
97	96	adantr	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \to (n < s + 1 \to n - 1 \leq s)$
98	97	imp	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \land n < s + 1) \to n - 1 \leq s$
99		elfz2nn0	$⊢ n - 1 \in (0 \dots s) \leftrightarrow (n - 1 \in ℕ_{0} \land s \in ℕ_{0} \land n - 1 \leq s)$
100	85 86 98 99	syl3anbrc	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \land n < s + 1) \to n - 1 \in (0 \dots s)$
101	78 100	ffvelcdmd	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \land n < s + 1) \to b (n - 1) \in B$
102		df-3an	$⊢ (N \in Fin \land R \in Ring \land b (n - 1) \in B) \leftrightarrow ((N \in Fin \land R \in Ring) \land b (n - 1) \in B)$
103	77 101 102	sylanbrc	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \land n < s + 1) \to (N \in Fin \land R \in Ring \land b (n - 1) \in B)$
104	8 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land b (n - 1) \in B) \to T (b (n - 1)) \in {Base}_{Y}$
105	103 104	syl	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \land n < s + 1) \to T (b (n - 1)) \in {Base}_{Y}$
106	19	ad2antrr	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land n < s + 1) \to Y \in Ring$
107	21	ad2antrr	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land n < s + 1) \to T (M) \in {Base}_{Y}$
108	45	ad2antrr	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land n < s + 1) \to (N \in Fin \land R \in Ring \land s \in ℕ_{0})$
109		simprr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to b \in (B^{(0 \dots s)})$
110	109	ad2antrr	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land n < s + 1) \to b \in (B^{(0 \dots s)})$
111		simplr	$⊢ ((s \in ℕ \land n \in ℕ_{0}) \land n < s + 1) \to n \in ℕ_{0}$
112	25	ad2antrr	$⊢ ((s \in ℕ \land n \in ℕ_{0}) \land n < s + 1) \to s \in ℕ_{0}$
113		nn0z	$⊢ n \in ℕ_{0} \to n \in ℤ$
114		nnz	$⊢ s \in ℕ \to s \in ℤ$
115		zleltp1	$⊢ (n \in ℤ \land s \in ℤ) \to (n \leq s \leftrightarrow n < s + 1)$
116	113 114 115	syl2anr	$⊢ (s \in ℕ \land n \in ℕ_{0}) \to (n \leq s \leftrightarrow n < s + 1)$
117	116	biimpar	$⊢ ((s \in ℕ \land n \in ℕ_{0}) \land n < s + 1) \to n \leq s$
118		elfz2nn0	$⊢ n \in (0 \dots s) \leftrightarrow (n \in ℕ_{0} \land s \in ℕ_{0} \land n \leq s)$
119	111 112 117 118	syl3anbrc	$⊢ ((s \in ℕ \land n \in ℕ_{0}) \land n < s + 1) \to n \in (0 \dots s)$
120	119	exp31	$⊢ s \in ℕ \to (n \in ℕ_{0} \to (n < s + 1 \to n \in (0 \dots s)))$
121	120	ad2antrl	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (n \in ℕ_{0} \to (n < s + 1 \to n \in (0 \dots s)))$
122	121	imp31	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land n < s + 1) \to n \in (0 \dots s)$
123	1 2 3 4 8	m2pmfzmap	$⊢ ((N \in Fin \land R \in Ring \land s \in ℕ_{0}) \land (b \in (B^{(0 \dots s)}) \land n \in (0 \dots s))) \to T (b (n)) \in {Base}_{Y}$
124	108 110 122 123	syl12anc	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land n < s + 1) \to T (b (n)) \in {Base}_{Y}$
125	15 5	ringcl	$⊢ (Y \in Ring \land T (M) \in {Base}_{Y} \land T (b (n)) \in {Base}_{Y}) \to T (M) \underset{˙}{\times} T (b (n)) \in {Base}_{Y}$
126	106 107 124 125	syl3anc	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land n < s + 1) \to T (M) \underset{˙}{\times} T (b (n)) \in {Base}_{Y}$
127	126	adantlr	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \land n < s + 1) \to T (M) \underset{˙}{\times} T (b (n)) \in {Base}_{Y}$
128	15 6	grpsubcl	$⊢ (Y \in Grp \land T (b (n - 1)) \in {Base}_{Y} \land T (M) \underset{˙}{\times} T (b (n)) \in {Base}_{Y}) \to T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n))) \in {Base}_{Y}$
129	76 105 127 128	syl3anc	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \land n < s + 1) \to T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n))) \in {Base}_{Y}$
130	129	ex	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \to (n < s + 1 \to T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n))) \in {Base}_{Y})$
131	73 130	syld	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \to ((\neg n = s + 1 \land \neg s + 1 < n) \to T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n))) \in {Base}_{Y})$
132	131	impl	$⊢ ((((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \land \neg n = s + 1) \land \neg s + 1 < n) \to T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n))) \in {Base}_{Y}$
133	54 132	ifclda	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \land \neg n = s + 1) \to if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n)))) \in {Base}_{Y}$
134	53 133	ifclda	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \land \neg n = 0) \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))))) \in {Base}_{Y}$
135	41 134	ifclda	$⊢ (((N \in Fin \land R \in Ring \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 {Base}_{Y}$
136	135 9	fmptd	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to G : ℕ_{0} ⟶ {Base}_{Y}$

Metamath Proof Explorer

Theorem chfacfisf

Proof