Metamath Proof Explorer

Theorem dprdfid

Description: A function mapping all but one arguments to zero sums to the value of this argument in a direct product. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 14-Jul-2019)

Ref Expression
Hypotheses eldprdi.0 
|- .0. = ( 0g ` G )
eldprdi.w 
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
eldprdi.1 
|- ( ph -> G dom DProd S )
eldprdi.2 
|- ( ph -> dom S = I )
dprdfid.3 
|- ( ph -> X e. I )
dprdfid.4 
|- ( ph -> A e. ( S ` X ) )
dprdfid.f 
|- F = ( n e. I |-> if ( n = X , A , .0. ) )
Assertion dprdfid 
|- ( ph -> ( F e. W /\ ( G gsum F ) = A ) )

Proof

Step Hyp Ref Expression
1 eldprdi.0 
 |-  .0. = ( 0g ` G )
2 eldprdi.w 
 |-  W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
3 eldprdi.1 
 |-  ( ph -> G dom DProd S )
4 eldprdi.2 
 |-  ( ph -> dom S = I )
5 dprdfid.3 
 |-  ( ph -> X e. I )
6 dprdfid.4 
 |-  ( ph -> A e. ( S ` X ) )
7 dprdfid.f 
 |-  F = ( n e. I |-> if ( n = X , A , .0. ) )
8 6 ad2antrr 
 |-  ( ( ( ph /\ n e. I ) /\ n = X ) -> A e. ( S ` X ) )
9 simpr 
 |-  ( ( ( ph /\ n e. I ) /\ n = X ) -> n = X )
10 9 fveq2d 
 |-  ( ( ( ph /\ n e. I ) /\ n = X ) -> ( S ` n ) = ( S ` X ) )
11 8 10 eleqtrrd 
 |-  ( ( ( ph /\ n e. I ) /\ n = X ) -> A e. ( S ` n ) )
12 3 4 dprdf2 
 |-  ( ph -> S : I --> ( SubGrp ` G ) )
13 12 ffvelcdmda 
 |-  ( ( ph /\ n e. I ) -> ( S ` n ) e. ( SubGrp ` G ) )
14 1 subg0cl 
 |-  ( ( S ` n ) e. ( SubGrp ` G ) -> .0. e. ( S ` n ) )
15 13 14 syl 
 |-  ( ( ph /\ n e. I ) -> .0. e. ( S ` n ) )
16 15 adantr 
 |-  ( ( ( ph /\ n e. I ) /\ -. n = X ) -> .0. e. ( S ` n ) )
17 11 16 ifclda 
 |-  ( ( ph /\ n e. I ) -> if ( n = X , A , .0. ) e. ( S ` n ) )
18 3 4 dprddomcld 
 |-  ( ph -> I e. _V )
19 1 fvexi 
 |-  .0. e. _V
20 19 a1i 
 |-  ( ph -> .0. e. _V )
21 eqid 
 |-  ( n e. I |-> if ( n = X , A , .0. ) ) = ( n e. I |-> if ( n = X , A , .0. ) )
22 18 20 21 sniffsupp 
 |-  ( ph -> ( n e. I |-> if ( n = X , A , .0. ) ) finSupp .0. )
23 2 3 4 17 22 dprdwd 
 |-  ( ph -> ( n e. I |-> if ( n = X , A , .0. ) ) e. W )
24 7 23 eqeltrid 
 |-  ( ph -> F e. W )
25 eqid 
 |-  ( Base ` G ) = ( Base ` G )
26 dprdgrp 
 |-  ( G dom DProd S -> G e. Grp )
27 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
28 3 26 27 3syl 
 |-  ( ph -> G e. Mnd )
29 2 3 4 24 25 dprdff 
 |-  ( ph -> F : I --> ( Base ` G ) )
30 7 oveq1i 
 |-  ( F supp .0. ) = ( ( n e. I |-> if ( n = X , A , .0. ) ) supp .0. )
31 eldifsni 
 |-  ( n e. ( I \ { X } ) -> n =/= X )
32 31 adantl 
 |-  ( ( ph /\ n e. ( I \ { X } ) ) -> n =/= X )
33 ifnefalse 
 |-  ( n =/= X -> if ( n = X , A , .0. ) = .0. )
34 32 33 syl 
 |-  ( ( ph /\ n e. ( I \ { X } ) ) -> if ( n = X , A , .0. ) = .0. )
35 34 18 suppss2 
 |-  ( ph -> ( ( n e. I |-> if ( n = X , A , .0. ) ) supp .0. ) C_ { X } )
36 30 35 eqsstrid 
 |-  ( ph -> ( F supp .0. ) C_ { X } )
37 25 1 28 18 5 29 36 gsumpt 
 |-  ( ph -> ( G gsum F ) = ( F ` X ) )
38 iftrue 
 |-  ( n = X -> if ( n = X , A , .0. ) = A )
39 7 38 5 6 fvmptd3 
 |-  ( ph -> ( F ` X ) = A )
40 37 39 eqtrd 
 |-  ( ph -> ( G gsum F ) = A )
41 24 40 jca 
 |-  ( ph -> ( F e. W /\ ( G gsum F ) = A ) )