Metamath Proof Explorer

Theorem stoweidlem2

Description: lemma for stoweid : here we prove that the subalgebra of continuous functions, which contains constant functions, is closed under scaling. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem2.1 
|- F/ t ph
stoweidlem2.2 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
stoweidlem2.3 
|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
stoweidlem2.4 
|- ( ( ph /\ f e. A ) -> f : T --> RR )
stoweidlem2.5 
|- ( ph -> E e. RR )
stoweidlem2.6 
|- ( ph -> F e. A )
Assertion stoweidlem2 
|- ( ph -> ( t e. T |-> ( E x. ( F ` t ) ) ) e. A )

Proof

Step Hyp Ref Expression
1 stoweidlem2.1 
 |-  F/ t ph
2 stoweidlem2.2 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
3 stoweidlem2.3 
 |-  ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
4 stoweidlem2.4 
 |-  ( ( ph /\ f e. A ) -> f : T --> RR )
5 stoweidlem2.5 
 |-  ( ph -> E e. RR )
6 stoweidlem2.6 
 |-  ( ph -> F e. A )
7 simpr 
 |-  ( ( ph /\ t e. T ) -> t e. T )
8 5 adantr 
 |-  ( ( ph /\ t e. T ) -> E e. RR )
9 eqidd 
 |-  ( s = t -> E = E )
10 9 cbvmptv 
 |-  ( s e. T |-> E ) = ( t e. T |-> E )
11 10 fvmpt2 
 |-  ( ( t e. T /\ E e. RR ) -> ( ( s e. T |-> E ) ` t ) = E )
12 7 8 11 syl2anc 
 |-  ( ( ph /\ t e. T ) -> ( ( s e. T |-> E ) ` t ) = E )
13 12 eqcomd 
 |-  ( ( ph /\ t e. T ) -> E = ( ( s e. T |-> E ) ` t ) )
14 13 oveq1d 
 |-  ( ( ph /\ t e. T ) -> ( E x. ( F ` t ) ) = ( ( ( s e. T |-> E ) ` t ) x. ( F ` t ) ) )
15 1 14 mpteq2da 
 |-  ( ph -> ( t e. T |-> ( E x. ( F ` t ) ) ) = ( t e. T |-> ( ( ( s e. T |-> E ) ` t ) x. ( F ` t ) ) ) )
16 id 
 |-  ( x = E -> x = E )
17 16 mpteq2dv 
 |-  ( x = E -> ( t e. T |-> x ) = ( t e. T |-> E ) )
18 17 eleq1d 
 |-  ( x = E -> ( ( t e. T |-> x ) e. A <-> ( t e. T |-> E ) e. A ) )
19 18 imbi2d 
 |-  ( x = E -> ( ( ph -> ( t e. T |-> x ) e. A ) <-> ( ph -> ( t e. T |-> E ) e. A ) ) )
20 3 expcom 
 |-  ( x e. RR -> ( ph -> ( t e. T |-> x ) e. A ) )
21 19 20 vtoclga 
 |-  ( E e. RR -> ( ph -> ( t e. T |-> E ) e. A ) )
22 5 21 mpcom 
 |-  ( ph -> ( t e. T |-> E ) e. A )
23 10 22 eqeltrid 
 |-  ( ph -> ( s e. T |-> E ) e. A )
24 fveq1 
 |-  ( f = ( s e. T |-> E ) -> ( f ` t ) = ( ( s e. T |-> E ) ` t ) )
25 24 oveq1d 
 |-  ( f = ( s e. T |-> E ) -> ( ( f ` t ) x. ( F ` t ) ) = ( ( ( s e. T |-> E ) ` t ) x. ( F ` t ) ) )
26 25 mpteq2dv 
 |-  ( f = ( s e. T |-> E ) -> ( t e. T |-> ( ( f ` t ) x. ( F ` t ) ) ) = ( t e. T |-> ( ( ( s e. T |-> E ) ` t ) x. ( F ` t ) ) ) )
27 26 eleq1d 
 |-  ( f = ( s e. T |-> E ) -> ( ( t e. T |-> ( ( f ` t ) x. ( F ` t ) ) ) e. A <-> ( t e. T |-> ( ( ( s e. T |-> E ) ` t ) x. ( F ` t ) ) ) e. A ) )
28 27 imbi2d 
 |-  ( f = ( s e. T |-> E ) -> ( ( ph -> ( t e. T |-> ( ( f ` t ) x. ( F ` t ) ) ) e. A ) <-> ( ph -> ( t e. T |-> ( ( ( s e. T |-> E ) ` t ) x. ( F ` t ) ) ) e. A ) ) )
29 6 adantr 
 |-  ( ( ph /\ f e. A ) -> F e. A )
30 fveq1 
 |-  ( g = F -> ( g ` t ) = ( F ` t ) )
31 30 oveq2d 
 |-  ( g = F -> ( ( f ` t ) x. ( g ` t ) ) = ( ( f ` t ) x. ( F ` t ) ) )
32 31 mpteq2dv 
 |-  ( g = F -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) = ( t e. T |-> ( ( f ` t ) x. ( F ` t ) ) ) )
33 32 eleq1d 
 |-  ( g = F -> ( ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A <-> ( t e. T |-> ( ( f ` t ) x. ( F ` t ) ) ) e. A ) )
34 33 imbi2d 
 |-  ( g = F -> ( ( ( ph /\ f e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A ) <-> ( ( ph /\ f e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( F ` t ) ) ) e. A ) ) )
35 2 3comr 
 |-  ( ( g e. A /\ ph /\ f e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
36 35 3expib 
 |-  ( g e. A -> ( ( ph /\ f e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A ) )
37 34 36 vtoclga 
 |-  ( F e. A -> ( ( ph /\ f e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( F ` t ) ) ) e. A ) )
38 29 37 mpcom 
 |-  ( ( ph /\ f e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( F ` t ) ) ) e. A )
39 38 expcom 
 |-  ( f e. A -> ( ph -> ( t e. T |-> ( ( f ` t ) x. ( F ` t ) ) ) e. A ) )
40 28 39 vtoclga 
 |-  ( ( s e. T |-> E ) e. A -> ( ph -> ( t e. T |-> ( ( ( s e. T |-> E ) ` t ) x. ( F ` t ) ) ) e. A ) )
41 23 40 mpcom 
 |-  ( ph -> ( t e. T |-> ( ( ( s e. T |-> E ) ` t ) x. ( F ` t ) ) ) e. A )
42 15 41 eqeltrd 
 |-  ( ph -> ( t e. T |-> ( E x. ( F ` t ) ) ) e. A )