Metamath Proof Explorer

Theorem stoweidlem33

Description: If a set of real functions from a common domain is closed under addition, multiplication and it contains constants, then it is closed under subtraction. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem33.1 ⊢Ⅎ_tF
stoweidlem33.2 ⊢Ⅎ_tG
stoweidlem33.3 ⊢Ⅎtφ
stoweidlem33.4 ⊢φ∧f∈A→f:T⟶ℝ
stoweidlem33.5 ⊢φ∧f∈A∧g∈A→t∈T⟼f⁡t+g⁡t∈A
stoweidlem33.6 ⊢φ∧f∈A∧g∈A→t∈T⟼f⁡t⁢g⁡t∈A
stoweidlem33.7 ⊢φ∧x∈ℝ→t∈T⟼x∈A
Assertion stoweidlem33 ⊢φ∧F∈A∧G∈A→t∈T⟼F⁡t−G⁡t∈A

Proof

Step Hyp Ref Expression
1 stoweidlem33.1 ⊢Ⅎ_tF
2 stoweidlem33.2 ⊢Ⅎ_tG
3 stoweidlem33.3 ⊢Ⅎtφ
4 stoweidlem33.4 ⊢φ∧f∈A→f:T⟶ℝ
5 stoweidlem33.5 ⊢φ∧f∈A∧g∈A→t∈T⟼f⁡t+g⁡t∈A
6 stoweidlem33.6 ⊢φ∧f∈A∧g∈A→t∈T⟼f⁡t⁢g⁡t∈A
7 stoweidlem33.7 ⊢φ∧x∈ℝ→t∈T⟼x∈A
8 eqid ⊢t∈T⟼F⁡t−G⁡t=t∈T⟼F⁡t−G⁡t
9 eqid ⊢t∈T⟼−1=t∈T⟼−1
10 eqid ⊢t∈T⟼t∈T⟼−1⁡t⁢G⁡t=t∈T⟼t∈T⟼−1⁡t⁢G⁡t
11 3 1 2 8 9 10 4 5 6 7 stoweidlem22 ⊢φ∧F∈A∧G∈A→t∈T⟼F⁡t−G⁡t∈A