Metamath Proof Explorer

Theorem stoweidlem22

Description: If a set of real functions from a common domain is closed under addition, multiplication and it contains constants, then it is closed under subtraction. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem22.8 
|- F/ t ph
stoweidlem22.9 
|- F/_ t F
stoweidlem22.10 
|- F/_ t G
stoweidlem22.1 
|- H = ( t e. T |-> ( ( F ` t ) - ( G ` t ) ) )
stoweidlem22.2 
|- I = ( t e. T |-> -u 1 )
stoweidlem22.3 
|- L = ( t e. T |-> ( ( I ` t ) x. ( G ` t ) ) )
stoweidlem22.4 
|- ( ( ph /\ f e. A ) -> f : T --> RR )
stoweidlem22.5 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
stoweidlem22.6 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
stoweidlem22.7 
|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
Assertion stoweidlem22 
|- ( ( ph /\ F e. A /\ G e. A ) -> ( t e. T |-> ( ( F ` t ) - ( G ` t ) ) ) e. A )

Proof

Step Hyp Ref Expression
1 stoweidlem22.8 
 |-  F/ t ph
2 stoweidlem22.9 
 |-  F/_ t F
3 stoweidlem22.10 
 |-  F/_ t G
4 stoweidlem22.1 
 |-  H = ( t e. T |-> ( ( F ` t ) - ( G ` t ) ) )
5 stoweidlem22.2 
 |-  I = ( t e. T |-> -u 1 )
6 stoweidlem22.3 
 |-  L = ( t e. T |-> ( ( I ` t ) x. ( G ` t ) ) )
7 stoweidlem22.4 
 |-  ( ( ph /\ f e. A ) -> f : T --> RR )
8 stoweidlem22.5 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
9 stoweidlem22.6 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
10 stoweidlem22.7 
 |-  ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
11 2 nfel1 
 |-  F/ t F e. A
12 3 nfel1 
 |-  F/ t G e. A
13 1 11 12 nf3an 
 |-  F/ t ( ph /\ F e. A /\ G e. A )
14 simpr 
 |-  ( ( ( ph /\ F e. A /\ G e. A ) /\ t e. T ) -> t e. T )
15 simpl1 
 |-  ( ( ( ph /\ F e. A /\ G e. A ) /\ t e. T ) -> ph )
16 neg1rr 
 |-  -u 1 e. RR
17 10 stoweidlem4 
 |-  ( ( ph /\ -u 1 e. RR ) -> ( t e. T |-> -u 1 ) e. A )
18 16 17 mpan2 
 |-  ( ph -> ( t e. T |-> -u 1 ) e. A )
19 5 18 eqeltrid 
 |-  ( ph -> I e. A )
20 eleq1 
 |-  ( f = I -> ( f e. A <-> I e. A ) )
21 20 anbi2d 
 |-  ( f = I -> ( ( ph /\ f e. A ) <-> ( ph /\ I e. A ) ) )
22 feq1 
 |-  ( f = I -> ( f : T --> RR <-> I : T --> RR ) )
23 21 22 imbi12d 
 |-  ( f = I -> ( ( ( ph /\ f e. A ) -> f : T --> RR ) <-> ( ( ph /\ I e. A ) -> I : T --> RR ) ) )
24 23 7 vtoclg 
 |-  ( I e. A -> ( ( ph /\ I e. A ) -> I : T --> RR ) )
25 24 anabsi7 
 |-  ( ( ph /\ I e. A ) -> I : T --> RR )
26 15 19 25 syl2anc2 
 |-  ( ( ( ph /\ F e. A /\ G e. A ) /\ t e. T ) -> I : T --> RR )
27 26 14 ffvelrnd 
 |-  ( ( ( ph /\ F e. A /\ G e. A ) /\ t e. T ) -> ( I ` t ) e. RR )
28 simpl3 
 |-  ( ( ( ph /\ F e. A /\ G e. A ) /\ t e. T ) -> G e. A )
29 eleq1 
 |-  ( f = G -> ( f e. A <-> G e. A ) )
30 29 anbi2d 
 |-  ( f = G -> ( ( ph /\ f e. A ) <-> ( ph /\ G e. A ) ) )
31 feq1 
 |-  ( f = G -> ( f : T --> RR <-> G : T --> RR ) )
32 30 31 imbi12d 
 |-  ( f = G -> ( ( ( ph /\ f e. A ) -> f : T --> RR ) <-> ( ( ph /\ G e. A ) -> G : T --> RR ) ) )
33 32 7 vtoclg 
 |-  ( G e. A -> ( ( ph /\ G e. A ) -> G : T --> RR ) )
34 33 anabsi7 
 |-  ( ( ph /\ G e. A ) -> G : T --> RR )
35 34 3adant3 
 |-  ( ( ph /\ G e. A /\ t e. T ) -> G : T --> RR )
36 simp3 
 |-  ( ( ph /\ G e. A /\ t e. T ) -> t e. T )
37 35 36 ffvelrnd 
 |-  ( ( ph /\ G e. A /\ t e. T ) -> ( G ` t ) e. RR )
38 15 28 14 37 syl3anc 
 |-  ( ( ( ph /\ F e. A /\ G e. A ) /\ t e. T ) -> ( G ` t ) e. RR )
39 27 38 remulcld 
 |-  ( ( ( ph /\ F e. A /\ G e. A ) /\ t e. T ) -> ( ( I ` t ) x. ( G ` t ) ) e. RR )
40 6 fvmpt2 
 |-  ( ( t e. T /\ ( ( I ` t ) x. ( G ` t ) ) e. RR ) -> ( L ` t ) = ( ( I ` t ) x. ( G ` t ) ) )
41 14 39 40 syl2anc 
 |-  ( ( ( ph /\ F e. A /\ G e. A ) /\ t e. T ) -> ( L ` t ) = ( ( I ` t ) x. ( G ` t ) ) )
42 5 fvmpt2 
 |-  ( ( t e. T /\ -u 1 e. RR ) -> ( I ` t ) = -u 1 )
43 16 42 mpan2 
 |-  ( t e. T -> ( I ` t ) = -u 1 )
44 43 adantl 
 |-  ( ( ( ph /\ F e. A /\ G e. A ) /\ t e. T ) -> ( I ` t ) = -u 1 )
45 44 oveq1d 
 |-  ( ( ( ph /\ F e. A /\ G e. A ) /\ t e. T ) -> ( ( I ` t ) x. ( G ` t ) ) = ( -u 1 x. ( G ` t ) ) )
46 38 recnd 
 |-  ( ( ( ph /\ F e. A /\ G e. A ) /\ t e. T ) -> ( G ` t ) e. CC )
47 46 mulm1d 
 |-  ( ( ( ph /\ F e. A /\ G e. A ) /\ t e. T ) -> ( -u 1 x. ( G ` t ) ) = -u ( G ` t ) )
48 41 45 47 3eqtrd 
 |-  ( ( ( ph /\ F e. A /\ G e. A ) /\ t e. T ) -> ( L ` t ) = -u ( G ` t ) )
49 48 oveq2d 
 |-  ( ( ( ph /\ F e. A /\ G e. A ) /\ t e. T ) -> ( ( F ` t ) + ( L ` t ) ) = ( ( F ` t ) + -u ( G ` t ) ) )
50 simpl2 
 |-  ( ( ( ph /\ F e. A /\ G e. A ) /\ t e. T ) -> F e. A )
51 eleq1 
 |-  ( f = F -> ( f e. A <-> F e. A ) )
52 51 anbi2d 
 |-  ( f = F -> ( ( ph /\ f e. A ) <-> ( ph /\ F e. A ) ) )
53 feq1 
 |-  ( f = F -> ( f : T --> RR <-> F : T --> RR ) )
54 52 53 imbi12d 
 |-  ( f = F -> ( ( ( ph /\ f e. A ) -> f : T --> RR ) <-> ( ( ph /\ F e. A ) -> F : T --> RR ) ) )
55 54 7 vtoclg 
 |-  ( F e. A -> ( ( ph /\ F e. A ) -> F : T --> RR ) )
56 55 anabsi7 
 |-  ( ( ph /\ F e. A ) -> F : T --> RR )
57 15 50 56 syl2anc 
 |-  ( ( ( ph /\ F e. A /\ G e. A ) /\ t e. T ) -> F : T --> RR )
58 57 14 ffvelrnd 
 |-  ( ( ( ph /\ F e. A /\ G e. A ) /\ t e. T ) -> ( F ` t ) e. RR )
59 58 recnd 
 |-  ( ( ( ph /\ F e. A /\ G e. A ) /\ t e. T ) -> ( F ` t ) e. CC )
60 59 46 negsubd 
 |-  ( ( ( ph /\ F e. A /\ G e. A ) /\ t e. T ) -> ( ( F ` t ) + -u ( G ` t ) ) = ( ( F ` t ) - ( G ` t ) ) )
61 49 60 eqtr2d 
 |-  ( ( ( ph /\ F e. A /\ G e. A ) /\ t e. T ) -> ( ( F ` t ) - ( G ` t ) ) = ( ( F ` t ) + ( L ` t ) ) )
62 13 61 mpteq2da 
 |-  ( ( ph /\ F e. A /\ G e. A ) -> ( t e. T |-> ( ( F ` t ) - ( G ` t ) ) ) = ( t e. T |-> ( ( F ` t ) + ( L ` t ) ) ) )
63 19 3ad2ant1 
 |-  ( ( ph /\ F e. A /\ G e. A ) -> I e. A )
64 nfmpt1 
 |-  F/_ t ( t e. T |-> -u 1 )
65 5 64 nfcxfr 
 |-  F/_ t I
66 65 nfeq2 
 |-  F/ t f = I
67 3 nfeq2 
 |-  F/ t g = G
68 66 67 9 stoweidlem6 
 |-  ( ( ph /\ I e. A /\ G e. A ) -> ( t e. T |-> ( ( I ` t ) x. ( G ` t ) ) ) e. A )
69 63 68 syld3an2 
 |-  ( ( ph /\ F e. A /\ G e. A ) -> ( t e. T |-> ( ( I ` t ) x. ( G ` t ) ) ) e. A )
70 6 69 eqeltrid 
 |-  ( ( ph /\ F e. A /\ G e. A ) -> L e. A )
71 nfmpt1 
 |-  F/_ t ( t e. T |-> ( ( I ` t ) x. ( G ` t ) ) )
72 6 71 nfcxfr 
 |-  F/_ t L
73 8 2 72 stoweidlem8 
 |-  ( ( ph /\ F e. A /\ L e. A ) -> ( t e. T |-> ( ( F ` t ) + ( L ` t ) ) ) e. A )
74 70 73 syld3an3 
 |-  ( ( ph /\ F e. A /\ G e. A ) -> ( t e. T |-> ( ( F ` t ) + ( L ` t ) ) ) e. A )
75 62 74 eqeltrd 
 |-  ( ( ph /\ F e. A /\ G e. A ) -> ( t e. T |-> ( ( F ` t ) - ( G ` t ) ) ) e. A )