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 ffvelrnd ( ( ( 𝜑𝐹𝐴𝐺𝐴 ) ∧ 𝑡𝑇 ) → ( 𝐼𝑡 ) ∈ ℝ )
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 ffvelrnd ( ( 𝜑𝐺𝐴𝑡𝑇 ) → ( 𝐺𝑡 ) ∈ ℝ )
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 ffvelrnd ( ( ( 𝜑𝐹𝐴𝐺𝐴 ) ∧ 𝑡𝑇 ) → ( 𝐹𝑡 ) ∈ ℝ )
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 ( ( 𝜑𝐹𝐴𝐺𝐴 ) → ( 𝑡𝑇 ↦ ( ( 𝐹𝑡 ) − ( 𝐺𝑡 ) ) ) ∈ 𝐴 )