chfacfpmmulcl

Description: Closure of the value of the "characteristic factor function" multiplied with a constant polynomial matrix. (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	chfacfpmmulcl	$⊢ ((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)) \underset{˙}{\times} G (K) \in {Base}_{Y}$

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		crngring	$⊢ R \in CRing \to R \in Ring$
12	3 4	pmatring	$⊢ (N \in Fin \land R \in Ring) \to Y \in Ring$
13	11 12	sylan2	$⊢ (N \in Fin \land R \in CRing) \to Y \in Ring$
14	13	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Ring$
15	14	3ad2ant1	$⊢ ((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 Ring$
16		eqid	$⊢ {mulGrp}_{Y} = {mulGrp}_{Y}$
17		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
18	16 17	mgpbas	$⊢ {Base}_{Y} = {Base}_{{mulGrp}_{Y}}$
19	16	ringmgp	$⊢ Y \in Ring \to {mulGrp}_{Y} \in Mnd$
20	14 19	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {mulGrp}_{Y} \in Mnd$
21	20	3ad2ant1	$⊢ ((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$
22		simp3	$⊢ ((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}$
23	8 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in {Base}_{Y}$
24	11 23	syl3an2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to T (M) \in {Base}_{Y}$
25	24	3ad2ant1	$⊢ ((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}$
26	18 10 21 22 25	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} T (M) \in {Base}_{Y}$
27	1 2 3 4 5 6 7 8 9	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}$
28	11 27	syl3anl2	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to G : ℕ_{0} ⟶ {Base}_{Y}$
29	28	3adant3	$⊢ ((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 G : ℕ_{0} ⟶ {Base}_{Y}$
30	29 22	ffvelcdmd	$⊢ ((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 G (K) \in {Base}_{Y}$
31	17 5	ringcl	$⊢ (Y \in Ring \land K \underset{˙}{\times} T (M) \in {Base}_{Y} \land G (K) \in {Base}_{Y}) \to (K \underset{˙}{\times} T (M)) \underset{˙}{\times} G (K) \in {Base}_{Y}$
32	15 26 30 31	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)) \underset{˙}{\times} G (K) \in {Base}_{Y}$

Metamath Proof Explorer

Theorem chfacfpmmulcl

Proof