Description: lemma for stoweid : here we prove that the subalgebra of continuous functions, which contains constant functions, is closed under scaling. (Contributed by Glauco Siliprandi, 20-Apr-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | stoweidlem2.1 | |
|
stoweidlem2.2 | |
||
stoweidlem2.3 | |
||
stoweidlem2.4 | |
||
stoweidlem2.5 | |
||
stoweidlem2.6 | |
||
Assertion | stoweidlem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | stoweidlem2.1 | |
|
2 | stoweidlem2.2 | |
|
3 | stoweidlem2.3 | |
|
4 | stoweidlem2.4 | |
|
5 | stoweidlem2.5 | |
|
6 | stoweidlem2.6 | |
|
7 | simpr | |
|
8 | 5 | adantr | |
9 | eqidd | |
|
10 | 9 | cbvmptv | |
11 | 10 | fvmpt2 | |
12 | 7 8 11 | syl2anc | |
13 | 12 | eqcomd | |
14 | 13 | oveq1d | |
15 | 1 14 | mpteq2da | |
16 | id | |
|
17 | 16 | mpteq2dv | |
18 | 17 | eleq1d | |
19 | 18 | imbi2d | |
20 | 3 | expcom | |
21 | 19 20 | vtoclga | |
22 | 5 21 | mpcom | |
23 | 10 22 | eqeltrid | |
24 | fveq1 | |
|
25 | 24 | oveq1d | |
26 | 25 | mpteq2dv | |
27 | 26 | eleq1d | |
28 | 27 | imbi2d | |
29 | 6 | adantr | |
30 | fveq1 | |
|
31 | 30 | oveq2d | |
32 | 31 | mpteq2dv | |
33 | 32 | eleq1d | |
34 | 33 | imbi2d | |
35 | 2 | 3comr | |
36 | 35 | 3expib | |
37 | 34 36 | vtoclga | |
38 | 29 37 | mpcom | |
39 | 38 | expcom | |
40 | 28 39 | vtoclga | |
41 | 23 40 | mpcom | |
42 | 15 41 | eqeltrd | |