Metamath Proof Explorer

Theorem flcidc

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

Ref Expression
Hypotheses flcidc.f 
|- ( ph -> F = ( j e. S |-> if ( j = K , 1 , 0 ) ) )
flcidc.s 
|- ( ph -> S e. Fin )
flcidc.k 
|- ( ph -> K e. S )
flcidc.b 
|- ( ( ph /\ i e. S ) -> B e. CC )
Assertion flcidc 
|- ( ph -> sum_ i e. S ( ( F ` i ) x. B ) = [_ K / i ]_ B )

Proof

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