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