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 eqtr3id
 |-  ( ( 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. )