Description: Lemma 1 for gsum2d . (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 8-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | gsum2d.b | |
|
gsum2d.z | |
||
gsum2d.g | |
||
gsum2d.a | |
||
gsum2d.r | |
||
gsum2d.d | |
||
gsum2d.s | |
||
gsum2d.f | |
||
gsum2d.w | |
||
Assertion | gsum2dlem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gsum2d.b | |
|
2 | gsum2d.z | |
|
3 | gsum2d.g | |
|
4 | gsum2d.a | |
|
5 | gsum2d.r | |
|
6 | gsum2d.d | |
|
7 | gsum2d.s | |
|
8 | gsum2d.f | |
|
9 | gsum2d.w | |
|
10 | imaexg | |
|
11 | 4 10 | syl | |
12 | vex | |
|
13 | vex | |
|
14 | 12 13 | elimasn | |
15 | df-ov | |
|
16 | 8 | ffvelrnda | |
17 | 15 16 | eqeltrid | |
18 | 14 17 | sylan2b | |
19 | 18 | fmpttd | |
20 | 9 | fsuppimpd | |
21 | rnfi | |
|
22 | 20 21 | syl | |
23 | 14 | biimpi | |
24 | 12 13 | opelrn | |
25 | 24 | con3i | |
26 | 23 25 | anim12i | |
27 | eldif | |
|
28 | eldif | |
|
29 | 26 27 28 | 3imtr4i | |
30 | ssidd | |
|
31 | 2 | fvexi | |
32 | 31 | a1i | |
33 | 8 30 4 32 | suppssr | |
34 | 15 33 | eqtrid | |
35 | 29 34 | sylan2 | |
36 | 35 11 | suppss2 | |
37 | 22 36 | ssfid | |
38 | 1 2 3 11 19 37 | gsumcl2 | |