# Metamath Proof Explorer

## Theorem 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}\phantom{\rule{.4em}{0ex}}{\phi }$
stoweidlem16.2 ${⊢}{Y}=\left\{{h}\in {A}|\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)\right\}$
stoweidlem16.3 ${⊢}{H}=\left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)$
stoweidlem16.4 ${⊢}\left({\phi }\wedge {f}\in {A}\right)\to {f}:{T}⟶ℝ$
stoweidlem16.5 ${⊢}\left({\phi }\wedge {f}\in {A}\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)\in {A}$
Assertion stoweidlem16 ${⊢}\left({\phi }\wedge {f}\in {Y}\wedge {g}\in {Y}\right)\to {H}\in {Y}$

### Proof

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