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 𝑡 𝜑
stoweidlem2.2 ( ( 𝜑𝑓𝐴𝑔𝐴 ) → ( 𝑡𝑇 ↦ ( ( 𝑓𝑡 ) · ( 𝑔𝑡 ) ) ) ∈ 𝐴 )
stoweidlem2.3 ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝑡𝑇𝑥 ) ∈ 𝐴 )
stoweidlem2.4 ( ( 𝜑𝑓𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
stoweidlem2.5 ( 𝜑𝐸 ∈ ℝ )
stoweidlem2.6 ( 𝜑𝐹𝐴 )
Assertion stoweidlem2 ( 𝜑 → ( 𝑡𝑇 ↦ ( 𝐸 · ( 𝐹𝑡 ) ) ) ∈ 𝐴 )

Proof

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 ( 𝜑 → ( 𝑡𝑇 ↦ ( 𝐸 · ( 𝐹𝑡 ) ) ) ∈ 𝐴 )