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 ⊢ Ⅎ 𝑡 𝜑
stoweidlem22.9 ⊢ Ⅎ 𝑡 𝐹
stoweidlem22.10 ⊢ Ⅎ 𝑡 𝐺
stoweidlem22.1 ⊢ 𝐻 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) )
stoweidlem22.2 ⊢ 𝐼 = ( 𝑡 ∈ 𝑇 ↦ - 1 )
stoweidlem22.3 ⊢ 𝐿 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) )
stoweidlem22.4 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
stoweidlem22.5 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem22.6 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem22.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
Assertion stoweidlem22 ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 stoweidlem22.8 ⊢ Ⅎ 𝑡 𝜑
2 stoweidlem22.9 ⊢ Ⅎ 𝑡 𝐹
3 stoweidlem22.10 ⊢ Ⅎ 𝑡 𝐺
4 stoweidlem22.1 ⊢ 𝐻 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) )
5 stoweidlem22.2 ⊢ 𝐼 = ( 𝑡 ∈ 𝑇 ↦ - 1 )
6 stoweidlem22.3 ⊢ 𝐿 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) )
7 stoweidlem22.4 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
8 stoweidlem22.5 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
9 stoweidlem22.6 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
10 stoweidlem22.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
11 2 nfel1 ⊢ Ⅎ 𝑡 𝐹 ∈ 𝐴
12 3 nfel1 ⊢ Ⅎ 𝑡 𝐺 ∈ 𝐴
13 1 11 12 nf3an ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 )
14 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
15 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝜑 )
16 neg1rr ⊢ - 1 ∈ ℝ
17 10 stoweidlem4 ⊢ ( ( 𝜑 ∧ - 1 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ - 1 ) ∈ 𝐴 )
18 16 17 mpan2 ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ - 1 ) ∈ 𝐴 )
19 5 18 eqeltrid ⊢ ( 𝜑 → 𝐼 ∈ 𝐴 )
20 eleq1 ⊢ ( 𝑓 = 𝐼 → ( 𝑓 ∈ 𝐴 ↔ 𝐼 ∈ 𝐴 ) )
21 20 anbi2d ⊢ ( 𝑓 = 𝐼 → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝐼 ∈ 𝐴 ) ) )
22 feq1 ⊢ ( 𝑓 = 𝐼 → ( 𝑓 : 𝑇 ⟶ ℝ ↔ 𝐼 : 𝑇 ⟶ ℝ ) )
23 21 22 imbi12d ⊢ ( 𝑓 = 𝐼 → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ 𝐼 ∈ 𝐴 ) → 𝐼 : 𝑇 ⟶ ℝ ) ) )
24 23 7 vtoclg ⊢ ( 𝐼 ∈ 𝐴 → ( ( 𝜑 ∧ 𝐼 ∈ 𝐴 ) → 𝐼 : 𝑇 ⟶ ℝ ) )
25 24 anabsi7 ⊢ ( ( 𝜑 ∧ 𝐼 ∈ 𝐴 ) → 𝐼 : 𝑇 ⟶ ℝ )
26 15 19 25 syl2anc2 ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝐼 : 𝑇 ⟶ ℝ )
27 26 14 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐼 ‘ 𝑡 ) ∈ ℝ )
28 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝐺 ∈ 𝐴 )
29 eleq1 ⊢ ( 𝑓 = 𝐺 → ( 𝑓 ∈ 𝐴 ↔ 𝐺 ∈ 𝐴 ) )
30 29 anbi2d ⊢ ( 𝑓 = 𝐺 → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) ) )
31 feq1 ⊢ ( 𝑓 = 𝐺 → ( 𝑓 : 𝑇 ⟶ ℝ ↔ 𝐺 : 𝑇 ⟶ ℝ ) )
32 30 31 imbi12d ⊢ ( 𝑓 = 𝐺 → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) → 𝐺 : 𝑇 ⟶ ℝ ) ) )
33 32 7 vtoclg ⊢ ( 𝐺 ∈ 𝐴 → ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) → 𝐺 : 𝑇 ⟶ ℝ ) )
34 33 anabsi7 ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) → 𝐺 : 𝑇 ⟶ ℝ )
35 34 3adant3 ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ∧ 𝑡 ∈ 𝑇 ) → 𝐺 : 𝑇 ⟶ ℝ )
36 simp3 ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
37 35 36 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑡 ) ∈ ℝ )
38 15 28 14 37 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑡 ) ∈ ℝ )
39 27 38 remulcld ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ∈ ℝ )
40 6 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ∈ ℝ ) → ( 𝐿 ‘ 𝑡 ) = ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) )
41 14 39 40 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐿 ‘ 𝑡 ) = ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) )
42 5 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ - 1 ∈ ℝ ) → ( 𝐼 ‘ 𝑡 ) = - 1 )
43 16 42 mpan2 ⊢ ( 𝑡 ∈ 𝑇 → ( 𝐼 ‘ 𝑡 ) = - 1 )
44 43 adantl ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐼 ‘ 𝑡 ) = - 1 )
45 44 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) = ( - 1 · ( 𝐺 ‘ 𝑡 ) ) )
46 38 recnd ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑡 ) ∈ ℂ )
47 46 mulm1d ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( - 1 · ( 𝐺 ‘ 𝑡 ) ) = - ( 𝐺 ‘ 𝑡 ) )
48 41 45 47 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐿 ‘ 𝑡 ) = - ( 𝐺 ‘ 𝑡 ) )
49 48 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) + ( 𝐿 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) + - ( 𝐺 ‘ 𝑡 ) ) )
50 simpl2 ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝐹 ∈ 𝐴 )
51 eleq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∈ 𝐴 ↔ 𝐹 ∈ 𝐴 ) )
52 51 anbi2d ⊢ ( 𝑓 = 𝐹 → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝐹 ∈ 𝐴 ) ) )
53 feq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝑇 ⟶ ℝ ↔ 𝐹 : 𝑇 ⟶ ℝ ) )
54 52 53 imbi12d ⊢ ( 𝑓 = 𝐹 → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ) → 𝐹 : 𝑇 ⟶ ℝ ) ) )
55 54 7 vtoclg ⊢ ( 𝐹 ∈ 𝐴 → ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ) → 𝐹 : 𝑇 ⟶ ℝ ) )
56 55 anabsi7 ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ) → 𝐹 : 𝑇 ⟶ ℝ )
57 15 50 56 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝐹 : 𝑇 ⟶ ℝ )
58 57 14 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
59 58 recnd ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
60 59 46 negsubd ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) + - ( 𝐺 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) )
61 49 60 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) + ( 𝐿 ‘ 𝑡 ) ) )
62 13 61 mpteq2da ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝐿 ‘ 𝑡 ) ) ) )
63 19 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → 𝐼 ∈ 𝐴 )
64 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ - 1 )
65 5 64 nfcxfr ⊢ Ⅎ 𝑡 𝐼
66 65 nfeq2 ⊢ Ⅎ 𝑡 𝑓 = 𝐼
67 3 nfeq2 ⊢ Ⅎ 𝑡 𝑔 = 𝐺
68 66 67 9 stoweidlem6 ⊢ ( ( 𝜑 ∧ 𝐼 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 )
69 63 68 syld3an2 ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 )
70 6 69 eqeltrid ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → 𝐿 ∈ 𝐴 )
71 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) )
72 6 71 nfcxfr ⊢ Ⅎ 𝑡 𝐿
73 8 2 72 stoweidlem8 ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐿 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝐿 ‘ 𝑡 ) ) ) ∈ 𝐴 )
74 70 73 syld3an3 ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝐿 ‘ 𝑡 ) ) ) ∈ 𝐴 )
75 62 74 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 )