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

Proof

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