stoweidlem2

Description: lemma for stoweid : here we prove that the subalgebra of continuous functions, which contains constant functions, is closed under scaling. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem2.1	$⊢ Ⅎ t φ$
	stoweidlem2.2	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem2.3	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
	stoweidlem2.4	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
	stoweidlem2.5	$⊢ φ \to E \in ℝ$
	stoweidlem2.6	$⊢ φ \to F \in A$
Assertion	stoweidlem2	$⊢ φ \to (t \in T ⟼ E F (t)) \in A$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem2.1	$⊢ Ⅎ t φ$
2		stoweidlem2.2	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
3		stoweidlem2.3	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
4		stoweidlem2.4	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
5		stoweidlem2.5	$⊢ φ \to E \in ℝ$
6		stoweidlem2.6	$⊢ φ \to F \in A$
7		simpr	$⊢ (φ \land t \in T) \to t \in T$
8	5	adantr	$⊢ (φ \land t \in T) \to E \in ℝ$
9		eqidd	$⊢ s = t \to E = E$
10	9	cbvmptv	$⊢ (s \in T ⟼ E) = (t \in T ⟼ E)$
11	10	fvmpt2	$⊢ (t \in T \land E \in ℝ) \to (s \in T ⟼ E) (t) = E$
12	7 8 11	syl2anc	$⊢ (φ \land t \in T) \to (s \in T ⟼ E) (t) = E$
13	12	eqcomd	$⊢ (φ \land t \in T) \to E = (s \in T ⟼ E) (t)$
14	13	oveq1d	$⊢ (φ \land t \in T) \to E F (t) = (s \in T ⟼ E) (t) F (t)$
15	1 14	mpteq2da	$⊢ φ \to (t \in T ⟼ E F (t)) = (t \in T ⟼ (s \in T ⟼ E) (t) F (t))$
16		id	$⊢ x = E \to x = E$
17	16	mpteq2dv	$⊢ x = E \to (t \in T ⟼ x) = (t \in T ⟼ E)$
18	17	eleq1d	$⊢ x = E \to ((t \in T ⟼ x) \in A \leftrightarrow (t \in T ⟼ E) \in A)$
19	18	imbi2d	$⊢ x = E \to ((φ \to (t \in T ⟼ x) \in A) \leftrightarrow (φ \to (t \in T ⟼ E) \in A))$
20	3	expcom	$⊢ x \in ℝ \to (φ \to (t \in T ⟼ x) \in A)$
21	19 20	vtoclga	$⊢ E \in ℝ \to (φ \to (t \in T ⟼ E) \in A)$
22	5 21	mpcom	$⊢ φ \to (t \in T ⟼ E) \in A$
23	10 22	eqeltrid	$⊢ φ \to (s \in T ⟼ E) \in A$
24		fveq1	$⊢ f = (s \in T ⟼ E) \to f (t) = (s \in T ⟼ E) (t)$
25	24	oveq1d	$⊢ f = (s \in T ⟼ E) \to f (t) F (t) = (s \in T ⟼ E) (t) F (t)$
26	25	mpteq2dv	$⊢ f = (s \in T ⟼ E) \to (t \in T ⟼ f (t) F (t)) = (t \in T ⟼ (s \in T ⟼ E) (t) F (t))$
27	26	eleq1d	$⊢ f = (s \in T ⟼ E) \to ((t \in T ⟼ f (t) F (t)) \in A \leftrightarrow (t \in T ⟼ (s \in T ⟼ E) (t) F (t)) \in A)$
28	27	imbi2d	$⊢ f = (s \in T ⟼ E) \to ((φ \to (t \in T ⟼ f (t) F (t)) \in A) \leftrightarrow (φ \to (t \in T ⟼ (s \in T ⟼ E) (t) F (t)) \in A))$
29	6	adantr	$⊢ (φ \land f \in A) \to F \in A$
30		fveq1	$⊢ g = F \to g (t) = F (t)$
31	30	oveq2d	$⊢ g = F \to f (t) g (t) = f (t) F (t)$
32	31	mpteq2dv	$⊢ g = F \to (t \in T ⟼ f (t) g (t)) = (t \in T ⟼ f (t) F (t))$
33	32	eleq1d	$⊢ g = F \to ((t \in T ⟼ f (t) g (t)) \in A \leftrightarrow (t \in T ⟼ f (t) F (t)) \in A)$
34	33	imbi2d	$⊢ g = F \to (((φ \land f \in A) \to (t \in T ⟼ f (t) g (t)) \in A) \leftrightarrow ((φ \land f \in A) \to (t \in T ⟼ f (t) F (t)) \in A))$
35	2	3comr	$⊢ (g \in A \land φ \land f \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
36	35	3expib	$⊢ g \in A \to ((φ \land f \in A) \to (t \in T ⟼ f (t) g (t)) \in A)$
37	34 36	vtoclga	$⊢ F \in A \to ((φ \land f \in A) \to (t \in T ⟼ f (t) F (t)) \in A)$
38	29 37	mpcom	$⊢ (φ \land f \in A) \to (t \in T ⟼ f (t) F (t)) \in A$
39	38	expcom	$⊢ f \in A \to (φ \to (t \in T ⟼ f (t) F (t)) \in A)$
40	28 39	vtoclga	$⊢ (s \in T ⟼ E) \in A \to (φ \to (t \in T ⟼ (s \in T ⟼ E) (t) F (t)) \in A)$
41	23 40	mpcom	$⊢ φ \to (t \in T ⟼ (s \in T ⟼ E) (t) F (t)) \in A$
42	15 41	eqeltrd	$⊢ φ \to (t \in T ⟼ E F (t)) \in A$

Metamath Proof Explorer

Theorem stoweidlem2

Proof