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

Theorem offval 7102
Description: Value of an operation applied to two functions. (Contributed by Mario Carneiro, 20-Jul-2014.)
Hypotheses
Ref Expression
offval.1 (𝜑𝐹 Fn 𝐴)
offval.2 (𝜑𝐺 Fn 𝐵)
offval.3 (𝜑𝐴𝑉)
offval.4 (𝜑𝐵𝑊)
offval.5 (𝐴𝐵) = 𝑆
offval.6 ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐶)
offval.7 ((𝜑𝑥𝐵) → (𝐺𝑥) = 𝐷)
Assertion
Ref Expression
offval (𝜑 → (𝐹𝑓 𝑅𝐺) = (𝑥𝑆 ↦ (𝐶𝑅𝐷)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹   𝑥,𝐺   𝜑,𝑥   𝑥,𝑆   𝑥,𝑅
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝐷(𝑥)   𝑉(𝑥)   𝑊(𝑥)

Proof of Theorem offval
Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 offval.1 . . . 4 (𝜑𝐹 Fn 𝐴)
2 offval.3 . . . 4 (𝜑𝐴𝑉)
3 fnex 6674 . . . 4 ((𝐹 Fn 𝐴𝐴𝑉) → 𝐹 ∈ V)
41, 2, 3syl2anc 579 . . 3 (𝜑𝐹 ∈ V)
5 offval.2 . . . 4 (𝜑𝐺 Fn 𝐵)
6 offval.4 . . . 4 (𝜑𝐵𝑊)
7 fnex 6674 . . . 4 ((𝐺 Fn 𝐵𝐵𝑊) → 𝐺 ∈ V)
85, 6, 7syl2anc 579 . . 3 (𝜑𝐺 ∈ V)
9 fndm 6168 . . . . . . . 8 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
101, 9syl 17 . . . . . . 7 (𝜑 → dom 𝐹 = 𝐴)
11 fndm 6168 . . . . . . . 8 (𝐺 Fn 𝐵 → dom 𝐺 = 𝐵)
125, 11syl 17 . . . . . . 7 (𝜑 → dom 𝐺 = 𝐵)
1310, 12ineq12d 3977 . . . . . 6 (𝜑 → (dom 𝐹 ∩ dom 𝐺) = (𝐴𝐵))
14 offval.5 . . . . . 6 (𝐴𝐵) = 𝑆
1513, 14syl6eq 2815 . . . . 5 (𝜑 → (dom 𝐹 ∩ dom 𝐺) = 𝑆)
1615mpteq1d 4897 . . . 4 (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) = (𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥))))
17 inex1g 4962 . . . . . 6 (𝐴𝑉 → (𝐴𝐵) ∈ V)
1814, 17syl5eqelr 2849 . . . . 5 (𝐴𝑉𝑆 ∈ V)
19 mptexg 6677 . . . . 5 (𝑆 ∈ V → (𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) ∈ V)
202, 18, 193syl 18 . . . 4 (𝜑 → (𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) ∈ V)
2116, 20eqeltrd 2844 . . 3 (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) ∈ V)
22 dmeq 5492 . . . . . 6 (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
23 dmeq 5492 . . . . . 6 (𝑔 = 𝐺 → dom 𝑔 = dom 𝐺)
2422, 23ineqan12d 3978 . . . . 5 ((𝑓 = 𝐹𝑔 = 𝐺) → (dom 𝑓 ∩ dom 𝑔) = (dom 𝐹 ∩ dom 𝐺))
25 fveq1 6374 . . . . . 6 (𝑓 = 𝐹 → (𝑓𝑥) = (𝐹𝑥))
26 fveq1 6374 . . . . . 6 (𝑔 = 𝐺 → (𝑔𝑥) = (𝐺𝑥))
2725, 26oveqan12d 6861 . . . . 5 ((𝑓 = 𝐹𝑔 = 𝐺) → ((𝑓𝑥)𝑅(𝑔𝑥)) = ((𝐹𝑥)𝑅(𝐺𝑥)))
2824, 27mpteq12dv 4892 . . . 4 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓𝑥)𝑅(𝑔𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))))
29 df-of 7095 . . . 4 𝑓 𝑅 = (𝑓 ∈ V, 𝑔 ∈ V ↦ (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓𝑥)𝑅(𝑔𝑥))))
3028, 29ovmpt2ga 6988 . . 3 ((𝐹 ∈ V ∧ 𝐺 ∈ V ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) ∈ V) → (𝐹𝑓 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))))
314, 8, 21, 30syl3anc 1490 . 2 (𝜑 → (𝐹𝑓 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))))
3214eleq2i 2836 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝑆)
33 elin 3958 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
3432, 33bitr3i 268 . . . 4 (𝑥𝑆 ↔ (𝑥𝐴𝑥𝐵))
35 offval.6 . . . . . 6 ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐶)
3635adantrr 708 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑥𝐵)) → (𝐹𝑥) = 𝐶)
37 offval.7 . . . . . 6 ((𝜑𝑥𝐵) → (𝐺𝑥) = 𝐷)
3837adantrl 707 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑥𝐵)) → (𝐺𝑥) = 𝐷)
3936, 38oveq12d 6860 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑥𝐵)) → ((𝐹𝑥)𝑅(𝐺𝑥)) = (𝐶𝑅𝐷))
4034, 39sylan2b 587 . . 3 ((𝜑𝑥𝑆) → ((𝐹𝑥)𝑅(𝐺𝑥)) = (𝐶𝑅𝐷))
4140mpteq2dva 4903 . 2 (𝜑 → (𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) = (𝑥𝑆 ↦ (𝐶𝑅𝐷)))
4231, 16, 413eqtrd 2803 1 (𝜑 → (𝐹𝑓 𝑅𝐺) = (𝑥𝑆 ↦ (𝐶𝑅𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1652  wcel 2155  Vcvv 3350  cin 3731  cmpt 4888  dom cdm 5277   Fn wfn 6063  cfv 6068  (class class class)co 6842  𝑓 cof 7093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pr 5062
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095
This theorem is referenced by:  ofval  7104  offn  7106  offval2f  7107  off  7110  ofres  7111  offval2  7112  ofco  7115  offveqb  7117  suppssof1  7531  o1rlimmul  14634  gsumbagdiaglem  19649  evlslem1  19788  psrplusgpropd  19879  frlmipval  20394  frlmphllem  20395  frlmphl  20396  mat1dimscm  20558  rrxcph  23469  rrxds  23470  mbfadd  23719  mbfsub  23720  mbfmullem2  23782  mbfmul  23784  bddmulibl  23896  dvcmulf  23999  ofrn2  29892  off2  29893  ofresid  29894  ofcof  30616  plymul02  31072  signsplypnf  31076  signsply0  31077  matunitlindflem1  33829  matunitlindflem2  33830  poimirlem3  33836  poimirlem4  33837  poimirlem16  33849  poimirlem19  33852  poimirlem28  33861  broucube  33867  itg2addnc  33887  ftc1anclem8  33915  dflinc2  42868  fdivmpt  43003
  Copyright terms: Public domain W3C validator