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 
|- F/ t ph
stoweidlem16.2 
|- Y = { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }
stoweidlem16.3 
|- H = ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) )
stoweidlem16.4 
|- ( ( ph /\ f e. A ) -> f : T --> RR )
stoweidlem16.5 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
Assertion stoweidlem16 
|- ( ( ph /\ f e. Y /\ g e. Y ) -> H e. Y )

Proof

Step Hyp Ref Expression
1 stoweidlem16.1 
 |-  F/ t ph
2 stoweidlem16.2 
 |-  Y = { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }
3 stoweidlem16.3 
 |-  H = ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) )
4 stoweidlem16.4 
 |-  ( ( ph /\ f e. A ) -> f : T --> RR )
5 stoweidlem16.5 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
6 simp1 
 |-  ( ( ph /\ f e. Y /\ g e. Y ) -> ph )
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 -> ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> A. t e. T ( 0 <_ ( f ` t ) /\ ( f ` t ) <_ 1 ) ) )
12 11 2 elrab2 
 |-  ( f e. Y <-> ( f e. A /\ A. t e. T ( 0 <_ ( f ` t ) /\ ( f ` t ) <_ 1 ) ) )
13 12 simplbi 
 |-  ( f e. Y -> f e. A )
14 13 3ad2ant2 
 |-  ( ( ph /\ f e. Y /\ g e. Y ) -> f e. 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 -> ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> A. t e. T ( 0 <_ ( g ` t ) /\ ( g ` t ) <_ 1 ) ) )
20 19 2 elrab2 
 |-  ( g e. Y <-> ( g e. A /\ A. t e. T ( 0 <_ ( g ` t ) /\ ( g ` t ) <_ 1 ) ) )
21 20 simplbi 
 |-  ( g e. Y -> g e. A )
22 21 3ad2ant3 
 |-  ( ( ph /\ f e. Y /\ g e. Y ) -> g e. A )
23 6 14 22 5 syl3anc 
 |-  ( ( ph /\ f e. Y /\ g e. Y ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
24 3 23 eqeltrid 
 |-  ( ( ph /\ f e. Y /\ g e. Y ) -> H e. A )
25 nfra1 
 |-  F/ t A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 )
26 nfcv 
 |-  F/_ t A
27 25 26 nfrabw 
 |-  F/_ t { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }
28 2 27 nfcxfr 
 |-  F/_ t Y
29 28 nfcri 
 |-  F/ t f e. Y
30 28 nfcri 
 |-  F/ t g e. Y
31 1 29 30 nf3an 
 |-  F/ t ( ph /\ f e. Y /\ g e. Y )
32 6 14 jca 
 |-  ( ( ph /\ f e. Y /\ g e. Y ) -> ( ph /\ f e. A ) )
33 32 adantr 
 |-  ( ( ( ph /\ f e. Y /\ g e. Y ) /\ t e. T ) -> ( ph /\ f e. A ) )
34 33 4 syl 
 |-  ( ( ( ph /\ f e. Y /\ g e. Y ) /\ t e. T ) -> f : T --> RR )
35 simpr 
 |-  ( ( ( ph /\ f e. Y /\ g e. Y ) /\ t e. T ) -> t e. T )
36 34 35 ffvelrnd 
 |-  ( ( ( ph /\ f e. Y /\ g e. Y ) /\ t e. T ) -> ( f ` t ) e. RR )
37 6 22 jca 
 |-  ( ( ph /\ f e. Y /\ g e. Y ) -> ( ph /\ g e. A ) )
38 eleq1w 
 |-  ( f = g -> ( f e. A <-> g e. A ) )
39 38 anbi2d 
 |-  ( f = g -> ( ( ph /\ f e. A ) <-> ( ph /\ g e. A ) ) )
40 feq1 
 |-  ( f = g -> ( f : T --> RR <-> g : T --> RR ) )
41 39 40 imbi12d 
 |-  ( f = g -> ( ( ( ph /\ f e. A ) -> f : T --> RR ) <-> ( ( ph /\ g e. A ) -> g : T --> RR ) ) )
42 41 4 vtoclg 
 |-  ( g e. A -> ( ( ph /\ g e. A ) -> g : T --> RR ) )
43 22 37 42 sylc 
 |-  ( ( ph /\ f e. Y /\ g e. Y ) -> g : T --> RR )
44 43 ffvelrnda 
 |-  ( ( ( ph /\ f e. Y /\ g e. Y ) /\ t e. T ) -> ( g ` t ) e. RR )
45 12 simprbi 
 |-  ( f e. Y -> A. t e. T ( 0 <_ ( f ` t ) /\ ( f ` t ) <_ 1 ) )
46 45 3ad2ant2 
 |-  ( ( ph /\ f e. Y /\ g e. Y ) -> A. t e. T ( 0 <_ ( f ` t ) /\ ( f ` t ) <_ 1 ) )
47 46 r19.21bi 
 |-  ( ( ( ph /\ f e. Y /\ g e. Y ) /\ t e. T ) -> ( 0 <_ ( f ` t ) /\ ( f ` t ) <_ 1 ) )
48 47 simpld 
 |-  ( ( ( ph /\ f e. Y /\ g e. Y ) /\ t e. T ) -> 0 <_ ( f ` t ) )
49 20 simprbi 
 |-  ( g e. Y -> A. t e. T ( 0 <_ ( g ` t ) /\ ( g ` t ) <_ 1 ) )
50 49 3ad2ant3 
 |-  ( ( ph /\ f e. Y /\ g e. Y ) -> A. t e. T ( 0 <_ ( g ` t ) /\ ( g ` t ) <_ 1 ) )
51 50 r19.21bi 
 |-  ( ( ( ph /\ f e. Y /\ g e. Y ) /\ t e. T ) -> ( 0 <_ ( g ` t ) /\ ( g ` t ) <_ 1 ) )
52 51 simpld 
 |-  ( ( ( ph /\ f e. Y /\ g e. Y ) /\ t e. T ) -> 0 <_ ( g ` t ) )
53 36 44 48 52 mulge0d 
 |-  ( ( ( ph /\ f e. Y /\ g e. Y ) /\ t e. T ) -> 0 <_ ( ( f ` t ) x. ( g ` t ) ) )
54 36 44 remulcld 
 |-  ( ( ( ph /\ f e. Y /\ g e. Y ) /\ t e. T ) -> ( ( f ` t ) x. ( g ` t ) ) e. RR )
55 3 fvmpt2 
 |-  ( ( t e. T /\ ( ( f ` t ) x. ( g ` t ) ) e. RR ) -> ( H ` t ) = ( ( f ` t ) x. ( g ` t ) ) )
56 35 54 55 syl2anc 
 |-  ( ( ( ph /\ f e. Y /\ g e. Y ) /\ t e. T ) -> ( H ` t ) = ( ( f ` t ) x. ( g ` t ) ) )
57 53 56 breqtrrd 
 |-  ( ( ( ph /\ f e. Y /\ g e. Y ) /\ t e. T ) -> 0 <_ ( H ` t ) )
58 1red 
 |-  ( ( ( ph /\ f e. Y /\ g e. Y ) /\ t e. T ) -> 1 e. RR )
59 47 simprd 
 |-  ( ( ( ph /\ f e. Y /\ g e. Y ) /\ t e. T ) -> ( f ` t ) <_ 1 )
60 51 simprd 
 |-  ( ( ( ph /\ f e. Y /\ g e. Y ) /\ t e. T ) -> ( g ` t ) <_ 1 )
61 36 58 44 58 48 52 59 60 lemul12ad 
 |-  ( ( ( ph /\ f e. Y /\ g e. Y ) /\ t e. T ) -> ( ( f ` t ) x. ( g ` t ) ) <_ ( 1 x. 1 ) )
62 1t1e1 
 |-  ( 1 x. 1 ) = 1
63 61 62 breqtrdi 
 |-  ( ( ( ph /\ f e. Y /\ g e. Y ) /\ t e. T ) -> ( ( f ` t ) x. ( g ` t ) ) <_ 1 )
64 56 63 eqbrtrd 
 |-  ( ( ( ph /\ f e. Y /\ g e. Y ) /\ t e. T ) -> ( H ` t ) <_ 1 )
65 57 64 jca 
 |-  ( ( ( ph /\ f e. Y /\ g e. Y ) /\ t e. T ) -> ( 0 <_ ( H ` t ) /\ ( H ` t ) <_ 1 ) )
66 65 ex 
 |-  ( ( ph /\ f e. Y /\ g e. Y ) -> ( t e. T -> ( 0 <_ ( H ` t ) /\ ( H ` t ) <_ 1 ) ) )
67 31 66 ralrimi 
 |-  ( ( ph /\ f e. Y /\ g e. Y ) -> A. t e. T ( 0 <_ ( H ` t ) /\ ( H ` t ) <_ 1 ) )
68 nfmpt1 
 |-  F/_ t ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) )
69 3 68 nfcxfr 
 |-  F/_ t H
70 69 nfeq2 
 |-  F/ t h = 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 -> ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> A. t e. T ( 0 <_ ( H ` t ) /\ ( H ` t ) <_ 1 ) ) )
76 75 elrab 
 |-  ( H e. { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) } <-> ( H e. A /\ A. t e. T ( 0 <_ ( H ` t ) /\ ( H ` t ) <_ 1 ) ) )
77 24 67 76 sylanbrc 
 |-  ( ( ph /\ f e. Y /\ g e. Y ) -> H e. { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) } )
78 77 2 eleqtrrdi 
 |-  ( ( ph /\ f e. Y /\ g e. Y ) -> H e. Y )