Metamath Proof Explorer


Theorem gsum2dlem1

Description: Lemma 1 for gsum2d . (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 8-Jun-2019)

Ref Expression
Hypotheses gsum2d.b B=BaseG
gsum2d.z 0˙=0G
gsum2d.g φGCMnd
gsum2d.a φAV
gsum2d.r φRelA
gsum2d.d φDW
gsum2d.s φdomAD
gsum2d.f φF:AB
gsum2d.w φfinSupp0˙F
Assertion gsum2dlem1 φGkAjjFkB

Proof

Step Hyp Ref Expression
1 gsum2d.b B=BaseG
2 gsum2d.z 0˙=0G
3 gsum2d.g φGCMnd
4 gsum2d.a φAV
5 gsum2d.r φRelA
6 gsum2d.d φDW
7 gsum2d.s φdomAD
8 gsum2d.f φF:AB
9 gsum2d.w φfinSupp0˙F
10 imaexg AVAjV
11 4 10 syl φAjV
12 vex jV
13 vex kV
14 12 13 elimasn kAjjkA
15 df-ov jFk=Fjk
16 8 ffvelrnda φjkAFjkB
17 15 16 eqeltrid φjkAjFkB
18 14 17 sylan2b φkAjjFkB
19 18 fmpttd φkAjjFk:AjB
20 9 fsuppimpd φFsupp0˙Fin
21 rnfi Fsupp0˙Finransupp0˙FFin
22 20 21 syl φransupp0˙FFin
23 14 biimpi kAjjkA
24 12 13 opelrn jksupp0˙Fkransupp0˙F
25 24 con3i ¬kransupp0˙F¬jksupp0˙F
26 23 25 anim12i kAj¬kransupp0˙FjkA¬jksupp0˙F
27 eldif kAjransupp0˙FkAj¬kransupp0˙F
28 eldif jkAsupp0˙FjkA¬jksupp0˙F
29 26 27 28 3imtr4i kAjransupp0˙FjkAsupp0˙F
30 ssidd φFsupp0˙Fsupp0˙
31 2 fvexi 0˙V
32 31 a1i φ0˙V
33 8 30 4 32 suppssr φjkAsupp0˙FFjk=0˙
34 15 33 eqtrid φjkAsupp0˙FjFk=0˙
35 29 34 sylan2 φkAjransupp0˙FjFk=0˙
36 35 11 suppss2 φkAjjFksupp0˙ransupp0˙F
37 22 36 ssfid φkAjjFksupp0˙Fin
38 1 2 3 11 19 37 gsumcl2 φGkAjjFkB