evls1fpws

Description: Evaluation of a univariate subring polynomial as a function in a power series. (Contributed by Thierry Arnoux, 23-Jan-2025)

	Ref	Expression
Hypotheses	ressply1evl.q	$⊢ Q = S {evalSub}_{1} R$
	ressply1evl.k	$⊢ K = {Base}_{S}$
	ressply1evl.w	$⊢ W = {Poly}_{1} (U)$
	ressply1evl.u	$⊢ U = S ↾_{𝑠} R$
	ressply1evl.b	$⊢ B = {Base}_{W}$
	evls1fpws.s	$⊢ φ \to S \in CRing$
	evls1fpws.r	$⊢ φ \to R \in SubRing (S)$
	evls1fpws.y	$⊢ φ \to M \in B$
	evls1fpws.1	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
	evls1fpws.2	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{S}}$
	evls1fpws.a	$⊢ A = {coe}_{1} (M)$
Assertion	evls1fpws	$⊢ φ \to Q (M) = (x \in K ⟼ \underset{k \in ℕ_{0}}{\sum_{S}} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x)))$

Proof

Step	Hyp	Ref	Expression
1		ressply1evl.q	$⊢ Q = S {evalSub}_{1} R$
2		ressply1evl.k	$⊢ K = {Base}_{S}$
3		ressply1evl.w	$⊢ W = {Poly}_{1} (U)$
4		ressply1evl.u	$⊢ U = S ↾_{𝑠} R$
5		ressply1evl.b	$⊢ B = {Base}_{W}$
6		evls1fpws.s	$⊢ φ \to S \in CRing$
7		evls1fpws.r	$⊢ φ \to R \in SubRing (S)$
8		evls1fpws.y	$⊢ φ \to M \in B$
9		evls1fpws.1	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
10		evls1fpws.2	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{S}}$
11		evls1fpws.a	$⊢ A = {coe}_{1} (M)$
12	4	subrgring	$⊢ R \in SubRing (S) \to U \in Ring$
13	7 12	syl	$⊢ φ \to U \in Ring$
14		eqid	$⊢ {var}_{1} (U) = {var}_{1} (U)$
15		eqid	$⊢ \cdot_{W} = \cdot_{W}$
16		eqid	$⊢ {mulGrp}_{W} = {mulGrp}_{W}$
17		eqid	$⊢ \cdot_{{mulGrp}_{W}} = \cdot_{{mulGrp}_{W}}$
18	3 14 5 15 16 17 11	ply1coe	$⊢ (U \in Ring \land M \in B) \to M = \underset{k \in ℕ_{0}}{\sum_{W}} (A (k) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U)))$
19	13 8 18	syl2anc	$⊢ φ \to M = \underset{k \in ℕ_{0}}{\sum_{W}} (A (k) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U)))$
20	19	fveq2d	$⊢ φ \to Q (M) = Q (\underset{k \in ℕ_{0}}{\sum_{W}} (A (k) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U))))$
21		eqid	$⊢ 0_{W} = 0_{W}$
22		eqid	$⊢ S ↑_{𝑠} K = S ↑_{𝑠} K$
23	3	ply1lmod	$⊢ U \in Ring \to W \in LMod$
24	13 23	syl	$⊢ φ \to W \in LMod$
25	24	adantr	$⊢ (φ \land k \in ℕ_{0}) \to W \in LMod$
26		eqid	$⊢ {Base}_{U} = {Base}_{U}$
27	11 5 3 26	coe1fvalcl	$⊢ (M \in B \land k \in ℕ_{0}) \to A (k) \in {Base}_{U}$
28	8 27	sylan	$⊢ (φ \land k \in ℕ_{0}) \to A (k) \in {Base}_{U}$
29	3	ply1sca	$⊢ U \in Ring \to U = Scalar (W)$
30	13 29	syl	$⊢ φ \to U = Scalar (W)$
31	30	fveq2d	$⊢ φ \to {Base}_{U} = {Base}_{Scalar (W)}$
32	31	adantr	$⊢ (φ \land k \in ℕ_{0}) \to {Base}_{U} = {Base}_{Scalar (W)}$
33	28 32	eleqtrd	$⊢ (φ \land k \in ℕ_{0}) \to A (k) \in {Base}_{Scalar (W)}$
34	16 5	mgpbas	$⊢ B = {Base}_{{mulGrp}_{W}}$
35	3	ply1ring	$⊢ U \in Ring \to W \in Ring$
36	13 35	syl	$⊢ φ \to W \in Ring$
37	36	adantr	$⊢ (φ \land k \in ℕ_{0}) \to W \in Ring$
38	16	ringmgp	$⊢ W \in Ring \to {mulGrp}_{W} \in Mnd$
39	37 38	syl	$⊢ (φ \land k \in ℕ_{0}) \to {mulGrp}_{W} \in Mnd$
40		simpr	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℕ_{0}$
41	13	adantr	$⊢ (φ \land k \in ℕ_{0}) \to U \in Ring$
42	14 3 5	vr1cl	$⊢ U \in Ring \to {var}_{1} (U) \in B$
43	41 42	syl	$⊢ (φ \land k \in ℕ_{0}) \to {var}_{1} (U) \in B$
44	34 17 39 40 43	mulgnn0cld	$⊢ (φ \land k \in ℕ_{0}) \to k \cdot_{{mulGrp}_{W}} {var}_{1} (U) \in B$
45		eqid	$⊢ Scalar (W) = Scalar (W)$
46		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
47	5 45 15 46	lmodvscl	$⊢ (W \in LMod \land A (k) \in {Base}_{Scalar (W)} \land k \cdot_{{mulGrp}_{W}} {var}_{1} (U) \in B) \to A (k) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U)) \in B$
48	25 33 44 47	syl3anc	$⊢ (φ \land k \in ℕ_{0}) \to A (k) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U)) \in B$
49		ssidd	$⊢ φ \to ℕ_{0} \subseteq ℕ_{0}$
50		fvexd	$⊢ φ \to 0_{W} \in V$
51		fveq2	$⊢ k = j \to A (k) = A (j)$
52		oveq1	$⊢ k = j \to k \cdot_{{mulGrp}_{W}} {var}_{1} (U) = j \cdot_{{mulGrp}_{W}} {var}_{1} (U)$
53	51 52	oveq12d	$⊢ k = j \to A (k) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U)) = A (j) \cdot_{W} (j \cdot_{{mulGrp}_{W}} {var}_{1} (U))$
54		eqid	$⊢ 0_{U} = 0_{U}$
55	11 5 3 54	coe1ae0	$⊢ M \in B \to \exists i \in ℕ_{0} \forall j \in ℕ_{0} (i < j \to A (j) = 0_{U})$
56	8 55	syl	$⊢ φ \to \exists i \in ℕ_{0} \forall j \in ℕ_{0} (i < j \to A (j) = 0_{U})$
57		simpr	$⊢ (((φ \land i \in ℕ_{0}) \land j \in ℕ_{0}) \land A (j) = 0_{U}) \to A (j) = 0_{U}$
58	30	ad3antrrr	$⊢ (((φ \land i \in ℕ_{0}) \land j \in ℕ_{0}) \land A (j) = 0_{U}) \to U = Scalar (W)$
59	58	fveq2d	$⊢ (((φ \land i \in ℕ_{0}) \land j \in ℕ_{0}) \land A (j) = 0_{U}) \to 0_{U} = 0_{Scalar (W)}$
60	57 59	eqtrd	$⊢ (((φ \land i \in ℕ_{0}) \land j \in ℕ_{0}) \land A (j) = 0_{U}) \to A (j) = 0_{Scalar (W)}$
61	60	oveq1d	$⊢ (((φ \land i \in ℕ_{0}) \land j \in ℕ_{0}) \land A (j) = 0_{U}) \to A (j) \cdot_{W} (j \cdot_{{mulGrp}_{W}} {var}_{1} (U)) = 0_{Scalar (W)} \cdot_{W} (j \cdot_{{mulGrp}_{W}} {var}_{1} (U))$
62	24	ad3antrrr	$⊢ (((φ \land i \in ℕ_{0}) \land j \in ℕ_{0}) \land A (j) = 0_{U}) \to W \in LMod$
63	36 38	syl	$⊢ φ \to {mulGrp}_{W} \in Mnd$
64	63	adantr	$⊢ (φ \land j \in ℕ_{0}) \to {mulGrp}_{W} \in Mnd$
65		simpr	$⊢ (φ \land j \in ℕ_{0}) \to j \in ℕ_{0}$
66	13 42	syl	$⊢ φ \to {var}_{1} (U) \in B$
67	66	adantr	$⊢ (φ \land j \in ℕ_{0}) \to {var}_{1} (U) \in B$
68	34 17 64 65 67	mulgnn0cld	$⊢ (φ \land j \in ℕ_{0}) \to j \cdot_{{mulGrp}_{W}} {var}_{1} (U) \in B$
69	68	ad4ant13	$⊢ (((φ \land i \in ℕ_{0}) \land j \in ℕ_{0}) \land A (j) = 0_{U}) \to j \cdot_{{mulGrp}_{W}} {var}_{1} (U) \in B$
70		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
71	5 45 15 70 21	lmod0vs	$⊢ (W \in LMod \land j \cdot_{{mulGrp}_{W}} {var}_{1} (U) \in B) \to 0_{Scalar (W)} \cdot_{W} (j \cdot_{{mulGrp}_{W}} {var}_{1} (U)) = 0_{W}$
72	62 69 71	syl2anc	$⊢ (((φ \land i \in ℕ_{0}) \land j \in ℕ_{0}) \land A (j) = 0_{U}) \to 0_{Scalar (W)} \cdot_{W} (j \cdot_{{mulGrp}_{W}} {var}_{1} (U)) = 0_{W}$
73	61 72	eqtrd	$⊢ (((φ \land i \in ℕ_{0}) \land j \in ℕ_{0}) \land A (j) = 0_{U}) \to A (j) \cdot_{W} (j \cdot_{{mulGrp}_{W}} {var}_{1} (U)) = 0_{W}$
74	73	ex	$⊢ ((φ \land i \in ℕ_{0}) \land j \in ℕ_{0}) \to (A (j) = 0_{U} \to A (j) \cdot_{W} (j \cdot_{{mulGrp}_{W}} {var}_{1} (U)) = 0_{W})$
75	74	imim2d	$⊢ ((φ \land i \in ℕ_{0}) \land j \in ℕ_{0}) \to ((i < j \to A (j) = 0_{U}) \to (i < j \to A (j) \cdot_{W} (j \cdot_{{mulGrp}_{W}} {var}_{1} (U)) = 0_{W}))$
76	75	ralimdva	$⊢ (φ \land i \in ℕ_{0}) \to (\forall j \in ℕ_{0} (i < j \to A (j) = 0_{U}) \to \forall j \in ℕ_{0} (i < j \to A (j) \cdot_{W} (j \cdot_{{mulGrp}_{W}} {var}_{1} (U)) = 0_{W}))$
77	76	reximdva	$⊢ φ \to (\exists i \in ℕ_{0} \forall j \in ℕ_{0} (i < j \to A (j) = 0_{U}) \to \exists i \in ℕ_{0} \forall j \in ℕ_{0} (i < j \to A (j) \cdot_{W} (j \cdot_{{mulGrp}_{W}} {var}_{1} (U)) = 0_{W}))$
78	56 77	mpd	$⊢ φ \to \exists i \in ℕ_{0} \forall j \in ℕ_{0} (i < j \to A (j) \cdot_{W} (j \cdot_{{mulGrp}_{W}} {var}_{1} (U)) = 0_{W})$
79	50 48 53 78	mptnn0fsuppd	$⊢ φ \to {finSupp}_{0_{W}} ((k \in ℕ_{0} ⟼ A (k) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U))))$
80	1 2 3 21 4 22 5 6 7 48 49 79	evls1gsumadd	$⊢ φ \to Q (\underset{k \in ℕ_{0}}{\sum_{W}} (A (k) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U)))) = \underset{k \in ℕ_{0}}{\sum_{S ↑_{𝑠} K}} Q (A (k) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U)))$
81	1 2 22 4 3	evls1rhm	$⊢ (S \in CRing \land R \in SubRing (S)) \to Q \in (W RingHom (S ↑_{𝑠} K))$
82	6 7 81	syl2anc	$⊢ φ \to Q \in (W RingHom (S ↑_{𝑠} K))$
83	82	adantr	$⊢ (φ \land k \in ℕ_{0}) \to Q \in (W RingHom (S ↑_{𝑠} K))$
84		eqid	$⊢ algSc (W) = algSc (W)$
85	84 45 36 24 46 5	asclf	$⊢ φ \to algSc (W) : {Base}_{Scalar (W)} ⟶ B$
86	85	adantr	$⊢ (φ \land k \in ℕ_{0}) \to algSc (W) : {Base}_{Scalar (W)} ⟶ B$
87	86 33	ffvelcdmd	$⊢ (φ \land k \in ℕ_{0}) \to algSc (W) (A (k)) \in B$
88		eqid	$⊢ \cdot_{W} = \cdot_{W}$
89		eqid	$⊢ \cdot_{(S ↑_{𝑠} K)} = \cdot_{(S ↑_{𝑠} K)}$
90	5 88 89	rhmmul	$⊢ (Q \in (W RingHom (S ↑_{𝑠} K)) \land algSc (W) (A (k)) \in B \land k \cdot_{{mulGrp}_{W}} {var}_{1} (U) \in B) \to Q (algSc (W) (A (k)) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U))) = Q (algSc (W) (A (k))) \cdot_{(S ↑_{𝑠} K)} Q (k \cdot_{{mulGrp}_{W}} {var}_{1} (U))$
91	83 87 44 90	syl3anc	$⊢ (φ \land k \in ℕ_{0}) \to Q (algSc (W) (A (k)) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U))) = Q (algSc (W) (A (k))) \cdot_{(S ↑_{𝑠} K)} Q (k \cdot_{{mulGrp}_{W}} {var}_{1} (U))$
92	4	subrgcrng	$⊢ (S \in CRing \land R \in SubRing (S)) \to U \in CRing$
93	6 7 92	syl2anc	$⊢ φ \to U \in CRing$
94	3	ply1assa	$⊢ U \in CRing \to W \in AssAlg$
95	93 94	syl	$⊢ φ \to W \in AssAlg$
96	95	adantr	$⊢ (φ \land k \in ℕ_{0}) \to W \in AssAlg$
97	84 45 46 5 88 15	asclmul1	$⊢ (W \in AssAlg \land A (k) \in {Base}_{Scalar (W)} \land k \cdot_{{mulGrp}_{W}} {var}_{1} (U) \in B) \to algSc (W) (A (k)) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U)) = A (k) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U))$
98	96 33 44 97	syl3anc	$⊢ (φ \land k \in ℕ_{0}) \to algSc (W) (A (k)) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U)) = A (k) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U))$
99	98	fveq2d	$⊢ (φ \land k \in ℕ_{0}) \to Q (algSc (W) (A (k)) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U))) = Q (A (k) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U)))$
100		eqid	$⊢ {Base}_{(S ↑_{𝑠} K)} = {Base}_{(S ↑_{𝑠} K)}$
101	6	adantr	$⊢ (φ \land k \in ℕ_{0}) \to S \in CRing$
102	2	fvexi	$⊢ K \in V$
103	102	a1i	$⊢ (φ \land k \in ℕ_{0}) \to K \in V$
104	5 100	rhmf	$⊢ Q \in (W RingHom (S ↑_{𝑠} K)) \to Q : B ⟶ {Base}_{(S ↑_{𝑠} K)}$
105	83 104	syl	$⊢ (φ \land k \in ℕ_{0}) \to Q : B ⟶ {Base}_{(S ↑_{𝑠} K)}$
106	105 87	ffvelcdmd	$⊢ (φ \land k \in ℕ_{0}) \to Q (algSc (W) (A (k))) \in {Base}_{(S ↑_{𝑠} K)}$
107	105 44	ffvelcdmd	$⊢ (φ \land k \in ℕ_{0}) \to Q (k \cdot_{{mulGrp}_{W}} {var}_{1} (U)) \in {Base}_{(S ↑_{𝑠} K)}$
108	22 100 101 103 106 107 9 89	pwsmulrval	$⊢ (φ \land k \in ℕ_{0}) \to Q (algSc (W) (A (k))) \cdot_{(S ↑_{𝑠} K)} Q (k \cdot_{{mulGrp}_{W}} {var}_{1} (U)) = Q (algSc (W) (A (k))) {\underset{˙}{\cdot}}_{f} Q (k \cdot_{{mulGrp}_{W}} {var}_{1} (U))$
109	22 2 100 101 103 106	pwselbas	$⊢ (φ \land k \in ℕ_{0}) \to Q (algSc (W) (A (k))) : K ⟶ K$
110	109	ffnd	$⊢ (φ \land k \in ℕ_{0}) \to Q (algSc (W) (A (k))) Fn K$
111	22 2 100 101 103 107	pwselbas	$⊢ (φ \land k \in ℕ_{0}) \to Q (k \cdot_{{mulGrp}_{W}} {var}_{1} (U)) : K ⟶ K$
112	111	ffnd	$⊢ (φ \land k \in ℕ_{0}) \to Q (k \cdot_{{mulGrp}_{W}} {var}_{1} (U)) Fn K$
113		inidm	$⊢ K \cap K = K$
114	6	ad2antrr	$⊢ ((φ \land k \in ℕ_{0}) \land x \in K) \to S \in CRing$
115	7	ad2antrr	$⊢ ((φ \land k \in ℕ_{0}) \land x \in K) \to R \in SubRing (S)$
116	2	subrgss	$⊢ R \in SubRing (S) \to R \subseteq K$
117	7 116	syl	$⊢ φ \to R \subseteq K$
118	4 2	ressbas2	$⊢ R \subseteq K \to R = {Base}_{U}$
119	117 118	syl	$⊢ φ \to R = {Base}_{U}$
120	119	adantr	$⊢ (φ \land k \in ℕ_{0}) \to R = {Base}_{U}$
121	28 120	eleqtrrd	$⊢ (φ \land k \in ℕ_{0}) \to A (k) \in R$
122	121	adantr	$⊢ ((φ \land k \in ℕ_{0}) \land x \in K) \to A (k) \in R$
123		simpr	$⊢ ((φ \land k \in ℕ_{0}) \land x \in K) \to x \in K$
124	1 3 4 2 84 114 115 122 123	evls1scafv	$⊢ ((φ \land k \in ℕ_{0}) \land x \in K) \to Q (algSc (W) (A (k))) (x) = A (k)$
125		simplr	$⊢ ((φ \land k \in ℕ_{0}) \land x \in K) \to k \in ℕ_{0}$
126	1 4 3 14 2 17 10 114 115 125 123	evls1varpwval	$⊢ ((φ \land k \in ℕ_{0}) \land x \in K) \to Q (k \cdot_{{mulGrp}_{W}} {var}_{1} (U)) (x) = k \underset{˙}{\times} x$
127	110 112 103 103 113 124 126	offval	$⊢ (φ \land k \in ℕ_{0}) \to Q (algSc (W) (A (k))) {\underset{˙}{\cdot}}_{f} Q (k \cdot_{{mulGrp}_{W}} {var}_{1} (U)) = (x \in K ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x))$
128	108 127	eqtrd	$⊢ (φ \land k \in ℕ_{0}) \to Q (algSc (W) (A (k))) \cdot_{(S ↑_{𝑠} K)} Q (k \cdot_{{mulGrp}_{W}} {var}_{1} (U)) = (x \in K ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x))$
129	91 99 128	3eqtr3d	$⊢ (φ \land k \in ℕ_{0}) \to Q (A (k) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U))) = (x \in K ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x))$
130	129	mpteq2dva	$⊢ φ \to (k \in ℕ_{0} ⟼ Q (A (k) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U)))) = (k \in ℕ_{0} ⟼ (x \in K ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x)))$
131	130	oveq2d	$⊢ φ \to \underset{k \in ℕ_{0}}{\sum_{S ↑_{𝑠} K}} Q (A (k) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U))) = \underset{k \in ℕ_{0}}{\sum_{S ↑_{𝑠} K}} (x \in K ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x))$
132		eqid	$⊢ 0_{(S ↑_{𝑠} K)} = 0_{(S ↑_{𝑠} K)}$
133	102	a1i	$⊢ φ \to K \in V$
134		nn0ex	$⊢ ℕ_{0} \in V$
135	134	a1i	$⊢ φ \to ℕ_{0} \in V$
136	6	crngringd	$⊢ φ \to S \in Ring$
137	136	ringcmnd	$⊢ φ \to S \in CMnd$
138	136	ad2antrr	$⊢ ((φ \land k \in ℕ_{0}) \land x \in K) \to S \in Ring$
139	7	adantr	$⊢ (φ \land k \in ℕ_{0}) \to R \in SubRing (S)$
140	139 116	syl	$⊢ (φ \land k \in ℕ_{0}) \to R \subseteq K$
141	140 121	sseldd	$⊢ (φ \land k \in ℕ_{0}) \to A (k) \in K$
142	141	adantr	$⊢ ((φ \land k \in ℕ_{0}) \land x \in K) \to A (k) \in K$
143		eqid	$⊢ {mulGrp}_{S} = {mulGrp}_{S}$
144	143 2	mgpbas	$⊢ K = {Base}_{{mulGrp}_{S}}$
145	143	ringmgp	$⊢ S \in Ring \to {mulGrp}_{S} \in Mnd$
146	136 145	syl	$⊢ φ \to {mulGrp}_{S} \in Mnd$
147	146	ad2antrr	$⊢ ((φ \land k \in ℕ_{0}) \land x \in K) \to {mulGrp}_{S} \in Mnd$
148	144 10 147 125 123	mulgnn0cld	$⊢ ((φ \land k \in ℕ_{0}) \land x \in K) \to k \underset{˙}{\times} x \in K$
149	2 9 138 142 148	ringcld	$⊢ ((φ \land k \in ℕ_{0}) \land x \in K) \to A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x) \in K$
150	149	3impa	$⊢ (φ \land k \in ℕ_{0} \land x \in K) \to A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x) \in K$
151	150	3com23	$⊢ (φ \land x \in K \land k \in ℕ_{0}) \to A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x) \in K$
152	151	3expb	$⊢ (φ \land (x \in K \land k \in ℕ_{0})) \to A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x) \in K$
153	135	mptexd	$⊢ φ \to (k \in ℕ_{0} ⟼ (x \in K ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x))) \in V$
154		funmpt	$⊢ Fun (k \in ℕ_{0} ⟼ (x \in K ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x)))$
155	154	a1i	$⊢ φ \to Fun (k \in ℕ_{0} ⟼ (x \in K ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x)))$
156		fvexd	$⊢ φ \to 0_{(S ↑_{𝑠} K)} \in V$
157	11 5 3 54	coe1sfi	$⊢ M \in B \to {finSupp}_{0_{U}} (A)$
158	8 157	syl	$⊢ φ \to {finSupp}_{0_{U}} (A)$
159	158	fsuppimpd	$⊢ φ \to A supp 0_{U} \in Fin$
160	11 5 3 26	coe1f	$⊢ M \in B \to A : ℕ_{0} ⟶ {Base}_{U}$
161	8 160	syl	$⊢ φ \to A : ℕ_{0} ⟶ {Base}_{U}$
162	161	ffnd	$⊢ φ \to A Fn ℕ_{0}$
163	162	adantr	$⊢ (φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \to A Fn ℕ_{0}$
164	134	a1i	$⊢ (φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \to ℕ_{0} \in V$
165		fvexd	$⊢ (φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \to 0_{U} \in V$
166		simpr	$⊢ (φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \to k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))$
167	163 164 165 166	fvdifsupp	$⊢ (φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \to A (k) = 0_{U}$
168		eqid	$⊢ 0_{S} = 0_{S}$
169	4 168	subrg0	$⊢ R \in SubRing (S) \to 0_{S} = 0_{U}$
170	7 169	syl	$⊢ φ \to 0_{S} = 0_{U}$
171	170	adantr	$⊢ (φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \to 0_{S} = 0_{U}$
172	167 171	eqtr4d	$⊢ (φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \to A (k) = 0_{S}$
173	172	adantr	$⊢ ((φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \land x \in K) \to A (k) = 0_{S}$
174	173	oveq1d	$⊢ ((φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \land x \in K) \to A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x) = 0_{S} \underset{˙}{\cdot} (k \underset{˙}{\times} x)$
175	136	ad2antrr	$⊢ ((φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \land x \in K) \to S \in Ring$
176	175 145	syl	$⊢ ((φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \land x \in K) \to {mulGrp}_{S} \in Mnd$
177		simplr	$⊢ ((φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \land x \in K) \to k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))$
178	177	eldifad	$⊢ ((φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \land x \in K) \to k \in ℕ_{0}$
179		simpr	$⊢ ((φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \land x \in K) \to x \in K$
180	144 10 176 178 179	mulgnn0cld	$⊢ ((φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \land x \in K) \to k \underset{˙}{\times} x \in K$
181	2 9 168	ringlz	$⊢ (S \in Ring \land k \underset{˙}{\times} x \in K) \to 0_{S} \underset{˙}{\cdot} (k \underset{˙}{\times} x) = 0_{S}$
182	175 180 181	syl2anc	$⊢ ((φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \land x \in K) \to 0_{S} \underset{˙}{\cdot} (k \underset{˙}{\times} x) = 0_{S}$
183	174 182	eqtrd	$⊢ ((φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \land x \in K) \to A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x) = 0_{S}$
184	183	mpteq2dva	$⊢ (φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \to (x \in K ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x)) = (x \in K ⟼ 0_{S})$
185		fconstmpt	$⊢ K \times \{0_{S}\} = (x \in K ⟼ 0_{S})$
186	184 185	eqtr4di	$⊢ (φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \to (x \in K ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x)) = K \times \{0_{S}\}$
187	137	cmnmndd	$⊢ φ \to S \in Mnd$
188	22 168	pws0g	$⊢ (S \in Mnd \land K \in V) \to K \times \{0_{S}\} = 0_{(S ↑_{𝑠} K)}$
189	187 133 188	syl2anc	$⊢ φ \to K \times \{0_{S}\} = 0_{(S ↑_{𝑠} K)}$
190	189	adantr	$⊢ (φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \to K \times \{0_{S}\} = 0_{(S ↑_{𝑠} K)}$
191	186 190	eqtrd	$⊢ (φ \land k \in (ℕ_{0} ∖ {supp}_{0_{U}} (A))) \to (x \in K ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x)) = 0_{(S ↑_{𝑠} K)}$
192	191 135	suppss2	$⊢ φ \to (k \in ℕ_{0} ⟼ (x \in K ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x))) supp 0_{(S ↑_{𝑠} K)} \subseteq A supp 0_{U}$
193		suppssfifsupp	$⊢ (((k \in ℕ_{0} ⟼ (x \in K ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x))) \in V \land Fun (k \in ℕ_{0} ⟼ (x \in K ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x))) \land 0_{(S ↑_{𝑠} K)} \in V) \land (A supp 0_{U} \in Fin \land (k \in ℕ_{0} ⟼ (x \in K ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x))) supp 0_{(S ↑_{𝑠} K)} \subseteq A supp 0_{U})) \to {finSupp}_{0_{(S ↑_{𝑠} K)}} ((k \in ℕ_{0} ⟼ (x \in K ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x))))$
194	153 155 156 159 192 193	syl32anc	$⊢ φ \to {finSupp}_{0_{(S ↑_{𝑠} K)}} ((k \in ℕ_{0} ⟼ (x \in K ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x))))$
195	22 2 132 133 135 137 152 194	pwsgsum	$⊢ φ \to \underset{k \in ℕ_{0}}{\sum_{S ↑_{𝑠} K}} (x \in K ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x)) = (x \in K ⟼ \underset{k \in ℕ_{0}}{\sum_{S}} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x)))$
196	80 131 195	3eqtrd	$⊢ φ \to Q (\underset{k \in ℕ_{0}}{\sum_{W}} (A (k) \cdot_{W} (k \cdot_{{mulGrp}_{W}} {var}_{1} (U)))) = (x \in K ⟼ \underset{k \in ℕ_{0}}{\sum_{S}} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x)))$
197	20 196	eqtrd	$⊢ φ \to Q (M) = (x \in K ⟼ \underset{k \in ℕ_{0}}{\sum_{S}} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} x)))$

Metamath Proof Explorer

Theorem evls1fpws

Proof