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	$⊢ \underline{Ⅎ} t F$
		stoweidlem33.2	$⊢ \underline{Ⅎ} t G$
		stoweidlem33.3	$⊢ Ⅎ t φ$
		stoweidlem33.4	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
		stoweidlem33.5	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
		stoweidlem33.6	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
		stoweidlem33.7	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
	Assertion	stoweidlem33	$⊢ (φ \land F \in A \land G \in A) \to (t \in T ⟼ F (t) - G (t)) \in A$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem33.1	$⊢ \underline{Ⅎ} t F$
2		stoweidlem33.2	$⊢ \underline{Ⅎ} t G$
3		stoweidlem33.3	$⊢ Ⅎ t φ$
4		stoweidlem33.4	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
5		stoweidlem33.5	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
6		stoweidlem33.6	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
7		stoweidlem33.7	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
8		eqid	$⊢ (t \in T ⟼ F (t) - G (t)) = (t \in T ⟼ F (t) - G (t))$
9		eqid	$⊢ (t \in T ⟼ - 1) = (t \in T ⟼ - 1)$
10		eqid	$⊢ (t \in T ⟼ (t \in T ⟼ - 1) (t) G (t)) = (t \in T ⟼ (t \in T ⟼ - 1) (t) G (t))$
11	3 1 2 8 9 10 4 5 6 7	stoweidlem22	$⊢ (φ \land F \in A \land G \in A) \to (t \in T ⟼ F (t) - G (t)) \in A$