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 t φ
stoweidlem22.9 _ t F
stoweidlem22.10 _ t G
stoweidlem22.1 H = t T F t G t
stoweidlem22.2 I = t T 1
stoweidlem22.3 L = t T I t G t
stoweidlem22.4 φ f A f : T
stoweidlem22.5 φ f A g A t T f t + g t A
stoweidlem22.6 φ f A g A t T f t g t A
stoweidlem22.7 φ x t T x A
Assertion stoweidlem22 φ F A G A t T F t G t A

Proof

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