chfacfscmulcl

Description: Closure of a scaled value of the "characteristic factor function". (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	chfacfscmulcl	$⊢ ((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) \underset{˙}{\cdot} G (K) \in {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		chfacfscmulcl.x	$⊢ X = {var}_{1} (R)$
11		chfacfscmulcl.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
12		chfacfscmulcl.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
13		crngring	$⊢ R \in CRing \to R \in Ring$
14	3 4	pmatlmod	$⊢ (N \in Fin \land R \in Ring) \to Y \in LMod$
15	13 14	sylan2	$⊢ (N \in Fin \land R \in CRing) \to Y \in LMod$
16	15	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in LMod$
17	16	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 LMod$
18	3	ply1ring	$⊢ R \in Ring \to P \in Ring$
19	13 18	syl	$⊢ R \in CRing \to P \in Ring$
20	19	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P \in Ring$
21		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
22	21	ringmgp	$⊢ P \in Ring \to {mulGrp}_{P} \in Mnd$
23	20 22	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {mulGrp}_{P} \in Mnd$
24	23	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}_{P} \in Mnd$
25		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}$
26	13	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in Ring$
27		eqid	$⊢ {Base}_{P} = {Base}_{P}$
28	10 3 27	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
29	26 28	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to X \in {Base}_{P}$
30	29	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 X \in {Base}_{P}$
31	21 27	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{P}}$
32	31 12	mulgnn0cl	$⊢ ({mulGrp}_{P} \in Mnd \land K \in ℕ_{0} \land X \in {Base}_{P}) \to K \underset{˙}{\times} X \in {Base}_{P}$
33	24 25 30 32	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} X \in {Base}_{P}$
34	3	ply1crng	$⊢ R \in CRing \to P \in CRing$
35	34	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land P \in CRing)$
36	35	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land P \in CRing)$
37	4	matsca2	$⊢ (N \in Fin \land P \in CRing) \to P = Scalar (Y)$
38	36 37	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P = Scalar (Y)$
39	38	eqcomd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Scalar (Y) = P$
40	39	fveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {Base}_{Scalar (Y)} = {Base}_{P}$
41	40	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 {Base}_{Scalar (Y)} = {Base}_{P}$
42	33 41	eleqtrrd	$⊢ ((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)}$
43	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}$
44	13 43	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}$
45	44	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}$
46	45 25	ffvelrnd	$⊢ ((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}$
47		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
48		eqid	$⊢ Scalar (Y) = Scalar (Y)$
49		eqid	$⊢ {Base}_{Scalar (Y)} = {Base}_{Scalar (Y)}$
50	47 48 11 49	lmodvscl	$⊢ (Y \in LMod \land K \underset{˙}{\times} X \in {Base}_{Scalar (Y)} \land G (K) \in {Base}_{Y}) \to (K \underset{˙}{\times} X) \underset{˙}{\cdot} G (K) \in {Base}_{Y}$
51	17 42 46 50	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} X) \underset{˙}{\cdot} G (K) \in {Base}_{Y}$

Metamath Proof Explorer

Theorem chfacfscmulcl

Proof