Theorem flcidc

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

	Ref	Expression
Hypotheses	flcidc.f	⊢ ( 𝜑 → 𝐹 = ( 𝑗 ∈ 𝑆 ↦ if ( 𝑗 = 𝐾 , 1 , 0 ) ) )
	flcidc.s	⊢ ( 𝜑 → 𝑆 ∈ Fin )
	flcidc.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑆 )
	flcidc.b	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑆 ) → 𝐵 ∈ ℂ )
Assertion	flcidc	⊢ ( 𝜑 → Σ 𝑖 ∈ 𝑆 ( ( 𝐹 ‘ 𝑖 ) · 𝐵 ) = ⦋ 𝐾 / 𝑖 ⦌ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		flcidc.f	⊢ ( 𝜑 → 𝐹 = ( 𝑗 ∈ 𝑆 ↦ if ( 𝑗 = 𝐾 , 1 , 0 ) ) )
2		flcidc.s	⊢ ( 𝜑 → 𝑆 ∈ Fin )
3		flcidc.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑆 )
4		flcidc.b	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑆 ) → 𝐵 ∈ ℂ )
5	1	fveq1d	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑖 ) = ( ( 𝑗 ∈ 𝑆 ↦ if ( 𝑗 = 𝐾 , 1 , 0 ) ) ‘ 𝑖 ) )
6	5	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ { 𝐾 } ) → ( 𝐹 ‘ 𝑖 ) = ( ( 𝑗 ∈ 𝑆 ↦ if ( 𝑗 = 𝐾 , 1 , 0 ) ) ‘ 𝑖 ) )
7	3	snssd	⊢ ( 𝜑 → { 𝐾 } ⊆ 𝑆 )
8	7	sselda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ { 𝐾 } ) → 𝑖 ∈ 𝑆 )
9		eqeq1	⊢ ( 𝑗 = 𝑖 → ( 𝑗 = 𝐾 ↔ 𝑖 = 𝐾 ) )
10	9	ifbid	⊢ ( 𝑗 = 𝑖 → if ( 𝑗 = 𝐾 , 1 , 0 ) = if ( 𝑖 = 𝐾 , 1 , 0 ) )
11		eqid	⊢ ( 𝑗 ∈ 𝑆 ↦ if ( 𝑗 = 𝐾 , 1 , 0 ) ) = ( 𝑗 ∈ 𝑆 ↦ if ( 𝑗 = 𝐾 , 1 , 0 ) )
12		1ex	⊢ 1 ∈ V
13		c0ex	⊢ 0 ∈ V
14	12 13	ifex	⊢ if ( 𝑖 = 𝐾 , 1 , 0 ) ∈ V
15	10 11 14	fvmpt	⊢ ( 𝑖 ∈ 𝑆 → ( ( 𝑗 ∈ 𝑆 ↦ if ( 𝑗 = 𝐾 , 1 , 0 ) ) ‘ 𝑖 ) = if ( 𝑖 = 𝐾 , 1 , 0 ) )
16	8 15	syl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ { 𝐾 } ) → ( ( 𝑗 ∈ 𝑆 ↦ if ( 𝑗 = 𝐾 , 1 , 0 ) ) ‘ 𝑖 ) = if ( 𝑖 = 𝐾 , 1 , 0 ) )
17	6 16	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ { 𝐾 } ) → ( 𝐹 ‘ 𝑖 ) = if ( 𝑖 = 𝐾 , 1 , 0 ) )
18		elsni	⊢ ( 𝑖 ∈ { 𝐾 } → 𝑖 = 𝐾 )
19	18	iftrued	⊢ ( 𝑖 ∈ { 𝐾 } → if ( 𝑖 = 𝐾 , 1 , 0 ) = 1 )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ { 𝐾 } ) → if ( 𝑖 = 𝐾 , 1 , 0 ) = 1 )
21	17 20	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ { 𝐾 } ) → ( 𝐹 ‘ 𝑖 ) = 1 )
22	21	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ { 𝐾 } ) → ( ( 𝐹 ‘ 𝑖 ) · 𝐵 ) = ( 1 · 𝐵 ) )
23	8 4	syldan	⊢ ( ( 𝜑 ∧ 𝑖 ∈ { 𝐾 } ) → 𝐵 ∈ ℂ )
24	23	mullidd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ { 𝐾 } ) → ( 1 · 𝐵 ) = 𝐵 )
25	22 24	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ { 𝐾 } ) → ( ( 𝐹 ‘ 𝑖 ) · 𝐵 ) = 𝐵 )
26	25	sumeq2dv	⊢ ( 𝜑 → Σ 𝑖 ∈ { 𝐾 } ( ( 𝐹 ‘ 𝑖 ) · 𝐵 ) = Σ 𝑖 ∈ { 𝐾 } 𝐵 )
27		ax-1cn	⊢ 1 ∈ ℂ
28		0cn	⊢ 0 ∈ ℂ
29	27 28	ifcli	⊢ if ( 𝑖 = 𝐾 , 1 , 0 ) ∈ ℂ
30	17 29	eqeltrdi	⊢ ( ( 𝜑 ∧ 𝑖 ∈ { 𝐾 } ) → ( 𝐹 ‘ 𝑖 ) ∈ ℂ )
31	30 23	mulcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ { 𝐾 } ) → ( ( 𝐹 ‘ 𝑖 ) · 𝐵 ) ∈ ℂ )
32	5	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑆 ∖ { 𝐾 } ) ) → ( 𝐹 ‘ 𝑖 ) = ( ( 𝑗 ∈ 𝑆 ↦ if ( 𝑗 = 𝐾 , 1 , 0 ) ) ‘ 𝑖 ) )
33		eldifi	⊢ ( 𝑖 ∈ ( 𝑆 ∖ { 𝐾 } ) → 𝑖 ∈ 𝑆 )
34	33	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑆 ∖ { 𝐾 } ) ) → 𝑖 ∈ 𝑆 )
35	34 15	syl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑆 ∖ { 𝐾 } ) ) → ( ( 𝑗 ∈ 𝑆 ↦ if ( 𝑗 = 𝐾 , 1 , 0 ) ) ‘ 𝑖 ) = if ( 𝑖 = 𝐾 , 1 , 0 ) )
36	32 35	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑆 ∖ { 𝐾 } ) ) → ( 𝐹 ‘ 𝑖 ) = if ( 𝑖 = 𝐾 , 1 , 0 ) )
37		eldifn	⊢ ( 𝑖 ∈ ( 𝑆 ∖ { 𝐾 } ) → ¬ 𝑖 ∈ { 𝐾 } )
38		velsn	⊢ ( 𝑖 ∈ { 𝐾 } ↔ 𝑖 = 𝐾 )
39	37 38	sylnib	⊢ ( 𝑖 ∈ ( 𝑆 ∖ { 𝐾 } ) → ¬ 𝑖 = 𝐾 )
40	39	iffalsed	⊢ ( 𝑖 ∈ ( 𝑆 ∖ { 𝐾 } ) → if ( 𝑖 = 𝐾 , 1 , 0 ) = 0 )
41	40	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑆 ∖ { 𝐾 } ) ) → if ( 𝑖 = 𝐾 , 1 , 0 ) = 0 )
42	36 41	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑆 ∖ { 𝐾 } ) ) → ( 𝐹 ‘ 𝑖 ) = 0 )
43	42	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑆 ∖ { 𝐾 } ) ) → ( ( 𝐹 ‘ 𝑖 ) · 𝐵 ) = ( 0 · 𝐵 ) )
44	34 4	syldan	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑆 ∖ { 𝐾 } ) ) → 𝐵 ∈ ℂ )
45	44	mul02d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑆 ∖ { 𝐾 } ) ) → ( 0 · 𝐵 ) = 0 )
46	43 45	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑆 ∖ { 𝐾 } ) ) → ( ( 𝐹 ‘ 𝑖 ) · 𝐵 ) = 0 )
47	7 31 46 2	fsumss	⊢ ( 𝜑 → Σ 𝑖 ∈ { 𝐾 } ( ( 𝐹 ‘ 𝑖 ) · 𝐵 ) = Σ 𝑖 ∈ 𝑆 ( ( 𝐹 ‘ 𝑖 ) · 𝐵 ) )
48		eleq1	⊢ ( 𝑗 = 𝐾 → ( 𝑗 ∈ 𝑆 ↔ 𝐾 ∈ 𝑆 ) )
49	48	anbi2d	⊢ ( 𝑗 = 𝐾 → ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ↔ ( 𝜑 ∧ 𝐾 ∈ 𝑆 ) ) )
50		csbeq1	⊢ ( 𝑗 = 𝐾 → ⦋ 𝑗 / 𝑖 ⦌ 𝐵 = ⦋ 𝐾 / 𝑖 ⦌ 𝐵 )
51	50	eleq1d	⊢ ( 𝑗 = 𝐾 → ( ⦋ 𝑗 / 𝑖 ⦌ 𝐵 ∈ ℂ ↔ ⦋ 𝐾 / 𝑖 ⦌ 𝐵 ∈ ℂ ) )
52	49 51	imbi12d	⊢ ( 𝑗 = 𝐾 → ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ⦋ 𝑗 / 𝑖 ⦌ 𝐵 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝐾 ∈ 𝑆 ) → ⦋ 𝐾 / 𝑖 ⦌ 𝐵 ∈ ℂ ) ) )
53		nfv	⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑗 ∈ 𝑆 )
54		nfcsb1v	⊢ Ⅎ 𝑖 ⦋ 𝑗 / 𝑖 ⦌ 𝐵
55	54	nfel1	⊢ Ⅎ 𝑖 ⦋ 𝑗 / 𝑖 ⦌ 𝐵 ∈ ℂ
56	53 55	nfim	⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ⦋ 𝑗 / 𝑖 ⦌ 𝐵 ∈ ℂ )
57		eleq1	⊢ ( 𝑖 = 𝑗 → ( 𝑖 ∈ 𝑆 ↔ 𝑗 ∈ 𝑆 ) )
58	57	anbi2d	⊢ ( 𝑖 = 𝑗 → ( ( 𝜑 ∧ 𝑖 ∈ 𝑆 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ) )
59		csbeq1a	⊢ ( 𝑖 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑖 ⦌ 𝐵 )
60	59	eleq1d	⊢ ( 𝑖 = 𝑗 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑗 / 𝑖 ⦌ 𝐵 ∈ ℂ ) )
61	58 60	imbi12d	⊢ ( 𝑖 = 𝑗 → ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑆 ) → 𝐵 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ⦋ 𝑗 / 𝑖 ⦌ 𝐵 ∈ ℂ ) ) )
62	56 61 4	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ⦋ 𝑗 / 𝑖 ⦌ 𝐵 ∈ ℂ )
63	52 62	vtoclg	⊢ ( 𝐾 ∈ 𝑆 → ( ( 𝜑 ∧ 𝐾 ∈ 𝑆 ) → ⦋ 𝐾 / 𝑖 ⦌ 𝐵 ∈ ℂ ) )
64	63	anabsi7	⊢ ( ( 𝜑 ∧ 𝐾 ∈ 𝑆 ) → ⦋ 𝐾 / 𝑖 ⦌ 𝐵 ∈ ℂ )
65	3 64	mpdan	⊢ ( 𝜑 → ⦋ 𝐾 / 𝑖 ⦌ 𝐵 ∈ ℂ )
66		sumsns	⊢ ( ( 𝐾 ∈ 𝑆 ∧ ⦋ 𝐾 / 𝑖 ⦌ 𝐵 ∈ ℂ ) → Σ 𝑖 ∈ { 𝐾 } 𝐵 = ⦋ 𝐾 / 𝑖 ⦌ 𝐵 )
67	3 65 66	syl2anc	⊢ ( 𝜑 → Σ 𝑖 ∈ { 𝐾 } 𝐵 = ⦋ 𝐾 / 𝑖 ⦌ 𝐵 )
68	26 47 67	3eqtr3d	⊢ ( 𝜑 → Σ 𝑖 ∈ 𝑆 ( ( 𝐹 ‘ 𝑖 ) · 𝐵 ) = ⦋ 𝐾 / 𝑖 ⦌ 𝐵 )