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 | ⊢ Ⅎ 𝑡 𝐹 | |
stoweidlem33.2 | ⊢ Ⅎ 𝑡 𝐺 | ||
stoweidlem33.3 | ⊢ Ⅎ 𝑡 𝜑 | ||
stoweidlem33.4 | ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) | ||
stoweidlem33.5 | ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) | ||
stoweidlem33.6 | ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) | ||
stoweidlem33.7 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 ) | ||
Assertion | stoweidlem33 | ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | stoweidlem33.1 | ⊢ Ⅎ 𝑡 𝐹 | |
2 | stoweidlem33.2 | ⊢ Ⅎ 𝑡 𝐺 | |
3 | stoweidlem33.3 | ⊢ Ⅎ 𝑡 𝜑 | |
4 | stoweidlem33.4 | ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) | |
5 | stoweidlem33.5 | ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) | |
6 | stoweidlem33.6 | ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) | |
7 | stoweidlem33.7 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 ) | |
8 | eqid | ⊢ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) ) | |
9 | eqid | ⊢ ( 𝑡 ∈ 𝑇 ↦ - 1 ) = ( 𝑡 ∈ 𝑇 ↦ - 1 ) | |
10 | eqid | ⊢ ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ - 1 ) ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ - 1 ) ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ) | |
11 | 3 1 2 8 9 10 4 5 6 7 | stoweidlem22 | ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 ) |