Theorem flcidc

Description: Finite linear combinations with an indicator function. (Contributed by Stefan O'Rear, 5-Dec-2014)

	Ref	Expression
Hypotheses	flcidc.f	$$⊢\phi \to F=\left(j\in S⟼if\left(j=K,1,0\right)\right)$$
	flcidc.s	$$⊢\phi \to S\in \mathrm{Fin}$$
	flcidc.k	$$⊢\phi \to K\in S$$
	flcidc.b	$$⊢\left(\phi \wedge i\in S\right)\to B\in ℂ$$
Assertion	flcidc	$$⊢\phi \to \sum _{i\in S}F\left(i\right)B=⦋K/i⦌B$$

Proof

Step	Hyp	Ref	Expression
1		flcidc.f	$$⊢\phi \to F=\left(j\in S⟼if\left(j=K,1,0\right)\right)$$
2		flcidc.s	$$⊢\phi \to S\in \mathrm{Fin}$$
3		flcidc.k	$$⊢\phi \to K\in S$$
4		flcidc.b	$$⊢\left(\phi \wedge i\in S\right)\to B\in ℂ$$
5	1	fveq1d	$$⊢\phi \to F\left(i\right)=\left(j\in S⟼if\left(j=K,1,0\right)\right)\left(i\right)$$
6	5	adantr	$$⊢\left(\phi \wedge i\in \left\{K\right\}\right)\to F\left(i\right)=\left(j\in S⟼if\left(j=K,1,0\right)\right)\left(i\right)$$
7	3	snssd	$$⊢\phi \to \left\{K\right\}\subseteq S$$
8	7	sselda	$$⊢\left(\phi \wedge i\in \left\{K\right\}\right)\to i\in S$$
9		eqeq1	$$⊢j=i\to \left(j=K\leftrightarrow i=K\right)$$
10	9	ifbid	$$⊢j=i\to if\left(j=K,1,0\right)=if\left(i=K,1,0\right)$$
11		eqid	$$⊢\left(j\in S⟼if\left(j=K,1,0\right)\right)=\left(j\in S⟼if\left(j=K,1,0\right)\right)$$
12		1ex	$$⊢1\in \mathrm{V}$$
13		c0ex	$$⊢0\in \mathrm{V}$$
14	12 13	ifex	$$⊢if\left(i=K,1,0\right)\in \mathrm{V}$$
15	10 11 14	fvmpt	$$⊢i\in S\to \left(j\in S⟼if\left(j=K,1,0\right)\right)\left(i\right)=if\left(i=K,1,0\right)$$
16	8 15	syl	$$⊢\left(\phi \wedge i\in \left\{K\right\}\right)\to \left(j\in S⟼if\left(j=K,1,0\right)\right)\left(i\right)=if\left(i=K,1,0\right)$$
17	6 16	eqtrd	$$⊢\left(\phi \wedge i\in \left\{K\right\}\right)\to F\left(i\right)=if\left(i=K,1,0\right)$$
18		elsni	$$⊢i\in \left\{K\right\}\to i=K$$
19	18	iftrued	$$⊢i\in \left\{K\right\}\to if\left(i=K,1,0\right)=1$$
20	19	adantl	$$⊢\left(\phi \wedge i\in \left\{K\right\}\right)\to if\left(i=K,1,0\right)=1$$
21	17 20	eqtrd	$$⊢\left(\phi \wedge i\in \left\{K\right\}\right)\to F\left(i\right)=1$$
22	21	oveq1d	$$⊢\left(\phi \wedge i\in \left\{K\right\}\right)\to F\left(i\right)B=1B$$
23	8 4	syldan	$$⊢\left(\phi \wedge i\in \left\{K\right\}\right)\to B\in ℂ$$
24	23	mulid2d	$$⊢\left(\phi \wedge i\in \left\{K\right\}\right)\to 1B=B$$
25	22 24	eqtrd	$$⊢\left(\phi \wedge i\in \left\{K\right\}\right)\to F\left(i\right)B=B$$
26	25	sumeq2dv	$$⊢\phi \to \sum _{i\in \left\{K\right\}}F\left(i\right)B=\sum _{i\in \left\{K\right\}}B$$
27		ax-1cn	$$⊢1\in ℂ$$
28		0cn	$$⊢0\in ℂ$$
29	27 28	ifcli	$$⊢if\left(i=K,1,0\right)\in ℂ$$
30	17 29	eqeltrdi	$$⊢\left(\phi \wedge i\in \left\{K\right\}\right)\to F\left(i\right)\in ℂ$$
31	30 23	mulcld	$$⊢\left(\phi \wedge i\in \left\{K\right\}\right)\to F\left(i\right)B\in ℂ$$
32	5	adantr	$$⊢\left(\phi \wedge i\in \left(S\setminus \left\{K\right\}\right)\right)\to F\left(i\right)=\left(j\in S⟼if\left(j=K,1,0\right)\right)\left(i\right)$$
33		eldifi	$$⊢i\in \left(S\setminus \left\{K\right\}\right)\to i\in S$$
34	33	adantl	$$⊢\left(\phi \wedge i\in \left(S\setminus \left\{K\right\}\right)\right)\to i\in S$$
35	34 15	syl	$$⊢\left(\phi \wedge i\in \left(S\setminus \left\{K\right\}\right)\right)\to \left(j\in S⟼if\left(j=K,1,0\right)\right)\left(i\right)=if\left(i=K,1,0\right)$$
36	32 35	eqtrd	$$⊢\left(\phi \wedge i\in \left(S\setminus \left\{K\right\}\right)\right)\to F\left(i\right)=if\left(i=K,1,0\right)$$
37		eldifn	$$⊢i\in \left(S\setminus \left\{K\right\}\right)\to \neg i\in \left\{K\right\}$$
38		velsn	$$⊢i\in \left\{K\right\}\leftrightarrow i=K$$
39	37 38	sylnib	$$⊢i\in \left(S\setminus \left\{K\right\}\right)\to \neg i=K$$
40	39	iffalsed	$$⊢i\in \left(S\setminus \left\{K\right\}\right)\to if\left(i=K,1,0\right)=0$$
41	40	adantl	$$⊢\left(\phi \wedge i\in \left(S\setminus \left\{K\right\}\right)\right)\to if\left(i=K,1,0\right)=0$$
42	36 41	eqtrd	$$⊢\left(\phi \wedge i\in \left(S\setminus \left\{K\right\}\right)\right)\to F\left(i\right)=0$$
43	42	oveq1d	$$⊢\left(\phi \wedge i\in \left(S\setminus \left\{K\right\}\right)\right)\to F\left(i\right)B=0\cdot B$$
44	34 4	syldan	$$⊢\left(\phi \wedge i\in \left(S\setminus \left\{K\right\}\right)\right)\to B\in ℂ$$
45	44	mul02d	$$⊢\left(\phi \wedge i\in \left(S\setminus \left\{K\right\}\right)\right)\to 0\cdot B=0$$
46	43 45	eqtrd	$$⊢\left(\phi \wedge i\in \left(S\setminus \left\{K\right\}\right)\right)\to F\left(i\right)B=0$$
47	7 31 46 2	fsumss	$$⊢\phi \to \sum _{i\in \left\{K\right\}}F\left(i\right)B=\sum _{i\in S}F\left(i\right)B$$
48		eleq1	$$⊢j=K\to \left(j\in S\leftrightarrow K\in S\right)$$
49	48	anbi2d	$$⊢j=K\to \left(\left(\phi \wedge j\in S\right)\leftrightarrow \left(\phi \wedge K\in S\right)\right)$$
50		csbeq1	$$⊢j=K\to ⦋j/i⦌B=⦋K/i⦌B$$
51	50	eleq1d	$$⊢j=K\to \left(⦋j/i⦌B\in ℂ\leftrightarrow ⦋K/i⦌B\in ℂ\right)$$
52	49 51	imbi12d	$$⊢j=K\to \left(\left(\left(\phi \wedge j\in S\right)\to ⦋j/i⦌B\in ℂ\right)\leftrightarrow \left(\left(\phi \wedge K\in S\right)\to ⦋K/i⦌B\in ℂ\right)\right)$$
53		nfv	$$⊢Ⅎi\left(\phi \wedge j\in S\right)$$
54		nfcsb1v	$$⊢\underset{\_}{Ⅎ}i⦋j/i⦌B$$
55	54	nfel1	$$⊢Ⅎi⦋j/i⦌B\in ℂ$$
56	53 55	nfim	$$⊢Ⅎi\left(\left(\phi \wedge j\in S\right)\to ⦋j/i⦌B\in ℂ\right)$$
57		eleq1	$$⊢i=j\to \left(i\in S\leftrightarrow j\in S\right)$$
58	57	anbi2d	$$⊢i=j\to \left(\left(\phi \wedge i\in S\right)\leftrightarrow \left(\phi \wedge j\in S\right)\right)$$
59		csbeq1a	$$⊢i=j\to B=⦋j/i⦌B$$
60	59	eleq1d	$$⊢i=j\to \left(B\in ℂ\leftrightarrow ⦋j/i⦌B\in ℂ\right)$$
61	58 60	imbi12d	$$⊢i=j\to \left(\left(\left(\phi \wedge i\in S\right)\to B\in ℂ\right)\leftrightarrow \left(\left(\phi \wedge j\in S\right)\to ⦋j/i⦌B\in ℂ\right)\right)$$
62	56 61 4	chvarfv	$$⊢\left(\phi \wedge j\in S\right)\to ⦋j/i⦌B\in ℂ$$
63	52 62	vtoclg	$$⊢K\in S\to \left(\left(\phi \wedge K\in S\right)\to ⦋K/i⦌B\in ℂ\right)$$
64	63	anabsi7	$$⊢\left(\phi \wedge K\in S\right)\to ⦋K/i⦌B\in ℂ$$
65	3 64	mpdan	$$⊢\phi \to ⦋K/i⦌B\in ℂ$$
66		sumsns	$$⊢\left(K\in S\wedge ⦋K/i⦌B\in ℂ\right)\to \sum _{i\in \left\{K\right\}}B=⦋K/i⦌B$$
67	3 65 66	syl2anc	$$⊢\phi \to \sum _{i\in \left\{K\right\}}B=⦋K/i⦌B$$
68	26 47 67	3eqtr3d	$$⊢\phi \to \sum _{i\in S}F\left(i\right)B=⦋K/i⦌B$$