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		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
19		eqid	$⊢ {Base}_{P} = {Base}_{P}$
20	18 19	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{P}}$
21	3	ply1ring	$⊢ R \in Ring \to P \in Ring$
22	13 21	syl	$⊢ R \in CRing \to P \in Ring$
23	22	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P \in Ring$
24	18	ringmgp	$⊢ P \in Ring \to {mulGrp}_{P} \in Mnd$
25	23 24	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {mulGrp}_{P} \in Mnd$
26	25	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$
27		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}$
28	13	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in Ring$
29	10 3 19	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
30	28 29	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to X \in {Base}_{P}$
31	30	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}$
32	20 12 26 27 31	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} X \in {Base}_{P}$
33	3	ply1crng	$⊢ R \in CRing \to P \in CRing$
34	33	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land P \in CRing)$
35	34	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land P \in CRing)$
36	4	matsca2	$⊢ (N \in Fin \land P \in CRing) \to P = Scalar (Y)$
37	35 36	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P = Scalar (Y)$
38	37	eqcomd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Scalar (Y) = P$
39	38	fveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {Base}_{Scalar (Y)} = {Base}_{P}$
40	39	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}$
41	32 40	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)}$
42	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}$
43	13 42	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}$
44	43	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}$
45	44 27	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}$
46		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
47		eqid	$⊢ Scalar (Y) = Scalar (Y)$
48		eqid	$⊢ {Base}_{Scalar (Y)} = {Base}_{Scalar (Y)}$
49	46 47 11 48	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}$
50	17 41 45 49	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