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	syl5eq	$⊢ φ \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	43	ringmgp	$⊢ P \in Ring \to {mulGrp}_{P} \in Mnd$
74	5 36 73	3syl	$⊢ φ \to {mulGrp}_{P} \in Mnd$
75	74	ad2antrr	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to {mulGrp}_{P} \in Mnd$
76		simpr	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
77		eqid	$⊢ {Base}_{P} = {Base}_{P}$
78	3 1 77	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
79	5 78	syl	$⊢ φ \to X \in {Base}_{P}$
80	79	ad2antrr	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to X \in {Base}_{P}$
81	43 77	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{P}}$
82	81 4	mulgnn0cl	$⊢ ({mulGrp}_{P} \in Mnd \land k \in ℕ_{0} \land X \in {Base}_{P}) \to k \underset{˙}{\times} X \in {Base}_{P}$
83	75 76 80 82	syl3anc	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to k \underset{˙}{\times} X \in {Base}_{P}$
84		eqid	$⊢ Scalar (P) = Scalar (P)$
85		eqid	$⊢ 0_{Scalar (P)} = 0_{Scalar (P)}$
86	77 84 7 85 35	lmod0vs	$⊢ (P \in LMod \land k \underset{˙}{\times} X \in {Base}_{P}) \to 0_{Scalar (P)} \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{P}$
87	72 83 86	syl2anc	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to 0_{Scalar (P)} \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{P}$
88	69 87	eqtrd	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to \underset{˙}{0} \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{P}$
89	63 88	sylan9eqr	$⊢ (((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \land A = \underset{˙}{0}) \to A \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{P}$
90	89	ex	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to (A = \underset{˙}{0} \to A \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{P})$
91	62 90	syl5bi	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to (⦋ k / k ⦌ A = \underset{˙}{0} \to A \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{P})$
92	91	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}))$
93	92	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}))$
94	60 93	syl5bi	$⊢ (φ \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}))$
95	94	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})$
96	2 35 39 49 50 95	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))$
97	96	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)))$
98	97	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)$
99	5	ad2antrr	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to R \in Ring$
100	11	ad2antrr	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to L \in ℕ_{0}$
101		elfznn0	$⊢ k \in (0 \dots s) \to k \in ℕ_{0}$
102		simpll	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to φ$
103	12	adantlr	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to A \in K$
104	102 76 103	3jca	$⊢ ((φ \land s \in ℕ_{0}) \land k \in ℕ_{0}) \to (φ \land k \in ℕ_{0} \land A \in K)$
105	101 104	sylan2	$⊢ ((φ \land s \in ℕ_{0}) \land k \in (0 \dots s)) \to (φ \land k \in ℕ_{0} \land A \in K)$
106	105 45	syl	$⊢ ((φ \land s \in ℕ_{0}) \land k \in (0 \dots s)) \to A \underset{˙}{*} (k \underset{˙}{\times} X) \in B$
107	106	ralrimiva	$⊢ (φ \land s \in ℕ_{0}) \to \forall k \in (0 \dots s) A \underset{˙}{*} (k \underset{˙}{\times} X) \in B$
108	107	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$
109		fzfid	$⊢ ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})) \to (0 \dots s) \in Fin$
110	1 2 99 100 108 109	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)$
111		nfv	$⊢ Ⅎ k (φ \land s \in ℕ_{0})$
112		nfcv	$⊢ \underline{Ⅎ} k ℕ_{0}$
113	112 54	nfralw	$⊢ Ⅎ k \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0})$
114	111 113	nfan	$⊢ Ⅎ k ((φ \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ A = \underset{˙}{0}))$
115	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$
116	12	expcom	$⊢ k \in ℕ_{0} \to (φ \to A \in K)$
117	116 101	syl11	$⊢ φ \to (k \in (0 \dots s) \to A \in K)$
118	117	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)$
119	118	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$
120	101	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}$
121	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}))$
122	115 119 120 121	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}))$
123		eqeq1	$⊢ n = L \to (n = k \leftrightarrow L = k)$
124	123	ifbid	$⊢ n = L \to if (n = k, A, \underset{˙}{0}) = if (L = k, A, \underset{˙}{0})$
125	124	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})$
126	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}$
127	6 8	ring0cl	$⊢ R \in Ring \to \underset{˙}{0} \in K$
128	5 127	syl	$⊢ φ \to \underset{˙}{0} \in K$
129	128	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$
130	119 129	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$
131	122 125 126 130	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})$
132	114 131	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}))$
133	132	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})$
134		breq2	$⊢ x = L \to (s < x \leftrightarrow s < L)$
135		csbeq1	$⊢ x = L \to ⦋ x / k ⦌ A = ⦋ L / k ⦌ A$
136	135	eqeq1d	$⊢ x = L \to (⦋ x / k ⦌ A = \underset{˙}{0} \leftrightarrow ⦋ L / k ⦌ A = \underset{˙}{0})$
137	134 136	imbi12d	$⊢ x = L \to ((s < x \to ⦋ x / k ⦌ A = \underset{˙}{0}) \leftrightarrow (s < L \to ⦋ L / k ⦌ A = \underset{˙}{0}))$
138	137	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})$
139		nfv	$⊢ Ⅎ k (φ \land (s \in ℕ_{0} \land s < L))$
140		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ L / k ⦌ A$
141	140	nfeq1	$⊢ Ⅎ k ⦋ L / k ⦌ A = \underset{˙}{0}$
142	139 141	nfan	$⊢ Ⅎ k ((φ \land (s \in ℕ_{0} \land s < L)) \land ⦋ L / k ⦌ A = \underset{˙}{0})$
143		elfz2nn0	$⊢ k \in (0 \dots s) \leftrightarrow (k \in ℕ_{0} \land s \in ℕ_{0} \land k \leq s)$
144		nn0re	$⊢ k \in ℕ_{0} \to k \in ℝ$
145	144	ad2antrr	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land L \in ℕ_{0}) \to k \in ℝ$
146		nn0re	$⊢ s \in ℕ_{0} \to s \in ℝ$
147	146	adantl	$⊢ (k \in ℕ_{0} \land s \in ℕ_{0}) \to s \in ℝ$
148	147	adantr	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land L \in ℕ_{0}) \to s \in ℝ$
149		nn0re	$⊢ L \in ℕ_{0} \to L \in ℝ$
150	149	adantl	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land L \in ℕ_{0}) \to L \in ℝ$
151		lelttr	$⊢ (k \in ℝ \land s \in ℝ \land L \in ℝ) \to ((k \leq s \land s < L) \to k < L)$
152	145 148 150 151	syl3anc	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land L \in ℕ_{0}) \to ((k \leq s \land s < L) \to k < L)$
153		animorr	$⊢ (((k \in ℕ_{0} \land s \in ℕ_{0}) \land L \in ℕ_{0}) \land k < L) \to (L < k \lor k < L)$
154		df-ne	$⊢ L \neq k \leftrightarrow \neg L = k$
155	144	adantr	$⊢ (k \in ℕ_{0} \land s \in ℕ_{0}) \to k \in ℝ$
156		lttri2	$⊢ (L \in ℝ \land k \in ℝ) \to (L \neq k \leftrightarrow (L < k \lor k < L))$
157	149 155 156	syl2anr	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land L \in ℕ_{0}) \to (L \neq k \leftrightarrow (L < k \lor k < L))$
158	157	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))$
159	154 158	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))$
160	153 159	mpbird	$⊢ (((k \in ℕ_{0} \land s \in ℕ_{0}) \land L \in ℕ_{0}) \land k < L) \to \neg L = k$
161	160	ex	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land L \in ℕ_{0}) \to (k < L \to \neg L = k)$
162	152 161	syld	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land L \in ℕ_{0}) \to ((k \leq s \land s < L) \to \neg L = k)$
163	162	exp4b	$⊢ (k \in ℕ_{0} \land s \in ℕ_{0}) \to (L \in ℕ_{0} \to (k \leq s \to (s < L \to \neg L = k)))$
164	163	expimpd	$⊢ k \in ℕ_{0} \to ((s \in ℕ_{0} \land L \in ℕ_{0}) \to (k \leq s \to (s < L \to \neg L = k)))$
165	164	com23	$⊢ k \in ℕ_{0} \to (k \leq s \to ((s \in ℕ_{0} \land L \in ℕ_{0}) \to (s < L \to \neg L = k)))$
166	165	imp	$⊢ (k \in ℕ_{0} \land k \leq s) \to ((s \in ℕ_{0} \land L \in ℕ_{0}) \to (s < L \to \neg L = k))$
167	166	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))$
168	143 167	sylbi	$⊢ k \in (0 \dots s) \to ((s \in ℕ_{0} \land L \in ℕ_{0}) \to (s < L \to \neg L = k))$
169	168	expd	$⊢ k \in (0 \dots s) \to (s \in ℕ_{0} \to (L \in ℕ_{0} \to (s < L \to \neg L = k)))$
170	11 169	syl7	$⊢ k \in (0 \dots s) \to (s \in ℕ_{0} \to (φ \to (s < L \to \neg L = k)))$
171	170	com12	$⊢ s \in ℕ_{0} \to (k \in (0 \dots s) \to (φ \to (s < L \to \neg L = k)))$
172	171	com24	$⊢ s \in ℕ_{0} \to (s < L \to (φ \to (k \in (0 \dots s) \to \neg L = k)))$
173	172	imp	$⊢ (s \in ℕ_{0} \land s < L) \to (φ \to (k \in (0 \dots s) \to \neg L = k))$
174	173	impcom	$⊢ (φ \land (s \in ℕ_{0} \land s < L)) \to (k \in (0 \dots s) \to \neg L = k)$
175	174	adantr	$⊢ ((φ \land (s \in ℕ_{0} \land s < L)) \land ⦋ L / k ⦌ A = \underset{˙}{0}) \to (k \in (0 \dots s) \to \neg L = k)$
176	175	imp	$⊢ (((φ \land (s \in ℕ_{0} \land s < L)) \land ⦋ L / k ⦌ A = \underset{˙}{0}) \land k \in (0 \dots s)) \to \neg L = k$
177	176	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}$
178	142 177	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})$
179	178	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}$
180		ringmnd	$⊢ R \in Ring \to R \in Mnd$
181	5 180	syl	$⊢ φ \to R \in Mnd$
182	181	adantr	$⊢ (φ \land (s \in ℕ_{0} \land s < L)) \to R \in Mnd$
183		ovex	$⊢ (0 \dots s) \in V$
184	8	gsumz	$⊢ (R \in Mnd \land (0 \dots s) \in V) \to {\sum_{R}}_{k = 0}^{s} \underset{˙}{0} = \underset{˙}{0}$
185	182 183 184	sylancl	$⊢ (φ \land (s \in ℕ_{0} \land s < L)) \to {\sum_{R}}_{k = 0}^{s} \underset{˙}{0} = \underset{˙}{0}$
186	185	adantr	$⊢ ((φ \land (s \in ℕ_{0} \land s < L)) \land ⦋ L / k ⦌ A = \underset{˙}{0}) \to {\sum_{R}}_{k = 0}^{s} \underset{˙}{0} = \underset{˙}{0}$
187		id	$⊢ ⦋ L / k ⦌ A = \underset{˙}{0} \to ⦋ L / k ⦌ A = \underset{˙}{0}$
188	187	eqcomd	$⊢ ⦋ L / k ⦌ A = \underset{˙}{0} \to \underset{˙}{0} = ⦋ L / k ⦌ A$
189	188	adantl	$⊢ ((φ \land (s \in ℕ_{0} \land s < L)) \land ⦋ L / k ⦌ A = \underset{˙}{0}) \to \underset{˙}{0} = ⦋ L / k ⦌ A$
190	179 186 189	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$
191	190	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)$
192	191	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))$
193	192	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))$
194	193	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)))$
195	194	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)))$
196	138 195	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)))$
197	196	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))))$
198	197	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))))$
199	11 198	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)))$
200	199	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)$
201	200	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)$
202		pm3.2	$⊢ (φ \land s \in ℕ_{0}) \to (\neg s < L \to ((φ \land s \in ℕ_{0}) \land \neg s < L))$
203	202	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))$
204	181	ad2antrr	$⊢ ((φ \land s \in ℕ_{0}) \land \neg s < L) \to R \in Mnd$
205	183	a1i	$⊢ ((φ \land s \in ℕ_{0}) \land \neg s < L) \to (0 \dots s) \in V$
206	11	nn0red	$⊢ φ \to L \in ℝ$
207		lenlt	$⊢ (L \in ℝ \land s \in ℝ) \to (L \leq s \leftrightarrow \neg s < L)$
208	206 146 207	syl2an	$⊢ (φ \land s \in ℕ_{0}) \to (L \leq s \leftrightarrow \neg s < L)$
209	11	ad2antrr	$⊢ ((φ \land s \in ℕ_{0}) \land L \leq s) \to L \in ℕ_{0}$
210		simplr	$⊢ ((φ \land s \in ℕ_{0}) \land L \leq s) \to s \in ℕ_{0}$
211		simpr	$⊢ ((φ \land s \in ℕ_{0}) \land L \leq s) \to L \leq s$
212		elfz2nn0	$⊢ L \in (0 \dots s) \leftrightarrow (L \in ℕ_{0} \land s \in ℕ_{0} \land L \leq s)$
213	209 210 211 212	syl3anbrc	$⊢ ((φ \land s \in ℕ_{0}) \land L \leq s) \to L \in (0 \dots s)$
214	213	ex	$⊢ (φ \land s \in ℕ_{0}) \to (L \leq s \to L \in (0 \dots s))$
215	208 214	sylbird	$⊢ (φ \land s \in ℕ_{0}) \to (\neg s < L \to L \in (0 \dots s))$
216	215	imp	$⊢ ((φ \land s \in ℕ_{0}) \land \neg s < L) \to L \in (0 \dots s)$
217		eqcom	$⊢ L = k \leftrightarrow k = L$
218		ifbi	$⊢ (L = k \leftrightarrow k = L) \to if (L = k, A, \underset{˙}{0}) = if (k = L, A, \underset{˙}{0})$
219	217 218	ax-mp	$⊢ if (L = k, A, \underset{˙}{0}) = if (k = L, A, \underset{˙}{0})$
220	219	mpteq2i	$⊢ (k \in (0 \dots s) ⟼ if (L = k, A, \underset{˙}{0})) = (k \in (0 \dots s) ⟼ if (k = L, A, \underset{˙}{0}))$
221	12 6	eleqtrdi	$⊢ (φ \land k \in ℕ_{0}) \to A \in {Base}_{R}$
222	221	ex	$⊢ φ \to (k \in ℕ_{0} \to A \in {Base}_{R})$
223	222	adantr	$⊢ (φ \land s \in ℕ_{0}) \to (k \in ℕ_{0} \to A \in {Base}_{R})$
224	223 101	impel	$⊢ ((φ \land s \in ℕ_{0}) \land k \in (0 \dots s)) \to A \in {Base}_{R}$
225	224	ralrimiva	$⊢ (φ \land s \in ℕ_{0}) \to \forall k \in (0 \dots s) A \in {Base}_{R}$
226	225	adantr	$⊢ ((φ \land s \in ℕ_{0}) \land \neg s < L) \to \forall k \in (0 \dots s) A \in {Base}_{R}$
227	8 204 205 216 220 226	gsummpt1n0	$⊢ ((φ \land s \in ℕ_{0}) \land \neg s < L) \to {\sum_{R}}_{k = 0}^{s} if (L = k, A, \underset{˙}{0}) = ⦋ L / k ⦌ A$
228	203 227	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)$
229	201 228	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$
230	133 229	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$
231	98 110 230	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$
232	231	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)$
233	34 232	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)$
234	233	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)$
235	23 234	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