stoweidlem16

Description: Lemma for stoweid . The subset Y of functions in the algebra A , with values in [ 0 , 1 ], is closed under multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem16.1	$⊢ Ⅎ t φ$
	stoweidlem16.2	$⊢ Y = \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
	stoweidlem16.3	$⊢ H = (t \in T ⟼ f (t) g (t))$
	stoweidlem16.4	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
	stoweidlem16.5	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
Assertion	stoweidlem16	$⊢ (φ \land f \in Y \land g \in Y) \to H \in Y$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem16.1	$⊢ Ⅎ t φ$
2		stoweidlem16.2	$⊢ Y = \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
3		stoweidlem16.3	$⊢ H = (t \in T ⟼ f (t) g (t))$
4		stoweidlem16.4	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
5		stoweidlem16.5	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
6		simp1	$⊢ (φ \land f \in Y \land g \in Y) \to φ$
7		fveq1	$⊢ h = f \to h (t) = f (t)$
8	7	breq2d	$⊢ h = f \to (0 \leq h (t) \leftrightarrow 0 \leq f (t))$
9	7	breq1d	$⊢ h = f \to (h (t) \leq 1 \leftrightarrow f (t) \leq 1)$
10	8 9	anbi12d	$⊢ h = f \to ((0 \leq h (t) \land h (t) \leq 1) \leftrightarrow (0 \leq f (t) \land f (t) \leq 1))$
11	10	ralbidv	$⊢ h = f \to (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \leftrightarrow \forall t \in T (0 \leq f (t) \land f (t) \leq 1))$
12	11 2	elrab2	$⊢ f \in Y \leftrightarrow (f \in A \land \forall t \in T (0 \leq f (t) \land f (t) \leq 1))$
13	12	simplbi	$⊢ f \in Y \to f \in A$
14	13	3ad2ant2	$⊢ (φ \land f \in Y \land g \in Y) \to f \in A$
15		fveq1	$⊢ h = g \to h (t) = g (t)$
16	15	breq2d	$⊢ h = g \to (0 \leq h (t) \leftrightarrow 0 \leq g (t))$
17	15	breq1d	$⊢ h = g \to (h (t) \leq 1 \leftrightarrow g (t) \leq 1)$
18	16 17	anbi12d	$⊢ h = g \to ((0 \leq h (t) \land h (t) \leq 1) \leftrightarrow (0 \leq g (t) \land g (t) \leq 1))$
19	18	ralbidv	$⊢ h = g \to (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \leftrightarrow \forall t \in T (0 \leq g (t) \land g (t) \leq 1))$
20	19 2	elrab2	$⊢ g \in Y \leftrightarrow (g \in A \land \forall t \in T (0 \leq g (t) \land g (t) \leq 1))$
21	20	simplbi	$⊢ g \in Y \to g \in A$
22	21	3ad2ant3	$⊢ (φ \land f \in Y \land g \in Y) \to g \in A$
23	6 14 22 5	syl3anc	$⊢ (φ \land f \in Y \land g \in Y) \to (t \in T ⟼ f (t) g (t)) \in A$
24	3 23	eqeltrid	$⊢ (φ \land f \in Y \land g \in Y) \to H \in A$
25		nfra1	$⊢ Ⅎ t \forall t \in T (0 \leq h (t) \land h (t) \leq 1)$
26		nfcv	$⊢ \underline{Ⅎ} t A$
27	25 26	nfrabw	$⊢ \underline{Ⅎ} t \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
28	2 27	nfcxfr	$⊢ \underline{Ⅎ} t Y$
29	28	nfcri	$⊢ Ⅎ t f \in Y$
30	28	nfcri	$⊢ Ⅎ t g \in Y$
31	1 29 30	nf3an	$⊢ Ⅎ t (φ \land f \in Y \land g \in Y)$
32	6 14	jca	$⊢ (φ \land f \in Y \land g \in Y) \to (φ \land f \in A)$
33	32	adantr	$⊢ ((φ \land f \in Y \land g \in Y) \land t \in T) \to (φ \land f \in A)$
34	33 4	syl	$⊢ ((φ \land f \in Y \land g \in Y) \land t \in T) \to f : T ⟶ ℝ$
35		simpr	$⊢ ((φ \land f \in Y \land g \in Y) \land t \in T) \to t \in T$
36	34 35	ffvelcdmd	$⊢ ((φ \land f \in Y \land g \in Y) \land t \in T) \to f (t) \in ℝ$
37	6 22	jca	$⊢ (φ \land f \in Y \land g \in Y) \to (φ \land g \in A)$
38		eleq1w	$⊢ f = g \to (f \in A \leftrightarrow g \in A)$
39	38	anbi2d	$⊢ f = g \to ((φ \land f \in A) \leftrightarrow (φ \land g \in A))$
40		feq1	$⊢ f = g \to (f : T ⟶ ℝ \leftrightarrow g : T ⟶ ℝ)$
41	39 40	imbi12d	$⊢ f = g \to (((φ \land f \in A) \to f : T ⟶ ℝ) \leftrightarrow ((φ \land g \in A) \to g : T ⟶ ℝ))$
42	41 4	vtoclg	$⊢ g \in A \to ((φ \land g \in A) \to g : T ⟶ ℝ)$
43	22 37 42	sylc	$⊢ (φ \land f \in Y \land g \in Y) \to g : T ⟶ ℝ$
44	43	ffvelcdmda	$⊢ ((φ \land f \in Y \land g \in Y) \land t \in T) \to g (t) \in ℝ$
45	12	simprbi	$⊢ f \in Y \to \forall t \in T (0 \leq f (t) \land f (t) \leq 1)$
46	45	3ad2ant2	$⊢ (φ \land f \in Y \land g \in Y) \to \forall t \in T (0 \leq f (t) \land f (t) \leq 1)$
47	46	r19.21bi	$⊢ ((φ \land f \in Y \land g \in Y) \land t \in T) \to (0 \leq f (t) \land f (t) \leq 1)$
48	47	simpld	$⊢ ((φ \land f \in Y \land g \in Y) \land t \in T) \to 0 \leq f (t)$
49	20	simprbi	$⊢ g \in Y \to \forall t \in T (0 \leq g (t) \land g (t) \leq 1)$
50	49	3ad2ant3	$⊢ (φ \land f \in Y \land g \in Y) \to \forall t \in T (0 \leq g (t) \land g (t) \leq 1)$
51	50	r19.21bi	$⊢ ((φ \land f \in Y \land g \in Y) \land t \in T) \to (0 \leq g (t) \land g (t) \leq 1)$
52	51	simpld	$⊢ ((φ \land f \in Y \land g \in Y) \land t \in T) \to 0 \leq g (t)$
53	36 44 48 52	mulge0d	$⊢ ((φ \land f \in Y \land g \in Y) \land t \in T) \to 0 \leq f (t) g (t)$
54	36 44	remulcld	$⊢ ((φ \land f \in Y \land g \in Y) \land t \in T) \to f (t) g (t) \in ℝ$
55	3	fvmpt2	$⊢ (t \in T \land f (t) g (t) \in ℝ) \to H (t) = f (t) g (t)$
56	35 54 55	syl2anc	$⊢ ((φ \land f \in Y \land g \in Y) \land t \in T) \to H (t) = f (t) g (t)$
57	53 56	breqtrrd	$⊢ ((φ \land f \in Y \land g \in Y) \land t \in T) \to 0 \leq H (t)$
58		1red	$⊢ ((φ \land f \in Y \land g \in Y) \land t \in T) \to 1 \in ℝ$
59	47	simprd	$⊢ ((φ \land f \in Y \land g \in Y) \land t \in T) \to f (t) \leq 1$
60	51	simprd	$⊢ ((φ \land f \in Y \land g \in Y) \land t \in T) \to g (t) \leq 1$
61	36 58 44 58 48 52 59 60	lemul12ad	$⊢ ((φ \land f \in Y \land g \in Y) \land t \in T) \to f (t) g (t) \leq 1 \cdot 1$
62		1t1e1	$⊢ 1 \cdot 1 = 1$
63	61 62	breqtrdi	$⊢ ((φ \land f \in Y \land g \in Y) \land t \in T) \to f (t) g (t) \leq 1$
64	56 63	eqbrtrd	$⊢ ((φ \land f \in Y \land g \in Y) \land t \in T) \to H (t) \leq 1$
65	57 64	jca	$⊢ ((φ \land f \in Y \land g \in Y) \land t \in T) \to (0 \leq H (t) \land H (t) \leq 1)$
66	65	ex	$⊢ (φ \land f \in Y \land g \in Y) \to (t \in T \to (0 \leq H (t) \land H (t) \leq 1))$
67	31 66	ralrimi	$⊢ (φ \land f \in Y \land g \in Y) \to \forall t \in T (0 \leq H (t) \land H (t) \leq 1)$
68		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ f (t) g (t))$
69	3 68	nfcxfr	$⊢ \underline{Ⅎ} t H$
70	69	nfeq2	$⊢ Ⅎ t h = H$
71		fveq1	$⊢ h = H \to h (t) = H (t)$
72	71	breq2d	$⊢ h = H \to (0 \leq h (t) \leftrightarrow 0 \leq H (t))$
73	71	breq1d	$⊢ h = H \to (h (t) \leq 1 \leftrightarrow H (t) \leq 1)$
74	72 73	anbi12d	$⊢ h = H \to ((0 \leq h (t) \land h (t) \leq 1) \leftrightarrow (0 \leq H (t) \land H (t) \leq 1))$
75	70 74	ralbid	$⊢ h = H \to (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \leftrightarrow \forall t \in T (0 \leq H (t) \land H (t) \leq 1))$
76	75	elrab	$⊢ H \in \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\} \leftrightarrow (H \in A \land \forall t \in T (0 \leq H (t) \land H (t) \leq 1))$
77	24 67 76	sylanbrc	$⊢ (φ \land f \in Y \land g \in Y) \to H \in \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
78	77 2	eleqtrrdi	$⊢ (φ \land f \in Y \land g \in Y) \to H \in Y$

Metamath Proof Explorer

Theorem stoweidlem16

Proof