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 ˙ = 0 G
gsum2d2.g φ G CMnd
gsum2d2.a φ A V
gsum2d2.r φ j A C W
gsum2d2.f φ j A k C X B
gsum2d2.u φ U Fin
gsum2d2.n φ j A k C ¬ j U k X = 0 ˙
Assertion gsum2d2lem φ finSupp 0 ˙ j A , k C X

Proof

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