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 ⊢ Ⅎ 𝑡 𝜑
stoweidlem16.2 ⊢ 𝑌 = { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) }
stoweidlem16.3 ⊢ 𝐻 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) )
stoweidlem16.4 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
stoweidlem16.5 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
Assertion stoweidlem16 ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → 𝐻 ∈ 𝑌 )

Proof

Step Hyp Ref Expression
1 stoweidlem16.1 ⊢ Ⅎ 𝑡 𝜑
2 stoweidlem16.2 ⊢ 𝑌 = { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) }
3 stoweidlem16.3 ⊢ 𝐻 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) )
4 stoweidlem16.4 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
5 stoweidlem16.5 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
6 simp1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → 𝜑 )
7 fveq1 ⊢ ( ℎ = 𝑓 → ( ℎ ‘ 𝑡 ) = ( 𝑓 ‘ 𝑡 ) )
8 7 breq2d ⊢ ( ℎ = 𝑓 → ( 0 ≤ ( ℎ ‘ 𝑡 ) ↔ 0 ≤ ( 𝑓 ‘ 𝑡 ) ) )
9 7 breq1d ⊢ ( ℎ = 𝑓 → ( ( ℎ ‘ 𝑡 ) ≤ 1 ↔ ( 𝑓 ‘ 𝑡 ) ≤ 1 ) )
10 8 9 anbi12d ⊢ ( ℎ = 𝑓 → ( ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( 𝑓 ‘ 𝑡 ) ∧ ( 𝑓 ‘ 𝑡 ) ≤ 1 ) ) )
11 10 ralbidv ⊢ ( ℎ = 𝑓 → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑓 ‘ 𝑡 ) ∧ ( 𝑓 ‘ 𝑡 ) ≤ 1 ) ) )
12 11 2 elrab2 ⊢ ( 𝑓 ∈ 𝑌 ↔ ( 𝑓 ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑓 ‘ 𝑡 ) ∧ ( 𝑓 ‘ 𝑡 ) ≤ 1 ) ) )
13 12 simplbi ⊢ ( 𝑓 ∈ 𝑌 → 𝑓 ∈ 𝐴 )
14 13 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → 𝑓 ∈ 𝐴 )
15 fveq1 ⊢ ( ℎ = 𝑔 → ( ℎ ‘ 𝑡 ) = ( 𝑔 ‘ 𝑡 ) )
16 15 breq2d ⊢ ( ℎ = 𝑔 → ( 0 ≤ ( ℎ ‘ 𝑡 ) ↔ 0 ≤ ( 𝑔 ‘ 𝑡 ) ) )
17 15 breq1d ⊢ ( ℎ = 𝑔 → ( ( ℎ ‘ 𝑡 ) ≤ 1 ↔ ( 𝑔 ‘ 𝑡 ) ≤ 1 ) )
18 16 17 anbi12d ⊢ ( ℎ = 𝑔 → ( ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( 𝑔 ‘ 𝑡 ) ∧ ( 𝑔 ‘ 𝑡 ) ≤ 1 ) ) )
19 18 ralbidv ⊢ ( ℎ = 𝑔 → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑔 ‘ 𝑡 ) ∧ ( 𝑔 ‘ 𝑡 ) ≤ 1 ) ) )
20 19 2 elrab2 ⊢ ( 𝑔 ∈ 𝑌 ↔ ( 𝑔 ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑔 ‘ 𝑡 ) ∧ ( 𝑔 ‘ 𝑡 ) ≤ 1 ) ) )
21 20 simplbi ⊢ ( 𝑔 ∈ 𝑌 → 𝑔 ∈ 𝐴 )
22 21 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → 𝑔 ∈ 𝐴 )
23 6 14 22 5 syl3anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
24 3 23 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → 𝐻 ∈ 𝐴 )
25 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 )
26 nfcv ⊢ Ⅎ 𝑡 𝐴
27 25 26 nfrabw ⊢ Ⅎ 𝑡 { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) }
28 2 27 nfcxfr ⊢ Ⅎ 𝑡 𝑌
29 28 nfcri ⊢ Ⅎ 𝑡 𝑓 ∈ 𝑌
30 28 nfcri ⊢ Ⅎ 𝑡 𝑔 ∈ 𝑌
31 1 29 30 nf3an ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 )
32 6 14 jca ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) )
33 32 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) )
34 33 4 syl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ∧ 𝑡 ∈ 𝑇 ) → 𝑓 : 𝑇 ⟶ ℝ )
35 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
36 34 35 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝑓 ‘ 𝑡 ) ∈ ℝ )
37 6 22 jca ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) )
38 eleq1w ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ∈ 𝐴 ↔ 𝑔 ∈ 𝐴 ) )
39 38 anbi2d ⊢ ( 𝑓 = 𝑔 → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) ) )
40 feq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 : 𝑇 ⟶ ℝ ↔ 𝑔 : 𝑇 ⟶ ℝ ) )
41 39 40 imbi12d ⊢ ( 𝑓 = 𝑔 → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) → 𝑔 : 𝑇 ⟶ ℝ ) ) )
42 41 4 vtoclg ⊢ ( 𝑔 ∈ 𝐴 → ( ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) → 𝑔 : 𝑇 ⟶ ℝ ) )
43 22 37 42 sylc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → 𝑔 : 𝑇 ⟶ ℝ )
44 43 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝑔 ‘ 𝑡 ) ∈ ℝ )
45 12 simprbi ⊢ ( 𝑓 ∈ 𝑌 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑓 ‘ 𝑡 ) ∧ ( 𝑓 ‘ 𝑡 ) ≤ 1 ) )
46 45 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑓 ‘ 𝑡 ) ∧ ( 𝑓 ‘ 𝑡 ) ≤ 1 ) )
47 46 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ∧ 𝑡 ∈ 𝑇 ) → ( 0 ≤ ( 𝑓 ‘ 𝑡 ) ∧ ( 𝑓 ‘ 𝑡 ) ≤ 1 ) )
48 47 simpld ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( 𝑓 ‘ 𝑡 ) )
49 20 simprbi ⊢ ( 𝑔 ∈ 𝑌 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑔 ‘ 𝑡 ) ∧ ( 𝑔 ‘ 𝑡 ) ≤ 1 ) )
50 49 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑔 ‘ 𝑡 ) ∧ ( 𝑔 ‘ 𝑡 ) ≤ 1 ) )
51 50 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ∧ 𝑡 ∈ 𝑇 ) → ( 0 ≤ ( 𝑔 ‘ 𝑡 ) ∧ ( 𝑔 ‘ 𝑡 ) ≤ 1 ) )
52 51 simpld ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( 𝑔 ‘ 𝑡 ) )
53 36 44 48 52 mulge0d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) )
54 36 44 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ∈ ℝ )
55 3 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ∈ ℝ ) → ( 𝐻 ‘ 𝑡 ) = ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) )
56 35 54 55 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐻 ‘ 𝑡 ) = ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) )
57 53 56 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( 𝐻 ‘ 𝑡 ) )
58 1red ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ∧ 𝑡 ∈ 𝑇 ) → 1 ∈ ℝ )
59 47 simprd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝑓 ‘ 𝑡 ) ≤ 1 )
60 51 simprd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝑔 ‘ 𝑡 ) ≤ 1 )
61 36 58 44 58 48 52 59 60 lemul12ad ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ≤ ( 1 · 1 ) )
62 1t1e1 ⊢ ( 1 · 1 ) = 1
63 61 62 breqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ≤ 1 )
64 56 63 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐻 ‘ 𝑡 ) ≤ 1 )
65 57 64 jca ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ∧ 𝑡 ∈ 𝑇 ) → ( 0 ≤ ( 𝐻 ‘ 𝑡 ) ∧ ( 𝐻 ‘ 𝑡 ) ≤ 1 ) )
66 65 ex ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 → ( 0 ≤ ( 𝐻 ‘ 𝑡 ) ∧ ( 𝐻 ‘ 𝑡 ) ≤ 1 ) ) )
67 31 66 ralrimi ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝐻 ‘ 𝑡 ) ∧ ( 𝐻 ‘ 𝑡 ) ≤ 1 ) )
68 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) )
69 3 68 nfcxfr ⊢ Ⅎ 𝑡 𝐻
70 69 nfeq2 ⊢ Ⅎ 𝑡 ℎ = 𝐻
71 fveq1 ⊢ ( ℎ = 𝐻 → ( ℎ ‘ 𝑡 ) = ( 𝐻 ‘ 𝑡 ) )
72 71 breq2d ⊢ ( ℎ = 𝐻 → ( 0 ≤ ( ℎ ‘ 𝑡 ) ↔ 0 ≤ ( 𝐻 ‘ 𝑡 ) ) )
73 71 breq1d ⊢ ( ℎ = 𝐻 → ( ( ℎ ‘ 𝑡 ) ≤ 1 ↔ ( 𝐻 ‘ 𝑡 ) ≤ 1 ) )
74 72 73 anbi12d ⊢ ( ℎ = 𝐻 → ( ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( 𝐻 ‘ 𝑡 ) ∧ ( 𝐻 ‘ 𝑡 ) ≤ 1 ) ) )
75 70 74 ralbid ⊢ ( ℎ = 𝐻 → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝐻 ‘ 𝑡 ) ∧ ( 𝐻 ‘ 𝑡 ) ≤ 1 ) ) )
76 75 elrab ⊢ ( 𝐻 ∈ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } ↔ ( 𝐻 ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝐻 ‘ 𝑡 ) ∧ ( 𝐻 ‘ 𝑡 ) ≤ 1 ) ) )
77 24 67 76 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → 𝐻 ∈ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } )
78 77 2 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → 𝐻 ∈ 𝑌 )