Metamath Proof Explorer


Theorem stoweidlem2

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 tφ
stoweidlem2.2 φfAgAtTftgtA
stoweidlem2.3 φxtTxA
stoweidlem2.4 φfAf:T
stoweidlem2.5 φE
stoweidlem2.6 φFA
Assertion stoweidlem2 φtTEFtA

Proof

Step Hyp Ref Expression
1 stoweidlem2.1 tφ
2 stoweidlem2.2 φfAgAtTftgtA
3 stoweidlem2.3 φxtTxA
4 stoweidlem2.4 φfAf:T
5 stoweidlem2.5 φE
6 stoweidlem2.6 φFA
7 simpr φtTtT
8 5 adantr φtTE
9 eqidd s=tE=E
10 9 cbvmptv sTE=tTE
11 10 fvmpt2 tTEsTEt=E
12 7 8 11 syl2anc φtTsTEt=E
13 12 eqcomd φtTE=sTEt
14 13 oveq1d φtTEFt=sTEtFt
15 1 14 mpteq2da φtTEFt=tTsTEtFt
16 id x=Ex=E
17 16 mpteq2dv x=EtTx=tTE
18 17 eleq1d x=EtTxAtTEA
19 18 imbi2d x=EφtTxAφtTEA
20 3 expcom xφtTxA
21 19 20 vtoclga EφtTEA
22 5 21 mpcom φtTEA
23 10 22 eqeltrid φsTEA
24 fveq1 f=sTEft=sTEt
25 24 oveq1d f=sTEftFt=sTEtFt
26 25 mpteq2dv f=sTEtTftFt=tTsTEtFt
27 26 eleq1d f=sTEtTftFtAtTsTEtFtA
28 27 imbi2d f=sTEφtTftFtAφtTsTEtFtA
29 6 adantr φfAFA
30 fveq1 g=Fgt=Ft
31 30 oveq2d g=Fftgt=ftFt
32 31 mpteq2dv g=FtTftgt=tTftFt
33 32 eleq1d g=FtTftgtAtTftFtA
34 33 imbi2d g=FφfAtTftgtAφfAtTftFtA
35 2 3comr gAφfAtTftgtA
36 35 3expib gAφfAtTftgtA
37 34 36 vtoclga FAφfAtTftFtA
38 29 37 mpcom φfAtTftFtA
39 38 expcom fAφtTftFtA
40 28 39 vtoclga sTEAφtTsTEtFtA
41 23 40 mpcom φtTsTEtFtA
42 15 41 eqeltrd φtTEFtA