Metamath Proof Explorer

Theorem gsum2d2lem

Description: Lemma for gsum2d2 : show the function is finitely supported. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 9-Jun-2019)

Ref Expression
Hypotheses gsum2d2.b 
|- B = ( Base ` G )
gsum2d2.z 
|- .0. = ( 0g ` G )
gsum2d2.g 
|- ( ph -> G e. CMnd )
gsum2d2.a 
|- ( ph -> A e. V )
gsum2d2.r 
|- ( ( ph /\ j e. A ) -> C e. W )
gsum2d2.f 
|- ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B )
gsum2d2.u 
|- ( ph -> U e. Fin )
gsum2d2.n 
|- ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) ) -> X = .0. )
Assertion gsum2d2lem 
|- ( ph -> ( j e. A , k e. C |-> X ) finSupp .0. )

Proof

Step Hyp Ref Expression
1 gsum2d2.b 
 |-  B = ( Base ` G )
2 gsum2d2.z 
 |-  .0. = ( 0g ` G )
3 gsum2d2.g 
 |-  ( ph -> G e. CMnd )
4 gsum2d2.a 
 |-  ( ph -> A e. V )
5 gsum2d2.r 
 |-  ( ( ph /\ j e. A ) -> C e. W )
6 gsum2d2.f 
 |-  ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B )
7 gsum2d2.u 
 |-  ( ph -> U e. Fin )
8 gsum2d2.n 
 |-  ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) ) -> X = .0. )
9 eqid 
 |-  ( j e. A , k e. C |-> X ) = ( j e. A , k e. C |-> X )
10 9 mpofun 
 |-  Fun ( j e. A , k e. C |-> X )
11 10 a1i 
 |-  ( ph -> Fun ( j e. A , k e. C |-> X ) )
12 6 ralrimivva 
 |-  ( ph -> A. j e. A A. k e. C X e. B )
13 9 fmpox 
 |-  ( A. j e. A A. k e. C X e. B <-> ( j e. A , k e. C |-> X ) : U_ j e. A ( { j } X. C ) --> B )
14 12 13 sylib 
 |-  ( ph -> ( j e. A , k e. C |-> X ) : U_ j e. A ( { j } X. C ) --> B )
15 nfv 
 |-  F/ j ph
16 nfiu1 
 |-  F/_ j U_ j e. A ( { j } X. C )
17 nfcv 
 |-  F/_ j U
18 16 17 nfdif 
 |-  F/_ j ( U_ j e. A ( { j } X. C ) \ U )
19 18 nfcri 
 |-  F/ j z e. ( U_ j e. A ( { j } X. C ) \ U )
20 15 19 nfan 
 |-  F/ j ( ph /\ z e. ( U_ j e. A ( { j } X. C ) \ U ) )
21 nfmpo1 
 |-  F/_ j ( j e. A , k e. C |-> X )
22 nfcv 
 |-  F/_ j z
23 21 22 nffv 
 |-  F/_ j ( ( j e. A , k e. C |-> X ) ` z )
24 23 nfeq1 
 |-  F/ j ( ( j e. A , k e. C |-> X ) ` z ) = .0.
25 relxp 
 |-  Rel ( { j } X. C )
26 25 rgenw 
 |-  A. j e. A Rel ( { j } X. C )
27 reliun 
 |-  ( Rel U_ j e. A ( { j } X. C ) <-> A. j e. A Rel ( { j } X. C ) )
28 26 27 mpbir 
 |-  Rel U_ j e. A ( { j } X. C )
29 eldifi 
 |-  ( z e. ( U_ j e. A ( { j } X. C ) \ U ) -> z e. U_ j e. A ( { j } X. C ) )
30 29 adantl 
 |-  ( ( ph /\ z e. ( U_ j e. A ( { j } X. C ) \ U ) ) -> z e. U_ j e. A ( { j } X. C ) )
31 elrel 
 |-  ( ( Rel U_ j e. A ( { j } X. C ) /\ z e. U_ j e. A ( { j } X. C ) ) -> E. j E. k z = <. j , k >. )
32 28 30 31 sylancr 
 |-  ( ( ph /\ z e. ( U_ j e. A ( { j } X. C ) \ U ) ) -> E. j E. k z = <. j , k >. )
33 nfv 
 |-  F/ k ( ph /\ z e. ( U_ j e. A ( { j } X. C ) \ U ) )
34 nfmpo2 
 |-  F/_ k ( j e. A , k e. C |-> X )
35 nfcv 
 |-  F/_ k z
36 34 35 nffv 
 |-  F/_ k ( ( j e. A , k e. C |-> X ) ` z )
37 36 nfeq1 
 |-  F/ k ( ( j e. A , k e. C |-> X ) ` z ) = .0.
38 simprr 
 |-  ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> z = <. j , k >. )
39 38 fveq2d 
 |-  ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> ( ( j e. A , k e. C |-> X ) ` z ) = ( ( j e. A , k e. C |-> X ) ` <. j , k >. ) )
40 df-ov 
 |-  ( j ( j e. A , k e. C |-> X ) k ) = ( ( j e. A , k e. C |-> X ) ` <. j , k >. )
41 simprl 
 |-  ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> z e. ( U_ j e. A ( { j } X. C ) \ U ) )
42 38 41 eqeltrrd 
 |-  ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> <. j , k >. e. ( U_ j e. A ( { j } X. C ) \ U ) )
43 42 eldifad 
 |-  ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> <. j , k >. e. U_ j e. A ( { j } X. C ) )
44 opeliunxp 
 |-  ( <. j , k >. e. U_ j e. A ( { j } X. C ) <-> ( j e. A /\ k e. C ) )
45 43 44 sylib 
 |-  ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> ( j e. A /\ k e. C ) )
46 45 simpld 
 |-  ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> j e. A )
47 45 simprd 
 |-  ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> k e. C )
48 45 6 syldan 
 |-  ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> X e. B )
49 9 ovmpt4g 
 |-  ( ( j e. A /\ k e. C /\ X e. B ) -> ( j ( j e. A , k e. C |-> X ) k ) = X )
50 46 47 48 49 syl3anc 
 |-  ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> ( j ( j e. A , k e. C |-> X ) k ) = X )
51 40 50 syl5eqr 
 |-  ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> ( ( j e. A , k e. C |-> X ) ` <. j , k >. ) = X )
52 eldifn 
 |-  ( z e. ( U_ j e. A ( { j } X. C ) \ U ) -> -. z e. U )
53 52 ad2antrl 
 |-  ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> -. z e. U )
54 38 eleq1d 
 |-  ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> ( z e. U <-> <. j , k >. e. U ) )
55 df-br 
 |-  ( j U k <-> <. j , k >. e. U )
56 54 55 bitr4di 
 |-  ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> ( z e. U <-> j U k ) )
57 53 56 mtbid 
 |-  ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> -. j U k )
58 45 57 jca 
 |-  ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> ( ( j e. A /\ k e. C ) /\ -. j U k ) )
59 58 8 syldan 
 |-  ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> X = .0. )
60 39 51 59 3eqtrd 
 |-  ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> ( ( j e. A , k e. C |-> X ) ` z ) = .0. )
61 60 expr 
 |-  ( ( ph /\ z e. ( U_ j e. A ( { j } X. C ) \ U ) ) -> ( z = <. j , k >. -> ( ( j e. A , k e. C |-> X ) ` z ) = .0. ) )
62 33 37 61 exlimd 
 |-  ( ( ph /\ z e. ( U_ j e. A ( { j } X. C ) \ U ) ) -> ( E. k z = <. j , k >. -> ( ( j e. A , k e. C |-> X ) ` z ) = .0. ) )
63 20 24 32 62 exlimimdd 
 |-  ( ( ph /\ z e. ( U_ j e. A ( { j } X. C ) \ U ) ) -> ( ( j e. A , k e. C |-> X ) ` z ) = .0. )
64 14 63 suppss 
 |-  ( ph -> ( ( j e. A , k e. C |-> X ) supp .0. ) C_ U )
65 7 64 ssfid 
 |-  ( ph -> ( ( j e. A , k e. C |-> X ) supp .0. ) e. Fin )
66 5 ralrimiva 
 |-  ( ph -> A. j e. A C e. W )
67 9 mpoexxg 
 |-  ( ( A e. V /\ A. j e. A C e. W ) -> ( j e. A , k e. C |-> X ) e. _V )
68 4 66 67 syl2anc 
 |-  ( ph -> ( j e. A , k e. C |-> X ) e. _V )
69 2 fvexi 
 |-  .0. e. _V
70 69 a1i 
 |-  ( ph -> .0. e. _V )
71 isfsupp 
 |-  ( ( ( j e. A , k e. C |-> X ) e. _V /\ .0. e. _V ) -> ( ( j e. A , k e. C |-> X ) finSupp .0. <-> ( Fun ( j e. A , k e. C |-> X ) /\ ( ( j e. A , k e. C |-> X ) supp .0. ) e. Fin ) ) )
72 68 70 71 syl2anc 
 |-  ( ph -> ( ( j e. A , k e. C |-> X ) finSupp .0. <-> ( Fun ( j e. A , k e. C |-> X ) /\ ( ( j e. A , k e. C |-> X ) supp .0. ) e. Fin ) ) )
73 11 65 72 mpbir2and 
 |-  ( ph -> ( j e. A , k e. C |-> X ) finSupp .0. )