Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem22 Structured version   Visualization version   GIF version

Theorem stoweidlem22 39567
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.)
Hypotheses
Ref Expression
stoweidlem22.8 𝑡𝜑
stoweidlem22.9 𝑡𝐹
stoweidlem22.10 𝑡𝐺
stoweidlem22.1 𝐻 = (𝑡𝑇 ↦ ((𝐹𝑡) − (𝐺𝑡)))
stoweidlem22.2 𝐼 = (𝑡𝑇 ↦ -1)
stoweidlem22.3 𝐿 = (𝑡𝑇 ↦ ((𝐼𝑡) · (𝐺𝑡)))
stoweidlem22.4 ((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ)
stoweidlem22.5 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
stoweidlem22.6 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
stoweidlem22.7 ((𝜑𝑥 ∈ ℝ) → (𝑡𝑇𝑥) ∈ 𝐴)
Assertion
Ref Expression
stoweidlem22 ((𝜑𝐹𝐴𝐺𝐴) → (𝑡𝑇 ↦ ((𝐹𝑡) − (𝐺𝑡))) ∈ 𝐴)
Distinct variable groups:   𝑓,𝑔,𝑡,𝐴   𝑓,𝐹,𝑔   𝑓,𝐺,𝑔   𝑓,𝐼,𝑔   𝑇,𝑓,𝑔,𝑡   𝜑,𝑓,𝑔   𝑔,𝐿   𝑥,𝑡,𝐴   𝑥,𝑇   𝜑,𝑥
Allowed substitution hints:   𝜑(𝑡)   𝐹(𝑥,𝑡)   𝐺(𝑥,𝑡)   𝐻(𝑥,𝑡,𝑓,𝑔)   𝐼(𝑥,𝑡)   𝐿(𝑥,𝑡,𝑓)

Proof of Theorem stoweidlem22
StepHypRef Expression
1 stoweidlem22.8 . . . 4 𝑡𝜑
2 stoweidlem22.9 . . . . 5 𝑡𝐹
32nfel1 2775 . . . 4 𝑡 𝐹𝐴
4 stoweidlem22.10 . . . . 5 𝑡𝐺
54nfel1 2775 . . . 4 𝑡 𝐺𝐴
61, 3, 5nf3an 1828 . . 3 𝑡(𝜑𝐹𝐴𝐺𝐴)
7 simpr 477 . . . . . . 7 (((𝜑𝐹𝐴𝐺𝐴) ∧ 𝑡𝑇) → 𝑡𝑇)
8 simpl1 1062 . . . . . . . . . 10 (((𝜑𝐹𝐴𝐺𝐴) ∧ 𝑡𝑇) → 𝜑)
9 stoweidlem22.2 . . . . . . . . . . . 12 𝐼 = (𝑡𝑇 ↦ -1)
10 neg1rr 11076 . . . . . . . . . . . . 13 -1 ∈ ℝ
11 stoweidlem22.7 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → (𝑡𝑇𝑥) ∈ 𝐴)
1211stoweidlem4 39549 . . . . . . . . . . . . 13 ((𝜑 ∧ -1 ∈ ℝ) → (𝑡𝑇 ↦ -1) ∈ 𝐴)
1310, 12mpan2 706 . . . . . . . . . . . 12 (𝜑 → (𝑡𝑇 ↦ -1) ∈ 𝐴)
149, 13syl5eqel 2702 . . . . . . . . . . 11 (𝜑𝐼𝐴)
15 eleq1 2686 . . . . . . . . . . . . . . 15 (𝑓 = 𝐼 → (𝑓𝐴𝐼𝐴))
1615anbi2d 739 . . . . . . . . . . . . . 14 (𝑓 = 𝐼 → ((𝜑𝑓𝐴) ↔ (𝜑𝐼𝐴)))
17 feq1 5988 . . . . . . . . . . . . . 14 (𝑓 = 𝐼 → (𝑓:𝑇⟶ℝ ↔ 𝐼:𝑇⟶ℝ))
1816, 17imbi12d 334 . . . . . . . . . . . . 13 (𝑓 = 𝐼 → (((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑𝐼𝐴) → 𝐼:𝑇⟶ℝ)))
19 stoweidlem22.4 . . . . . . . . . . . . 13 ((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ)
2018, 19vtoclg 3255 . . . . . . . . . . . 12 (𝐼𝐴 → ((𝜑𝐼𝐴) → 𝐼:𝑇⟶ℝ))
2120anabsi7 859 . . . . . . . . . . 11 ((𝜑𝐼𝐴) → 𝐼:𝑇⟶ℝ)
2214, 21mpdan 701 . . . . . . . . . 10 (𝜑𝐼:𝑇⟶ℝ)
238, 22syl 17 . . . . . . . . 9 (((𝜑𝐹𝐴𝐺𝐴) ∧ 𝑡𝑇) → 𝐼:𝑇⟶ℝ)
2423, 7ffvelrnd 6321 . . . . . . . 8 (((𝜑𝐹𝐴𝐺𝐴) ∧ 𝑡𝑇) → (𝐼𝑡) ∈ ℝ)
25 simpl3 1064 . . . . . . . . 9 (((𝜑𝐹𝐴𝐺𝐴) ∧ 𝑡𝑇) → 𝐺𝐴)
26 eleq1 2686 . . . . . . . . . . . . . . 15 (𝑓 = 𝐺 → (𝑓𝐴𝐺𝐴))
2726anbi2d 739 . . . . . . . . . . . . . 14 (𝑓 = 𝐺 → ((𝜑𝑓𝐴) ↔ (𝜑𝐺𝐴)))
28 feq1 5988 . . . . . . . . . . . . . 14 (𝑓 = 𝐺 → (𝑓:𝑇⟶ℝ ↔ 𝐺:𝑇⟶ℝ))
2927, 28imbi12d 334 . . . . . . . . . . . . 13 (𝑓 = 𝐺 → (((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑𝐺𝐴) → 𝐺:𝑇⟶ℝ)))
3029, 19vtoclg 3255 . . . . . . . . . . . 12 (𝐺𝐴 → ((𝜑𝐺𝐴) → 𝐺:𝑇⟶ℝ))
3130anabsi7 859 . . . . . . . . . . 11 ((𝜑𝐺𝐴) → 𝐺:𝑇⟶ℝ)
32313adant3 1079 . . . . . . . . . 10 ((𝜑𝐺𝐴𝑡𝑇) → 𝐺:𝑇⟶ℝ)
33 simp3 1061 . . . . . . . . . 10 ((𝜑𝐺𝐴𝑡𝑇) → 𝑡𝑇)
3432, 33ffvelrnd 6321 . . . . . . . . 9 ((𝜑𝐺𝐴𝑡𝑇) → (𝐺𝑡) ∈ ℝ)
358, 25, 7, 34syl3anc 1323 . . . . . . . 8 (((𝜑𝐹𝐴𝐺𝐴) ∧ 𝑡𝑇) → (𝐺𝑡) ∈ ℝ)
3624, 35remulcld 10021 . . . . . . 7 (((𝜑𝐹𝐴𝐺𝐴) ∧ 𝑡𝑇) → ((𝐼𝑡) · (𝐺𝑡)) ∈ ℝ)
37 stoweidlem22.3 . . . . . . . 8 𝐿 = (𝑡𝑇 ↦ ((𝐼𝑡) · (𝐺𝑡)))
3837fvmpt2 6253 . . . . . . 7 ((𝑡𝑇 ∧ ((𝐼𝑡) · (𝐺𝑡)) ∈ ℝ) → (𝐿𝑡) = ((𝐼𝑡) · (𝐺𝑡)))
397, 36, 38syl2anc 692 . . . . . 6 (((𝜑𝐹𝐴𝐺𝐴) ∧ 𝑡𝑇) → (𝐿𝑡) = ((𝐼𝑡) · (𝐺𝑡)))
409fvmpt2 6253 . . . . . . . . 9 ((𝑡𝑇 ∧ -1 ∈ ℝ) → (𝐼𝑡) = -1)
4110, 40mpan2 706 . . . . . . . 8 (𝑡𝑇 → (𝐼𝑡) = -1)
4241adantl 482 . . . . . . 7 (((𝜑𝐹𝐴𝐺𝐴) ∧ 𝑡𝑇) → (𝐼𝑡) = -1)
4342oveq1d 6625 . . . . . 6 (((𝜑𝐹𝐴𝐺𝐴) ∧ 𝑡𝑇) → ((𝐼𝑡) · (𝐺𝑡)) = (-1 · (𝐺𝑡)))
4435recnd 10019 . . . . . . 7 (((𝜑𝐹𝐴𝐺𝐴) ∧ 𝑡𝑇) → (𝐺𝑡) ∈ ℂ)
4544mulm1d 10433 . . . . . 6 (((𝜑𝐹𝐴𝐺𝐴) ∧ 𝑡𝑇) → (-1 · (𝐺𝑡)) = -(𝐺𝑡))
4639, 43, 453eqtrd 2659 . . . . 5 (((𝜑𝐹𝐴𝐺𝐴) ∧ 𝑡𝑇) → (𝐿𝑡) = -(𝐺𝑡))
4746oveq2d 6626 . . . 4 (((𝜑𝐹𝐴𝐺𝐴) ∧ 𝑡𝑇) → ((𝐹𝑡) + (𝐿𝑡)) = ((𝐹𝑡) + -(𝐺𝑡)))
48 simpl2 1063 . . . . . . . 8 (((𝜑𝐹𝐴𝐺𝐴) ∧ 𝑡𝑇) → 𝐹𝐴)
49 eleq1 2686 . . . . . . . . . . . 12 (𝑓 = 𝐹 → (𝑓𝐴𝐹𝐴))
5049anbi2d 739 . . . . . . . . . . 11 (𝑓 = 𝐹 → ((𝜑𝑓𝐴) ↔ (𝜑𝐹𝐴)))
51 feq1 5988 . . . . . . . . . . 11 (𝑓 = 𝐹 → (𝑓:𝑇⟶ℝ ↔ 𝐹:𝑇⟶ℝ))
5250, 51imbi12d 334 . . . . . . . . . 10 (𝑓 = 𝐹 → (((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑𝐹𝐴) → 𝐹:𝑇⟶ℝ)))
5352, 19vtoclg 3255 . . . . . . . . 9 (𝐹𝐴 → ((𝜑𝐹𝐴) → 𝐹:𝑇⟶ℝ))
5453anabsi7 859 . . . . . . . 8 ((𝜑𝐹𝐴) → 𝐹:𝑇⟶ℝ)
558, 48, 54syl2anc 692 . . . . . . 7 (((𝜑𝐹𝐴𝐺𝐴) ∧ 𝑡𝑇) → 𝐹:𝑇⟶ℝ)
5655, 7ffvelrnd 6321 . . . . . 6 (((𝜑𝐹𝐴𝐺𝐴) ∧ 𝑡𝑇) → (𝐹𝑡) ∈ ℝ)
5756recnd 10019 . . . . 5 (((𝜑𝐹𝐴𝐺𝐴) ∧ 𝑡𝑇) → (𝐹𝑡) ∈ ℂ)
5857, 44negsubd 10349 . . . 4 (((𝜑𝐹𝐴𝐺𝐴) ∧ 𝑡𝑇) → ((𝐹𝑡) + -(𝐺𝑡)) = ((𝐹𝑡) − (𝐺𝑡)))
5947, 58eqtr2d 2656 . . 3 (((𝜑𝐹𝐴𝐺𝐴) ∧ 𝑡𝑇) → ((𝐹𝑡) − (𝐺𝑡)) = ((𝐹𝑡) + (𝐿𝑡)))
606, 59mpteq2da 4708 . 2 ((𝜑𝐹𝐴𝐺𝐴) → (𝑡𝑇 ↦ ((𝐹𝑡) − (𝐺𝑡))) = (𝑡𝑇 ↦ ((𝐹𝑡) + (𝐿𝑡))))
61143ad2ant1 1080 . . . . 5 ((𝜑𝐹𝐴𝐺𝐴) → 𝐼𝐴)
62 nfmpt1 4712 . . . . . . . 8 𝑡(𝑡𝑇 ↦ -1)
639, 62nfcxfr 2759 . . . . . . 7 𝑡𝐼
6463nfeq2 2776 . . . . . 6 𝑡 𝑓 = 𝐼
654nfeq2 2776 . . . . . 6 𝑡 𝑔 = 𝐺
66 stoweidlem22.6 . . . . . 6 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
6764, 65, 66stoweidlem6 39551 . . . . 5 ((𝜑𝐼𝐴𝐺𝐴) → (𝑡𝑇 ↦ ((𝐼𝑡) · (𝐺𝑡))) ∈ 𝐴)
6861, 67syld3an2 1370 . . . 4 ((𝜑𝐹𝐴𝐺𝐴) → (𝑡𝑇 ↦ ((𝐼𝑡) · (𝐺𝑡))) ∈ 𝐴)
6937, 68syl5eqel 2702 . . 3 ((𝜑𝐹𝐴𝐺𝐴) → 𝐿𝐴)
70 stoweidlem22.5 . . . 4 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
71 nfmpt1 4712 . . . . 5 𝑡(𝑡𝑇 ↦ ((𝐼𝑡) · (𝐺𝑡)))
7237, 71nfcxfr 2759 . . . 4 𝑡𝐿
7370, 2, 72stoweidlem8 39553 . . 3 ((𝜑𝐹𝐴𝐿𝐴) → (𝑡𝑇 ↦ ((𝐹𝑡) + (𝐿𝑡))) ∈ 𝐴)
7469, 73syld3an3 1368 . 2 ((𝜑𝐹𝐴𝐺𝐴) → (𝑡𝑇 ↦ ((𝐹𝑡) + (𝐿𝑡))) ∈ 𝐴)
7560, 74eqeltrd 2698 1 ((𝜑𝐹𝐴𝐺𝐴) → (𝑡𝑇 ↦ ((𝐹𝑡) − (𝐺𝑡))) ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036   = wceq 1480  wnf 1705  wcel 1987  wnfc 2748  cmpt 4678  wf 5848  cfv 5852  (class class class)co 6610  cr 9886  1c1 9888   + caddc 9890   · cmul 9892  cmin 10217  -cneg 10218
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-po 5000  df-so 5001  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-er 7694  df-en 7907  df-dom 7908  df-sdom 7909  df-pnf 10027  df-mnf 10028  df-ltxr 10030  df-sub 10219  df-neg 10220
This theorem is referenced by:  stoweidlem33  39578
  Copyright terms: Public domain W3C validator