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φ
stoweidlem16.2 ⊢Y=h∈A|∀t∈T0≤h⁡t∧h⁡t≤1
stoweidlem16.3 ⊢H=t∈T⟼f⁡t⁢g⁡t
stoweidlem16.4 ⊢φ∧f∈A→f:T⟶ℝ
stoweidlem16.5 ⊢φ∧f∈A∧g∈A→t∈T⟼f⁡t⁢g⁡t∈A
Assertion stoweidlem16 ⊢φ∧f∈Y∧g∈Y→H∈Y

Proof

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