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