Description: Property 2 of an extension of a linear combination. (Contributed by AV, 20-Apr-2019) (Revised by AV, 30-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lincext.b | |
|
lincext.r | |
||
lincext.e | |
||
lincext.0 | |
||
lincext.z | |
||
lincext.n | |
||
lincext.f | |
||
Assertion | lincext2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lincext.b | |
|
2 | lincext.r | |
|
3 | lincext.e | |
|
4 | lincext.0 | |
|
5 | lincext.z | |
|
6 | lincext.n | |
|
7 | lincext.f | |
|
8 | fvex | |
|
9 | fvex | |
|
10 | 8 9 | ifex | |
11 | 10 7 | dmmpti | |
12 | 11 | difeq1i | |
13 | snssi | |
|
14 | 13 | 3ad2ant2 | |
15 | 14 | 3ad2ant2 | |
16 | dfss4 | |
|
17 | 15 16 | sylib | |
18 | snfi | |
|
19 | 17 18 | eqeltrdi | |
20 | 12 19 | eqeltrid | |
21 | 1 2 3 4 5 6 7 | lincext1 | |
22 | 21 | 3adant3 | |
23 | elmapfun | |
|
24 | 22 23 | syl | |
25 | elmapi | |
|
26 | 7 | fdmdifeqresdif | |
27 | 25 26 | syl | |
28 | 27 | 3ad2ant3 | |
29 | 28 | 3ad2ant2 | |
30 | simp3 | |
|
31 | 4 | fvexi | |
32 | 31 | a1i | |
33 | 20 22 24 29 30 32 | resfsupp | |