chfacfisfcpmat

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

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		chfacfisfcpmat.s	$⊢ S = N ConstPolyMat R$
11	10 3 4	cpmatsubgpmat	$⊢ (N \in Fin \land R \in Ring) \to S \in SubGrp (Y)$
12	11	3adant3	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to S \in SubGrp (Y)$
13	12	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to S \in SubGrp (Y)$
14		subgsubm	$⊢ S \in SubGrp (Y) \to S \in SubMnd (Y)$
15	7	subm0cl	$⊢ S \in SubMnd (Y) \to \underset{˙}{0} \in S$
16	12 14 15	3syl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \underset{˙}{0} \in S$
17	16	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 S$
18	10 3 4	cpmatsrgpmat	$⊢ (N \in Fin \land R \in Ring) \to S \in SubRing (Y)$
19	18	3adant3	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to S \in SubRing (Y)$
20	19	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to S \in SubRing (Y)$
21	10 8 1 2	m2cpm	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in S$
22	21	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 S$
23		3simpa	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (N \in Fin \land R \in Ring)$
24		elmapi	$⊢ b \in (B^{(0 \dots s)}) \to b : (0 \dots s) ⟶ B$
25	24	adantl	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to b : (0 \dots s) ⟶ B$
26		nnnn0	$⊢ s \in ℕ \to s \in ℕ_{0}$
27		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
28	26 27	eleqtrdi	$⊢ s \in ℕ \to s \in ℤ_{\geq 0}$
29		eluzfz1	$⊢ s \in ℤ_{\geq 0} \to 0 \in (0 \dots s)$
30	28 29	syl	$⊢ s \in ℕ \to 0 \in (0 \dots s)$
31	30	adantr	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to 0 \in (0 \dots s)$
32	25 31	ffvelrnd	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to b (0) \in B$
33	23 32	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)$
34		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)$
35	33 34	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)$
36	10 8 1 2	m2cpm	$⊢ (N \in Fin \land R \in Ring \land b (0) \in B) \to T (b (0)) \in S$
37	35 36	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 S$
38	5	subrgmcl	$⊢ (S \in SubRing (Y) \land T (M) \in S \land T (b (0)) \in S) \to T (M) \underset{˙}{\times} T (b (0)) \in S$
39	20 22 37 38	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 S$
40	6	subgsubcl	$⊢ (S \in SubGrp (Y) \land \underset{˙}{0} \in S \land T (M) \underset{˙}{\times} T (b (0)) \in S) \to \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))) \in S$
41	13 17 39 40	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 S$
42	41	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 S$
43		simpl1	$⊢ ((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$
44		simpl2	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to R \in Ring$
45	25	adantl	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to b : (0 \dots s) ⟶ B$
46		eluzfz2	$⊢ s \in ℤ_{\geq 0} \to s \in (0 \dots s)$
47	28 46	syl	$⊢ s \in ℕ \to s \in (0 \dots s)$
48	47	ad2antrl	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to s \in (0 \dots s)$
49	45 48	ffvelrnd	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to b (s) \in B$
50	10 8 1 2	m2cpm	$⊢ (N \in Fin \land R \in Ring \land b (s) \in B) \to T (b (s)) \in S$
51	43 44 49 50	syl3anc	$⊢ ((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 S$
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 S$
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 S$
54	17	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 S$
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	syl5bir	$⊢ (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	12	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 S \in SubGrp (Y)$
75	23	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)$
76	25	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$
77		neqne	$⊢ \neg n = 0 \to n \neq 0$
78	77	anim2i	$⊢ (n \in ℕ_{0} \land \neg n = 0) \to (n \in ℕ_{0} \land n \neq 0)$
79		elnnne0	$⊢ n \in ℕ \leftrightarrow (n \in ℕ_{0} \land n \neq 0)$
80	78 79	sylibr	$⊢ (n \in ℕ_{0} \land \neg n = 0) \to n \in ℕ$
81		nnm1nn0	$⊢ n \in ℕ \to n - 1 \in ℕ_{0}$
82	80 81	syl	$⊢ (n \in ℕ_{0} \land \neg n = 0) \to n - 1 \in ℕ_{0}$
83	82	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}$
84	26	adantr	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to s \in ℕ_{0}$
85	84	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}$
86	63	simprbda	$⊢ ((s \in ℕ \land n \in ℕ_{0}) \land n < s + 1) \to n \leq s + 1$
87	56	adantr	$⊢ ((s \in ℕ \land n \in ℕ_{0}) \land n < s + 1) \to n \in ℝ$
88		1red	$⊢ ((s \in ℕ \land n \in ℕ_{0}) \land n < s + 1) \to 1 \in ℝ$
89		nnre	$⊢ s \in ℕ \to s \in ℝ$
90	89	ad2antrr	$⊢ ((s \in ℕ \land n \in ℕ_{0}) \land n < s + 1) \to s \in ℝ$
91	87 88 90	lesubaddd	$⊢ ((s \in ℕ \land n \in ℕ_{0}) \land n < s + 1) \to (n - 1 \leq s \leftrightarrow n \leq s + 1)$
92	86 91	mpbird	$⊢ ((s \in ℕ \land n \in ℕ_{0}) \land n < s + 1) \to n - 1 \leq s$
93	92	exp31	$⊢ s \in ℕ \to (n \in ℕ_{0} \to (n < s + 1 \to n - 1 \leq s))$
94	93	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))$
95	94	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)$
96	95	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)$
97	96	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$
98		elfz2nn0	$⊢ n - 1 \in (0 \dots s) \leftrightarrow (n - 1 \in ℕ_{0} \land s \in ℕ_{0} \land n - 1 \leq s)$
99	83 85 97 98	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)$
100	76 99	ffvelrnd	$⊢ (((((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$
101		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)$
102	75 100 101	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)$
103	10 8 1 2	m2cpm	$⊢ (N \in Fin \land R \in Ring \land b (n - 1) \in B) \to T (b (n - 1)) \in S$
104	102 103	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 S$
105	20	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 S \in SubRing (Y)$
106	22	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 S$
107	23 84	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})$
108		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})$
109	107 108	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})$
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 (N \in Fin \land R \in Ring \land s \in ℕ_{0})$
111	110	simp1d	$⊢ ((((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$
112	110	simp2d	$⊢ ((((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 R \in Ring$
113	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 b : (0 \dots s) ⟶ B$
114		simplr	$⊢ ((s \in ℕ \land n \in ℕ_{0}) \land n < s + 1) \to n \in ℕ_{0}$
115	26	ad2antrr	$⊢ ((s \in ℕ \land n \in ℕ_{0}) \land n < s + 1) \to s \in ℕ_{0}$
116		nn0z	$⊢ n \in ℕ_{0} \to n \in ℤ$
117		nnz	$⊢ s \in ℕ \to s \in ℤ$
118		zleltp1	$⊢ (n \in ℤ \land s \in ℤ) \to (n \leq s \leftrightarrow n < s + 1)$
119	116 117 118	syl2anr	$⊢ (s \in ℕ \land n \in ℕ_{0}) \to (n \leq s \leftrightarrow n < s + 1)$
120	119	biimpar	$⊢ ((s \in ℕ \land n \in ℕ_{0}) \land n < s + 1) \to n \leq s$
121		elfz2nn0	$⊢ n \in (0 \dots s) \leftrightarrow (n \in ℕ_{0} \land s \in ℕ_{0} \land n \leq s)$
122	114 115 120 121	syl3anbrc	$⊢ ((s \in ℕ \land n \in ℕ_{0}) \land n < s + 1) \to n \in (0 \dots s)$
123	122	exp31	$⊢ s \in ℕ \to (n \in ℕ_{0} \to (n < s + 1 \to n \in (0 \dots s)))$
124	123	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)))$
125	124	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)$
126	113 125	ffvelrnd	$⊢ ((((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 (n) \in B$
127	10 8 1 2	m2cpm	$⊢ (N \in Fin \land R \in Ring \land b (n) \in B) \to T (b (n)) \in S$
128	111 112 126 127	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 (b (n)) \in S$
129	5	subrgmcl	$⊢ (S \in SubRing (Y) \land T (M) \in S \land T (b (n)) \in S) \to T (M) \underset{˙}{\times} T (b (n)) \in S$
130	105 106 128 129	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 S$
131	130	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 S$
132	6	subgsubcl	$⊢ (S \in SubGrp (Y) \land T (b (n - 1)) \in S \land T (M) \underset{˙}{\times} T (b (n)) \in S) \to T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n))) \in S$
133	74 104 131 132	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 S$
134	133	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 S)$
135	73 134	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 S)$
136	135	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 S$
137	54 136	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 S$
138	53 137	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 S$
139	42 138	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 S$
140	139 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} ⟶ S$

Metamath Proof Explorer

Theorem chfacfisfcpmat

Proof