Metamath Proof Explorer

Theorem dpjrid

Description: The Y -th index projection annihilates elements of other factors. (Contributed by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypotheses dpjfval.1 
|- ( ph -> G dom DProd S )
dpjfval.2 
|- ( ph -> dom S = I )
dpjfval.p 
|- P = ( G dProj S )
dpjlid.3 
|- ( ph -> X e. I )
dpjlid.4 
|- ( ph -> A e. ( S ` X ) )
dpjrid.0 
|- .0. = ( 0g ` G )
dpjrid.5 
|- ( ph -> Y e. I )
dpjrid.6 
|- ( ph -> Y =/= X )
Assertion dpjrid 
|- ( ph -> ( ( P ` Y ) ` A ) = .0. )

Proof

Step Hyp Ref Expression
1 dpjfval.1 
 |-  ( ph -> G dom DProd S )
2 dpjfval.2 
 |-  ( ph -> dom S = I )
3 dpjfval.p 
 |-  P = ( G dProj S )
4 dpjlid.3 
 |-  ( ph -> X e. I )
5 dpjlid.4 
 |-  ( ph -> A e. ( S ` X ) )
6 dpjrid.0 
 |-  .0. = ( 0g ` G )
7 dpjrid.5 
 |-  ( ph -> Y e. I )
8 dpjrid.6 
 |-  ( ph -> Y =/= X )
9 fveq2 
 |-  ( x = Y -> ( P ` x ) = ( P ` Y ) )
10 9 fveq1d 
 |-  ( x = Y -> ( ( P ` x ) ` A ) = ( ( P ` Y ) ` A ) )
11 eqeq1 
 |-  ( x = Y -> ( x = X <-> Y = X ) )
12 11 ifbid 
 |-  ( x = Y -> if ( x = X , A , .0. ) = if ( Y = X , A , .0. ) )
13 10 12 eqeq12d 
 |-  ( x = Y -> ( ( ( P ` x ) ` A ) = if ( x = X , A , .0. ) <-> ( ( P ` Y ) ` A ) = if ( Y = X , A , .0. ) ) )
14 eqid 
 |-  { h e. X_ i e. I ( S ` i ) | h finSupp .0. } = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
15 eqid 
 |-  ( x e. I |-> if ( x = X , A , .0. ) ) = ( x e. I |-> if ( x = X , A , .0. ) )
16 6 14 1 2 4 5 15 dprdfid 
 |-  ( ph -> ( ( x e. I |-> if ( x = X , A , .0. ) ) e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } /\ ( G gsum ( x e. I |-> if ( x = X , A , .0. ) ) ) = A ) )
17 16 simprd 
 |-  ( ph -> ( G gsum ( x e. I |-> if ( x = X , A , .0. ) ) ) = A )
18 17 eqcomd 
 |-  ( ph -> A = ( G gsum ( x e. I |-> if ( x = X , A , .0. ) ) ) )
19 1 2 4 dprdub 
 |-  ( ph -> ( S ` X ) C_ ( G DProd S ) )
20 19 5 sseldd 
 |-  ( ph -> A e. ( G DProd S ) )
21 16 simpld 
 |-  ( ph -> ( x e. I |-> if ( x = X , A , .0. ) ) e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } )
22 1 2 3 20 6 14 21 dpjeq 
 |-  ( ph -> ( A = ( G gsum ( x e. I |-> if ( x = X , A , .0. ) ) ) <-> A. x e. I ( ( P ` x ) ` A ) = if ( x = X , A , .0. ) ) )
23 18 22 mpbid 
 |-  ( ph -> A. x e. I ( ( P ` x ) ` A ) = if ( x = X , A , .0. ) )
24 13 23 7 rspcdva 
 |-  ( ph -> ( ( P ` Y ) ` A ) = if ( Y = X , A , .0. ) )
25 ifnefalse 
 |-  ( Y =/= X -> if ( Y = X , A , .0. ) = .0. )
26 8 25 syl 
 |-  ( ph -> if ( Y = X , A , .0. ) = .0. )
27 24 26 eqtrd 
 |-  ( ph -> ( ( P ` Y ) ` A ) = .0. )