gsummoncoe1

Description: A coefficient of the polynomial represented as a sum of scaled monomials is the coefficient of the corresponding scaled monomial. (Contributed by AV, 13-Oct-2019)

	Ref	Expression
Hypotheses	gsummonply1.p	$⊢ P = {Poly}_{1} (R)$
	gsummonply1.b	$⊢ B = {Base}_{P}$
	gsummonply1.x	$⊢ X = {var}_{1} (R)$
	gsummonply1.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	gsummonply1.r	$⊢ φ \to R \in Ring$
	gsummonply1.k	$⊢ K = {Base}_{R}$
	gsummonply1.m	$⊢ \underset{˙}{*} = \cdot_{P}$
	gsummonply1.0	$⊢ \underset{˙}{0} = 0_{R}$
	gsummonply1.a	$⊢ φ \to \forall k \in ℕ_{0} A \in K$
	gsummonply1.f	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((k \in ℕ_{0} ⟼ A))$
	gsummonply1.l	$⊢ φ \to L \in ℕ_{0}$
Assertion	gsummoncoe1	$⊢ φ \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} (A \underset{˙}{*} (k \underset{˙}{\times} X))) (L) = ⦋ L / k ⦌ A$

Proof

Step	Hyp	Ref	Expression
1		gsummonply1.p	$⊢ P = {Poly}_{1} (R)$
2		gsummonply1.b	$⊢ B = {Base}_{P}$
3		gsummonply1.x	$⊢ X = {var}_{1} (R)$
4		gsummonply1.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
5		gsummonply1.r	$⊢ φ \to R \in Ring$
6		gsummonply1.k	$⊢ K = {Base}_{R}$
7		gsummonply1.m	$⊢ \underset{˙}{*} = \cdot_{P}$
8		gsummonply1.0	$⊢ \underset{˙}{0} = 0_{R}$
9		gsummonply1.a	$⊢ φ \to \forall k \in ℕ_{0} A \in K$
10		gsummonply1.f	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((k \in ℕ_{0} ⟼ A))$
11		gsummonply1.l	$⊢ φ \to L \in ℕ_{0}$
12	9	r19.21bi	$⊢ (φ \land k \in ℕ_{0}) \to A \in K$
13	12	fmpttd	$⊢ φ \to (k \in ℕ_{0} ⟼ A) : ℕ_{0} ⟶ K$
14	6	fvexi	$⊢ K \in V$
15	14	a1i	$⊢ φ \to K \in V$
16		nn0ex	$⊢ ℕ_{0} \in V$
17		elmapg	$⊢ (K \in V \land ℕ_{0} \in V) \to ((k \in ℕ_{0} ⟼ A) \in (K^{ℕ_{0}}) \leftrightarrow (k \in ℕ_{0} ⟼ A) : ℕ_{0} ⟶ K)$
18	15 16 17	sylancl	$⊢ φ \to ((k \in ℕ_{0} ⟼ A) \in (K^{ℕ_{0}}) \leftrightarrow (k \in ℕ_{0} ⟼ A) : ℕ_{0} ⟶ K)$
19	13 18	mpbird	$⊢ φ \to (k \in ℕ_{0} ⟼ A) \in (K^{ℕ_{0}})$
20	8	fvexi	$⊢ \underset{˙}{0} \in V$
21		fsuppmapnn0ub	$⊢ ((k \in ℕ_{0} ⟼ A) \in (K^{ℕ_{0}}) \land \underset{˙}{0} \in V) \to ({finSupp}_{\underset{˙}{0}} ((k \in ℕ_{0} ⟼ A)) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to (k \in ℕ_{0} ⟼ A) (x) = \underset{˙}{0}))$
22	19 20 21	sylancl	$⊢ φ \to ({finSupp}_{\underset{˙}{0}} ((k \in ℕ_{0} ⟼ A)) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to (k \in ℕ_{0} ⟼ A) (x) = \underset{˙}{0}))$
23	10 22	mpd	$⊢ φ \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to (k \in ℕ_{0} ⟼ A) (x) = \underset{˙}{0})$
24		simpr	$⊢ ((φ \land s \in ℕ_{0}) \land x \in ℕ_{0}) \to x \in ℕ_{0}$
25	9	ad2antrr	$⊢ ((φ \land s \in ℕ_{0}) \land x \in ℕ_{0}) \to \forall k \in ℕ_{0} A \in K$
26		rspcsbela	$⊢ (x \in ℕ_{0} \land \forall k \in ℕ_{0} A \in K) \to ⦋ x / k ⦌ A \in K$
27	24 25 26	syl2anc	$⊢ ((φ \land s \in ℕ_{0}) \land x \in ℕ_{0}) \to ⦋ x / k ⦌ A \in K$
28		eqid	$⊢ (k \in ℕ_{0} ⟼ A) = (k \in ℕ_{0} ⟼ A)$
29	28	fvmpts	$⊢ (x \in ℕ_{0} \land ⦋ x / k ⦌ A \in K) \to (k \in ℕ_{0} ⟼ A) (x) = ⦋ x / k ⦌ A$
30	24 27 29	syl2anc	$⊢ ((φ \land s \in ℕ_{0}) \land x \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ A) (x) = ⦋ x / k ⦌ A$
31	30	eqeq1d	$⊢ ((φ \land s \in ℕ_{0}) \land x \in ℕ_{0}) \to ((k \in ℕ_{0} ⟼ A) (x) = \underset{˙}{0} \leftrightarrow ⦋ x / k ⦌ A = \underset{˙}{0})$
32	31	imbi2d	$⊢ ((φ \land s \in ℕ_{0}) \land x \in ℕ_{0}) \to ((s < x \to (k \in ℕ_{0} ⟼ A) (x) = \underset{˙}{0}) \leftrightarrow (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0}))$
33	32	biimpd	$⊢ ((φ \land s \in ℕ_{0}) \land x \in ℕ_{0}) \to ((s < x \to (k \in ℕ_{0} ⟼ A) (x) = \underset{˙}{0}) \to (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0}))$
34	33	ralimdva	$⊢ (φ \land s \in ℕ_{0}) \to (\forall x \in ℕ_{0} (s < x \to (k \in ℕ_{0} ⟼ A) (x) = \underset{˙}{0}) \to \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0}))$
35		eqid	$⊢ 0_{P} = 0_{P}$
36	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
37		ringcmn	$⊢ P \in Ring \to P \in CMnd$
38	5 36 37	3syl	$⊢ φ \to P \in CMnd$
39	38	ad2antrr	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to P \in CMnd$
40	5	3ad2ant1	$⊢ (φ \land k \in ℕ_{0} \land A \in K) \to R \in Ring$
41		simp3	$⊢ (φ \land k \in ℕ_{0} \land A \in K) \to A \in K$
42		simp2	$⊢ (φ \land k \in ℕ_{0} \land A \in K) \to k \in ℕ_{0}$
43		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
44	6 1 3 7 43 4 2	ply1tmcl	$⊢ (R \in Ring \land A \in K \land k \in ℕ_{0}) \to A \underset{˙}{*} (k \underset{˙}{\times} X) \in B$
45	40 41 42 44	syl3anc	$⊢ (φ \land k \in ℕ_{0} \land A \in K) \to A \underset{˙}{*} (k \underset{˙}{\times} X) \in B$
46	45	3expia	$⊢ (φ \land k \in ℕ_{0}) \to (A \in K \to A \underset{˙}{*} (k \underset{˙}{\times} X) \in B)$
47	46	ralimdva	$⊢ φ \to (\forall k \in ℕ_{0} A \in K \to \forall k \in ℕ_{0} A \underset{˙}{*} (k \underset{˙}{\times} X) \in B)$
48	9 47	mpd	$⊢ φ \to \forall k \in ℕ_{0} A \underset{˙}{*} (k \underset{˙}{\times} X) \in B$
49	48	ad2antrr	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to \forall k \in ℕ_{0} A \underset{˙}{*} (k \underset{˙}{\times} X) \in B$
50		simplr	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to s \in ℕ_{0}$
51		nfv	$⊢ Ⅎ k s < x$
52		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ x / k ⦌ A$
53	52	nfeq1	$⊢ Ⅎ k ⦋ x / k ⦌ A = \underset{˙}{0}$
54	51 53	nfim	$⊢ Ⅎ k (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})$
55		nfv	$⊢ Ⅎ x (s < k \to ⦋ k / k ⦌ A = \underset{˙}{0})$
56		breq2	$⊢ x = k \to (s < x \leftrightarrow s < k)$
57		csbeq1	$⊢ x = k \to ⦋ x / k ⦌ A = ⦋ k / k ⦌ A$
58	57	eqeq1d	$⊢ x = k \to (⦋ x / k ⦌ A = \underset{˙}{0} \leftrightarrow ⦋ k / k ⦌ A = \underset{˙}{0})$
59	56 58	imbi12d	$⊢ x = k \to ((s < x \to ⦋ x / k ⦌ A = \underset{˙}{0}) \leftrightarrow (s < k \to ⦋ k / k ⦌ A = \underset{˙}{0}))$
60	54 55 59	cbvralw	$⊢ \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0}) \leftrightarrow \forall k \in ℕ_{0} (s < k \to ⦋ k / k ⦌ A = \underset{˙}{0})$
61		csbid	$⊢ ⦋ k / k ⦌ A = A$
62	61	eqeq1i	$⊢ ⦋ k / k ⦌ A = \underset{˙}{0} \leftrightarrow A = \underset{˙}{0}$
63		oveq1	$⊢ A = \underset{˙}{0} \to A \underset{˙}{} (k \underset{˙}{\times} X) = \underset{˙}{0} \underset{˙}{} (k \underset{˙}{\times} X)$
64	1	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
65	5 64	syl	$⊢ φ \to R = Scalar (P)$
66	65	fveq2d	$⊢ φ \to 0_{R} = 0_{Scalar (P)}$
67	8 66	eqtrid	$⊢ φ \to \underset{˙}{0} = 0_{Scalar (P)}$
68	67	ad2antrr	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to \underset{˙}{0} = 0_{Scalar (P)}$
69	68	oveq1d	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to \underset{˙}{0} \underset{˙}{} (k \underset{˙}{\times} X) = 0_{Scalar (P)} \underset{˙}{} (k \underset{˙}{\times} X)$
70	1	ply1lmod	$⊢ R \in Ring \to P \in LMod$
71	5 70	syl	$⊢ φ \to P \in LMod$
72	71	ad2antrr	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to P \in LMod$
73		eqid	$⊢ {Base}_{P} = {Base}_{P}$
74	43 73	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{P}}$
75	43	ringmgp	$⊢ P \in Ring \to {mulGrp}_{P} \in Mnd$
76	5 36 75	3syl	$⊢ φ \to {mulGrp}_{P} \in Mnd$
77	76	ad2antrr	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to {mulGrp}_{P} \in Mnd$
78		simpr	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
79	3 1 73	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
80	5 79	syl	$⊢ φ \to X \in {Base}_{P}$
81	80	ad2antrr	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to X \in {Base}_{P}$
82	74 4 77 78 81	mulgnn0cld	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to k \underset{˙}{\times} X \in {Base}_{P}$
83		eqid	$⊢ Scalar (P) = Scalar (P)$
84		eqid	$⊢ 0_{Scalar (P)} = 0_{Scalar (P)}$
85	73 83 7 84 35	lmod0vs	$⊢ (P \in LMod \land k \underset{˙}{\times} X \in {Base}_{P}) \to 0_{Scalar (P)} \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{P}$
86	72 82 85	syl2anc	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to 0_{Scalar (P)} \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{P}$
87	69 86	eqtrd	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to \underset{˙}{0} \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{P}$
88	63 87	sylan9eqr	$⊢ (((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \land A = \underset{˙}{0}) \to A \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{P}$
89	88	ex	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to (A = \underset{˙}{0} \to A \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{P})$
90	62 89	biimtrid	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to (⦋ k / k ⦌ A = \underset{˙}{0} \to A \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{P})$
91	90	imim2d	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to ((s < k \to ⦋ k / k ⦌ A = \underset{˙}{0}) \to (s < k \to A \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{P}))$
92	91	ralimdva	$⊢ (φ \land s \in ℕ_{0}) \to (\forall k \in ℕ_{0} (s < k \to ⦋ k / k ⦌ A = \underset{˙}{0}) \to \forall k \in ℕ_{0} (s < k \to A \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{P}))$
93	60 92	biimtrid	$⊢ (φ \land s \in ℕ_{0}) \to (\forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0}) \to \forall k \in ℕ_{0} (s < k \to A \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{P}))$
94	93	imp	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to \forall k \in ℕ_{0} (s < k \to A \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{P})$
95	2 35 39 49 50 94	gsummptnn0fz	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to \underset{k \in ℕ_{0}}{\sum_{P}} (A \underset{˙}{} (k \underset{˙}{\times} X)) = {\sum_{P}}_{k = 0}^{s} (A \underset{˙}{} (k \underset{˙}{\times} X))$
96	95	fveq2d	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} (A \underset{˙}{} (k \underset{˙}{\times} X))) = {coe}_{1} ({\sum_{P}}_{k = 0}^{s} (A \underset{˙}{} (k \underset{˙}{\times} X)))$
97	96	fveq1d	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} (A \underset{˙}{} (k \underset{˙}{\times} X))) (L) = {coe}_{1} ({\sum_{P}}_{k = 0}^{s} (A \underset{˙}{} (k \underset{˙}{\times} X))) (L)$
98	5	ad2antrr	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to R \in Ring$
99	11	ad2antrr	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to L \in ℕ_{0}$
100		elfznn0	$⊢ k \in (0 \dots s) \to k \in ℕ_{0}$
101		simpll	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to φ$
102	12	adantlr	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to A \in K$
103	101 78 102	3jca	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to (φ \land k \in ℕ_{0} \land A \in K)$
104	100 103	sylan2	$⊢ ((φ \land s \in ℕ_{0}) \land k \in (0 \dots s)) \to (φ \land k \in ℕ_{0} \land A \in K)$
105	104 45	syl	$⊢ ((φ \land s \in ℕ_{0}) \land k \in (0 \dots s)) \to A \underset{˙}{*} (k \underset{˙}{\times} X) \in B$
106	105	ralrimiva	$⊢ (φ \land s \in ℕ_{0}) \to \forall k \in (0 \dots s) A \underset{˙}{*} (k \underset{˙}{\times} X) \in B$
107	106	adantr	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to \forall k \in (0 \dots s) A \underset{˙}{*} (k \underset{˙}{\times} X) \in B$
108		fzfid	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to (0 \dots s) \in Fin$
109	1 2 98 99 107 108	coe1fzgsumd	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to {coe}_{1} ({\sum_{P}}_{k = 0}^{s} (A \underset{˙}{} (k \underset{˙}{\times} X))) (L) = {\sum_{R}}_{k = 0}^{s} {coe}_{1} (A \underset{˙}{} (k \underset{˙}{\times} X)) (L)$
110		nfv	$⊢ Ⅎ k (φ \land s \in ℕ_{0})$
111		nfcv	$⊢ \underline{Ⅎ} k ℕ_{0}$
112	111 54	nfralw	$⊢ Ⅎ k \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})$
113	110 112	nfan	$⊢ Ⅎ k ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0}))$
114	5	ad3antrrr	$⊢ (((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \land k \in (0 \dots s)) \to R \in Ring$
115	12	expcom	$⊢ k \in ℕ_{0} \to (φ \to A \in K)$
116	115 100	syl11	$⊢ φ \to (k \in (0 \dots s) \to A \in K)$
117	116	ad2antrr	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to (k \in (0 \dots s) \to A \in K)$
118	117	imp	$⊢ (((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \land k \in (0 \dots s)) \to A \in K$
119	100	adantl	$⊢ (((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \land k \in (0 \dots s)) \to k \in ℕ_{0}$
120	8 6 1 3 7 43 4	coe1tm	$⊢ (R \in Ring \land A \in K \land k \in ℕ_{0}) \to {coe}_{1} (A \underset{˙}{*} (k \underset{˙}{\times} X)) = (n \in ℕ_{0} ⟼ if (n = k, A, \underset{˙}{0}))$
121	114 118 119 120	syl3anc	$⊢ (((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \land k \in (0 \dots s)) \to {coe}_{1} (A \underset{˙}{*} (k \underset{˙}{\times} X)) = (n \in ℕ_{0} ⟼ if (n = k, A, \underset{˙}{0}))$
122		eqeq1	$⊢ n = L \to (n = k \leftrightarrow L = k)$
123	122	ifbid	$⊢ n = L \to if (n = k, A, \underset{˙}{0}) = if (L = k, A, \underset{˙}{0})$
124	123	adantl	$⊢ ((((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \land k \in (0 \dots s)) \land n = L) \to if (n = k, A, \underset{˙}{0}) = if (L = k, A, \underset{˙}{0})$
125	11	ad3antrrr	$⊢ (((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \land k \in (0 \dots s)) \to L \in ℕ_{0}$
126	6 8	ring0cl	$⊢ R \in Ring \to \underset{˙}{0} \in K$
127	5 126	syl	$⊢ φ \to \underset{˙}{0} \in K$
128	127	ad3antrrr	$⊢ (((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \land k \in (0 \dots s)) \to \underset{˙}{0} \in K$
129	118 128	ifcld	$⊢ (((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \land k \in (0 \dots s)) \to if (L = k, A, \underset{˙}{0}) \in K$
130	121 124 125 129	fvmptd	$⊢ (((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \land k \in (0 \dots s)) \to {coe}_{1} (A \underset{˙}{*} (k \underset{˙}{\times} X)) (L) = if (L = k, A, \underset{˙}{0})$
131	113 130	mpteq2da	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to (k \in (0 \dots s) ⟼ {coe}_{1} (A \underset{˙}{*} (k \underset{˙}{\times} X)) (L)) = (k \in (0 \dots s) ⟼ if (L = k, A, \underset{˙}{0}))$
132	131	oveq2d	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to {\sum_{R}}_{k = 0}^{s} {coe}_{1} (A \underset{˙}{*} (k \underset{˙}{\times} X)) (L) = {\sum_{R}}_{k = 0}^{s} if (L = k, A, \underset{˙}{0})$
133		breq2	$⊢ x = L \to (s < x \leftrightarrow s < L)$
134		csbeq1	$⊢ x = L \to ⦋ x / k ⦌ A = ⦋ L / k ⦌ A$
135	134	eqeq1d	$⊢ x = L \to (⦋ x / k ⦌ A = \underset{˙}{0} \leftrightarrow ⦋ L / k ⦌ A = \underset{˙}{0})$
136	133 135	imbi12d	$⊢ x = L \to ((s < x \to ⦋ x / k ⦌ A = \underset{˙}{0}) \leftrightarrow (s < L \to ⦋ L / k ⦌ A = \underset{˙}{0}))$
137	136	rspcva	$⊢ (L \in ℕ_{0} \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to (s < L \to ⦋ L / k ⦌ A = \underset{˙}{0})$
138		nfv	$⊢ Ⅎ k (φ \land (s \in ℕ_{0} \land s < L))$
139		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ L / k ⦌ A$
140	139	nfeq1	$⊢ Ⅎ k ⦋ L / k ⦌ A = \underset{˙}{0}$
141	138 140	nfan	$⊢ Ⅎ k ((φ \land (s \in ℕ_{0} \land s < L)) \land ⦋ L / k ⦌ A = \underset{˙}{0})$
142		elfz2nn0	$⊢ k \in (0 \dots s) \leftrightarrow (k \in ℕ_{0} \land s \in ℕ_{0} \land k \leq s)$
143		nn0re	$⊢ k \in ℕ_{0} \to k \in ℝ$
144	143	ad2antrr	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land L \in ℕ_{0}) \to k \in ℝ$
145		nn0re	$⊢ s \in ℕ_{0} \to s \in ℝ$
146	145	adantl	$⊢ (k \in ℕ_{0} \land s \in ℕ_{0}) \to s \in ℝ$
147	146	adantr	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land L \in ℕ_{0}) \to s \in ℝ$
148		nn0re	$⊢ L \in ℕ_{0} \to L \in ℝ$
149	148	adantl	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land L \in ℕ_{0}) \to L \in ℝ$
150		lelttr	$⊢ (k \in ℝ \land s \in ℝ \land L \in ℝ) \to ((k \leq s \land s < L) \to k < L)$
151	144 147 149 150	syl3anc	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land L \in ℕ_{0}) \to ((k \leq s \land s < L) \to k < L)$
152		animorr	$⊢ (((k \in ℕ_{0} \land s \in ℕ_{0}) \land L \in ℕ_{0}) \land k < L) \to (L < k \lor k < L)$
153		df-ne	$⊢ L \neq k \leftrightarrow \neg L = k$
154	143	adantr	$⊢ (k \in ℕ_{0} \land s \in ℕ_{0}) \to k \in ℝ$
155		lttri2	$⊢ (L \in ℝ \land k \in ℝ) \to (L \neq k \leftrightarrow (L < k \lor k < L))$
156	148 154 155	syl2anr	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land L \in ℕ_{0}) \to (L \neq k \leftrightarrow (L < k \lor k < L))$
157	156	adantr	$⊢ (((k \in ℕ_{0} \land s \in ℕ_{0}) \land L \in ℕ_{0}) \land k < L) \to (L \neq k \leftrightarrow (L < k \lor k < L))$
158	153 157	bitr3id	$⊢ (((k \in ℕ_{0} \land s \in ℕ_{0}) \land L \in ℕ_{0}) \land k < L) \to (\neg L = k \leftrightarrow (L < k \lor k < L))$
159	152 158	mpbird	$⊢ (((k \in ℕ_{0} \land s \in ℕ_{0}) \land L \in ℕ_{0}) \land k < L) \to \neg L = k$
160	159	ex	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land L \in ℕ_{0}) \to (k < L \to \neg L = k)$
161	151 160	syld	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land L \in ℕ_{0}) \to ((k \leq s \land s < L) \to \neg L = k)$
162	161	exp4b	$⊢ (k \in ℕ_{0} \land s \in ℕ_{0}) \to (L \in ℕ_{0} \to (k \leq s \to (s < L \to \neg L = k)))$
163	162	expimpd	$⊢ k \in ℕ_{0} \to ((s \in ℕ_{0} \land L \in ℕ_{0}) \to (k \leq s \to (s < L \to \neg L = k)))$
164	163	com23	$⊢ k \in ℕ_{0} \to (k \leq s \to ((s \in ℕ_{0} \land L \in ℕ_{0}) \to (s < L \to \neg L = k)))$
165	164	imp	$⊢ (k \in ℕ_{0} \land k \leq s) \to ((s \in ℕ_{0} \land L \in ℕ_{0}) \to (s < L \to \neg L = k))$
166	165	3adant2	$⊢ (k \in ℕ_{0} \land s \in ℕ_{0} \land k \leq s) \to ((s \in ℕ_{0} \land L \in ℕ_{0}) \to (s < L \to \neg L = k))$
167	142 166	sylbi	$⊢ k \in (0 \dots s) \to ((s \in ℕ_{0} \land L \in ℕ_{0}) \to (s < L \to \neg L = k))$
168	167	expd	$⊢ k \in (0 \dots s) \to (s \in ℕ_{0} \to (L \in ℕ_{0} \to (s < L \to \neg L = k)))$
169	11 168	syl7	$⊢ k \in (0 \dots s) \to (s \in ℕ_{0} \to (φ \to (s < L \to \neg L = k)))$
170	169	com12	$⊢ s \in ℕ_{0} \to (k \in (0 \dots s) \to (φ \to (s < L \to \neg L = k)))$
171	170	com24	$⊢ s \in ℕ_{0} \to (s < L \to (φ \to (k \in (0 \dots s) \to \neg L = k)))$
172	171	imp	$⊢ (s \in ℕ_{0} \land s < L) \to (φ \to (k \in (0 \dots s) \to \neg L = k))$
173	172	impcom	$⊢ (φ \land (s \in ℕ_{0} \land s < L)) \to (k \in (0 \dots s) \to \neg L = k)$
174	173	adantr	$⊢ ((φ \land (s \in ℕ_{0} \land s < L)) \land ⦋ L / k ⦌ A = \underset{˙}{0}) \to (k \in (0 \dots s) \to \neg L = k)$
175	174	imp	$⊢ (((φ \land (s \in ℕ_{0} \land s < L)) \land ⦋ L / k ⦌ A = \underset{˙}{0}) \land k \in (0 \dots s)) \to \neg L = k$
176	175	iffalsed	$⊢ (((φ \land (s \in ℕ_{0} \land s < L)) \land ⦋ L / k ⦌ A = \underset{˙}{0}) \land k \in (0 \dots s)) \to if (L = k, A, \underset{˙}{0}) = \underset{˙}{0}$
177	141 176	mpteq2da	$⊢ ((φ \land (s \in ℕ_{0} \land s < L)) \land ⦋ L / k ⦌ A = \underset{˙}{0}) \to (k \in (0 \dots s) ⟼ if (L = k, A, \underset{˙}{0})) = (k \in (0 \dots s) ⟼ \underset{˙}{0})$
178	177	oveq2d	$⊢ ((φ \land (s \in ℕ_{0} \land s < L)) \land ⦋ L / k ⦌ A = \underset{˙}{0}) \to {\sum_{R}}_{k = 0}^{s} if (L = k, A, \underset{˙}{0}) = {\sum_{R}}_{k = 0}^{s} \underset{˙}{0}$
179		ringmnd	$⊢ R \in Ring \to R \in Mnd$
180	5 179	syl	$⊢ φ \to R \in Mnd$
181	180	adantr	$⊢ (φ \land (s \in ℕ_{0} \land s < L)) \to R \in Mnd$
182		ovex	$⊢ (0 \dots s) \in V$
183	8	gsumz	$⊢ (R \in Mnd \land (0 \dots s) \in V) \to {\sum_{R}}_{k = 0}^{s} \underset{˙}{0} = \underset{˙}{0}$
184	181 182 183	sylancl	$⊢ (φ \land (s \in ℕ_{0} \land s < L)) \to {\sum_{R}}_{k = 0}^{s} \underset{˙}{0} = \underset{˙}{0}$
185	184	adantr	$⊢ ((φ \land (s \in ℕ_{0} \land s < L)) \land ⦋ L / k ⦌ A = \underset{˙}{0}) \to {\sum_{R}}_{k = 0}^{s} \underset{˙}{0} = \underset{˙}{0}$
186		id	$⊢ ⦋ L / k ⦌ A = \underset{˙}{0} \to ⦋ L / k ⦌ A = \underset{˙}{0}$
187	186	eqcomd	$⊢ ⦋ L / k ⦌ A = \underset{˙}{0} \to \underset{˙}{0} = ⦋ L / k ⦌ A$
188	187	adantl	$⊢ ((φ \land (s \in ℕ_{0} \land s < L)) \land ⦋ L / k ⦌ A = \underset{˙}{0}) \to \underset{˙}{0} = ⦋ L / k ⦌ A$
189	178 185 188	3eqtrd	$⊢ ((φ \land (s \in ℕ_{0} \land s < L)) \land ⦋ L / k ⦌ A = \underset{˙}{0}) \to {\sum_{R}}_{k = 0}^{s} if (L = k, A, \underset{˙}{0}) = ⦋ L / k ⦌ A$
190	189	ex	$⊢ (φ \land (s \in ℕ_{0} \land s < L)) \to (⦋ L / k ⦌ A = \underset{˙}{0} \to {\sum_{R}}_{k = 0}^{s} if (L = k, A, \underset{˙}{0}) = ⦋ L / k ⦌ A)$
191	190	expr	$⊢ (φ \land s \in ℕ_{0}) \to (s < L \to (⦋ L / k ⦌ A = \underset{˙}{0} \to {\sum_{R}}_{k = 0}^{s} if (L = k, A, \underset{˙}{0}) = ⦋ L / k ⦌ A))$
192	191	a2d	$⊢ (φ \land s \in ℕ_{0}) \to ((s < L \to ⦋ L / k ⦌ A = \underset{˙}{0}) \to (s < L \to {\sum_{R}}_{k = 0}^{s} if (L = k, A, \underset{˙}{0}) = ⦋ L / k ⦌ A))$
193	192	ex	$⊢ φ \to (s \in ℕ_{0} \to ((s < L \to ⦋ L / k ⦌ A = \underset{˙}{0}) \to (s < L \to {\sum_{R}}_{k = 0}^{s} if (L = k, A, \underset{˙}{0}) = ⦋ L / k ⦌ A)))$
194	193	com13	$⊢ (s < L \to ⦋ L / k ⦌ A = \underset{˙}{0}) \to (s \in ℕ_{0} \to (φ \to (s < L \to {\sum_{R}}_{k = 0}^{s} if (L = k, A, \underset{˙}{0}) = ⦋ L / k ⦌ A)))$
195	137 194	syl	$⊢ (L \in ℕ_{0} \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to (s \in ℕ_{0} \to (φ \to (s < L \to {\sum_{R}}_{k = 0}^{s} if (L = k, A, \underset{˙}{0}) = ⦋ L / k ⦌ A)))$
196	195	ex	$⊢ L \in ℕ_{0} \to (\forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0}) \to (s \in ℕ_{0} \to (φ \to (s < L \to {\sum_{R}}_{k = 0}^{s} if (L = k, A, \underset{˙}{0}) = ⦋ L / k ⦌ A))))$
197	196	com24	$⊢ L \in ℕ_{0} \to (φ \to (s \in ℕ_{0} \to (\forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0}) \to (s < L \to {\sum_{R}}_{k = 0}^{s} if (L = k, A, \underset{˙}{0}) = ⦋ L / k ⦌ A))))$
198	11 197	mpcom	$⊢ φ \to (s \in ℕ_{0} \to (\forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0}) \to (s < L \to {\sum_{R}}_{k = 0}^{s} if (L = k, A, \underset{˙}{0}) = ⦋ L / k ⦌ A)))$
199	198	imp31	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to (s < L \to {\sum_{R}}_{k = 0}^{s} if (L = k, A, \underset{˙}{0}) = ⦋ L / k ⦌ A)$
200	199	com12	$⊢ s < L \to (((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to {\sum_{R}}_{k = 0}^{s} if (L = k, A, \underset{˙}{0}) = ⦋ L / k ⦌ A)$
201		pm3.2	$⊢ (φ \land s \in ℕ_{0}) \to (\neg s < L \to ((φ \land s \in ℕ_{0}) \land \neg s < L))$
202	201	adantr	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to (\neg s < L \to ((φ \land s \in ℕ_{0}) \land \neg s < L))$
203	180	ad2antrr	$⊢ ((φ \land s \in ℕ_{0}) \land \neg s < L) \to R \in Mnd$
204	182	a1i	$⊢ ((φ \land s \in ℕ_{0}) \land \neg s < L) \to (0 \dots s) \in V$
205	11	nn0red	$⊢ φ \to L \in ℝ$
206		lenlt	$⊢ (L \in ℝ \land s \in ℝ) \to (L \leq s \leftrightarrow \neg s < L)$
207	205 145 206	syl2an	$⊢ (φ \land s \in ℕ_{0}) \to (L \leq s \leftrightarrow \neg s < L)$
208	11	ad2antrr	$⊢ ((φ \land s \in ℕ_{0}) \land L \leq s) \to L \in ℕ_{0}$
209		simplr	$⊢ ((φ \land s \in ℕ_{0}) \land L \leq s) \to s \in ℕ_{0}$
210		simpr	$⊢ ((φ \land s \in ℕ_{0}) \land L \leq s) \to L \leq s$
211		elfz2nn0	$⊢ L \in (0 \dots s) \leftrightarrow (L \in ℕ_{0} \land s \in ℕ_{0} \land L \leq s)$
212	208 209 210 211	syl3anbrc	$⊢ ((φ \land s \in ℕ_{0}) \land L \leq s) \to L \in (0 \dots s)$
213	212	ex	$⊢ (φ \land s \in ℕ_{0}) \to (L \leq s \to L \in (0 \dots s))$
214	207 213	sylbird	$⊢ (φ \land s \in ℕ_{0}) \to (\neg s < L \to L \in (0 \dots s))$
215	214	imp	$⊢ ((φ \land s \in ℕ_{0}) \land \neg s < L) \to L \in (0 \dots s)$
216		eqcom	$⊢ L = k \leftrightarrow k = L$
217		ifbi	$⊢ (L = k \leftrightarrow k = L) \to if (L = k, A, \underset{˙}{0}) = if (k = L, A, \underset{˙}{0})$
218	216 217	ax-mp	$⊢ if (L = k, A, \underset{˙}{0}) = if (k = L, A, \underset{˙}{0})$
219	218	mpteq2i	$⊢ (k \in (0 \dots s) ⟼ if (L = k, A, \underset{˙}{0})) = (k \in (0 \dots s) ⟼ if (k = L, A, \underset{˙}{0}))$
220	12 6	eleqtrdi	$⊢ (φ \land k \in ℕ_{0}) \to A \in {Base}_{R}$
221	220	ex	$⊢ φ \to (k \in ℕ_{0} \to A \in {Base}_{R})$
222	221	adantr	$⊢ (φ \land s \in ℕ_{0}) \to (k \in ℕ_{0} \to A \in {Base}_{R})$
223	222 100	impel	$⊢ ((φ \land s \in ℕ_{0}) \land k \in (0 \dots s)) \to A \in {Base}_{R}$
224	223	ralrimiva	$⊢ (φ \land s \in ℕ_{0}) \to \forall k \in (0 \dots s) A \in {Base}_{R}$
225	224	adantr	$⊢ ((φ \land s \in ℕ_{0}) \land \neg s < L) \to \forall k \in (0 \dots s) A \in {Base}_{R}$
226	8 203 204 215 219 225	gsummpt1n0	$⊢ ((φ \land s \in ℕ_{0}) \land \neg s < L) \to {\sum_{R}}_{k = 0}^{s} if (L = k, A, \underset{˙}{0}) = ⦋ L / k ⦌ A$
227	202 226	syl6com	$⊢ \neg s < L \to (((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to {\sum_{R}}_{k = 0}^{s} if (L = k, A, \underset{˙}{0}) = ⦋ L / k ⦌ A)$
228	200 227	pm2.61i	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to {\sum_{R}}_{k = 0}^{s} if (L = k, A, \underset{˙}{0}) = ⦋ L / k ⦌ A$
229	132 228	eqtrd	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to {\sum_{R}}_{k = 0}^{s} {coe}_{1} (A \underset{˙}{*} (k \underset{˙}{\times} X)) (L) = ⦋ L / k ⦌ A$
230	97 109 229	3eqtrd	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} (A \underset{˙}{*} (k \underset{˙}{\times} X))) (L) = ⦋ L / k ⦌ A$
231	230	ex	$⊢ (φ \land s \in ℕ_{0}) \to (\forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0}) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} (A \underset{˙}{*} (k \underset{˙}{\times} X))) (L) = ⦋ L / k ⦌ A)$
232	34 231	syld	$⊢ (φ \land s \in ℕ_{0}) \to (\forall x \in ℕ_{0} (s < x \to (k \in ℕ_{0} ⟼ A) (x) = \underset{˙}{0}) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} (A \underset{˙}{*} (k \underset{˙}{\times} X))) (L) = ⦋ L / k ⦌ A)$
233	232	rexlimdva	$⊢ φ \to (\exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to (k \in ℕ_{0} ⟼ A) (x) = \underset{˙}{0}) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} (A \underset{˙}{*} (k \underset{˙}{\times} X))) (L) = ⦋ L / k ⦌ A)$
234	23 233	mpd	$⊢ φ \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} (A \underset{˙}{*} (k \underset{˙}{\times} X))) (L) = ⦋ L / k ⦌ A$

Metamath Proof Explorer

Theorem gsummoncoe1

Proof