Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  offres Structured version   Visualization version   GIF version

Theorem offres 7115
 Description: Pointwise combination commutes with restriction. (Contributed by Stefan O'Rear, 24-Jan-2015.)
Assertion
Ref Expression
offres ((𝐹𝑉𝐺𝑊) → ((𝐹𝑓 𝑅𝐺) ↾ 𝐷) = ((𝐹𝐷) ∘𝑓 𝑅(𝐺𝐷)))

Proof of Theorem offres
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 inss2 3817 . . . . . 6 ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) ⊆ 𝐷
21sseli 3583 . . . . 5 (𝑥 ∈ ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) → 𝑥𝐷)
3 fvres 6169 . . . . . 6 (𝑥𝐷 → ((𝐹𝐷)‘𝑥) = (𝐹𝑥))
4 fvres 6169 . . . . . 6 (𝑥𝐷 → ((𝐺𝐷)‘𝑥) = (𝐺𝑥))
53, 4oveq12d 6628 . . . . 5 (𝑥𝐷 → (((𝐹𝐷)‘𝑥)𝑅((𝐺𝐷)‘𝑥)) = ((𝐹𝑥)𝑅(𝐺𝑥)))
62, 5syl 17 . . . 4 (𝑥 ∈ ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) → (((𝐹𝐷)‘𝑥)𝑅((𝐺𝐷)‘𝑥)) = ((𝐹𝑥)𝑅(𝐺𝑥)))
76mpteq2ia 4705 . . 3 (𝑥 ∈ ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) ↦ (((𝐹𝐷)‘𝑥)𝑅((𝐺𝐷)‘𝑥))) = (𝑥 ∈ ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) ↦ ((𝐹𝑥)𝑅(𝐺𝑥)))
8 inindi 3813 . . . . 5 (𝐷 ∩ (dom 𝐹 ∩ dom 𝐺)) = ((𝐷 ∩ dom 𝐹) ∩ (𝐷 ∩ dom 𝐺))
9 incom 3788 . . . . 5 ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) = (𝐷 ∩ (dom 𝐹 ∩ dom 𝐺))
10 dmres 5383 . . . . . 6 dom (𝐹𝐷) = (𝐷 ∩ dom 𝐹)
11 dmres 5383 . . . . . 6 dom (𝐺𝐷) = (𝐷 ∩ dom 𝐺)
1210, 11ineq12i 3795 . . . . 5 (dom (𝐹𝐷) ∩ dom (𝐺𝐷)) = ((𝐷 ∩ dom 𝐹) ∩ (𝐷 ∩ dom 𝐺))
138, 9, 123eqtr4ri 2654 . . . 4 (dom (𝐹𝐷) ∩ dom (𝐺𝐷)) = ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷)
14 eqid 2621 . . . 4 (((𝐹𝐷)‘𝑥)𝑅((𝐺𝐷)‘𝑥)) = (((𝐹𝐷)‘𝑥)𝑅((𝐺𝐷)‘𝑥))
1513, 14mpteq12i 4707 . . 3 (𝑥 ∈ (dom (𝐹𝐷) ∩ dom (𝐺𝐷)) ↦ (((𝐹𝐷)‘𝑥)𝑅((𝐺𝐷)‘𝑥))) = (𝑥 ∈ ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) ↦ (((𝐹𝐷)‘𝑥)𝑅((𝐺𝐷)‘𝑥)))
16 resmpt3 5414 . . 3 ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) ↾ 𝐷) = (𝑥 ∈ ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) ↦ ((𝐹𝑥)𝑅(𝐺𝑥)))
177, 15, 163eqtr4ri 2654 . 2 ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) ↾ 𝐷) = (𝑥 ∈ (dom (𝐹𝐷) ∩ dom (𝐺𝐷)) ↦ (((𝐹𝐷)‘𝑥)𝑅((𝐺𝐷)‘𝑥)))
18 offval3 7114 . . 3 ((𝐹𝑉𝐺𝑊) → (𝐹𝑓 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))))
1918reseq1d 5360 . 2 ((𝐹𝑉𝐺𝑊) → ((𝐹𝑓 𝑅𝐺) ↾ 𝐷) = ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) ↾ 𝐷))
20 resexg 5406 . . 3 (𝐹𝑉 → (𝐹𝐷) ∈ V)
21 resexg 5406 . . 3 (𝐺𝑊 → (𝐺𝐷) ∈ V)
22 offval3 7114 . . 3 (((𝐹𝐷) ∈ V ∧ (𝐺𝐷) ∈ V) → ((𝐹𝐷) ∘𝑓 𝑅(𝐺𝐷)) = (𝑥 ∈ (dom (𝐹𝐷) ∩ dom (𝐺𝐷)) ↦ (((𝐹𝐷)‘𝑥)𝑅((𝐺𝐷)‘𝑥))))
2320, 21, 22syl2an 494 . 2 ((𝐹𝑉𝐺𝑊) → ((𝐹𝐷) ∘𝑓 𝑅(𝐺𝐷)) = (𝑥 ∈ (dom (𝐹𝐷) ∩ dom (𝐺𝐷)) ↦ (((𝐹𝐷)‘𝑥)𝑅((𝐺𝐷)‘𝑥))))
2417, 19, 233eqtr4a 2681 1 ((𝐹𝑉𝐺𝑊) → ((𝐹𝑓 𝑅𝐺) ↾ 𝐷) = ((𝐹𝐷) ∘𝑓 𝑅(𝐺𝐷)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1987  Vcvv 3189   ∩ cin 3558   ↦ cmpt 4678  dom cdm 5079   ↾ cres 5081  ‘cfv 5852  (class class class)co 6610   ∘𝑓 cof 6855 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-rep 4736  ax-sep 4746  ax-nul 4754  ax-pr 4872  ax-un 6909 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  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-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-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  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-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857 This theorem is referenced by:  pwssplit2  18992  pwssplit3  18993  islindf4  20109  tsmsadd  21873  jensen  24632  fdivmpt  41652
 Copyright terms: Public domain W3C validator