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

Theorem offval 7675
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 (𝜑 → (𝐹f 𝑅𝐺) = (𝑥𝑆 ↦ (𝐶𝑅𝐷)))
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 7215 . . . 4 ((𝐹 Fn 𝐴𝐴𝑉) → 𝐹 ∈ V)
41, 2, 3syl2anc 584 . . 3 (𝜑𝐹 ∈ V)
5 offval.2 . . . 4 (𝜑𝐺 Fn 𝐵)
6 offval.4 . . . 4 (𝜑𝐵𝑊)
7 fnex 7215 . . . 4 ((𝐺 Fn 𝐵𝐵𝑊) → 𝐺 ∈ V)
85, 6, 7syl2anc 584 . . 3 (𝜑𝐺 ∈ V)
91fndmd 6651 . . . . . . 7 (𝜑 → dom 𝐹 = 𝐴)
105fndmd 6651 . . . . . . 7 (𝜑 → dom 𝐺 = 𝐵)
119, 10ineq12d 4212 . . . . . 6 (𝜑 → (dom 𝐹 ∩ dom 𝐺) = (𝐴𝐵))
12 offval.5 . . . . . 6 (𝐴𝐵) = 𝑆
1311, 12eqtrdi 2788 . . . . 5 (𝜑 → (dom 𝐹 ∩ dom 𝐺) = 𝑆)
1413mpteq1d 5242 . . . 4 (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) = (𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥))))
15 inex1g 5318 . . . . . 6 (𝐴𝑉 → (𝐴𝐵) ∈ V)
1612, 15eqeltrrid 2838 . . . . 5 (𝐴𝑉𝑆 ∈ V)
17 mptexg 7219 . . . . 5 (𝑆 ∈ V → (𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) ∈ V)
182, 16, 173syl 18 . . . 4 (𝜑 → (𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) ∈ V)
1914, 18eqeltrd 2833 . . 3 (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) ∈ V)
20 dmeq 5901 . . . . . 6 (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
21 dmeq 5901 . . . . . 6 (𝑔 = 𝐺 → dom 𝑔 = dom 𝐺)
2220, 21ineqan12d 4213 . . . . 5 ((𝑓 = 𝐹𝑔 = 𝐺) → (dom 𝑓 ∩ dom 𝑔) = (dom 𝐹 ∩ dom 𝐺))
23 fveq1 6887 . . . . . 6 (𝑓 = 𝐹 → (𝑓𝑥) = (𝐹𝑥))
24 fveq1 6887 . . . . . 6 (𝑔 = 𝐺 → (𝑔𝑥) = (𝐺𝑥))
2523, 24oveqan12d 7424 . . . . 5 ((𝑓 = 𝐹𝑔 = 𝐺) → ((𝑓𝑥)𝑅(𝑔𝑥)) = ((𝐹𝑥)𝑅(𝐺𝑥)))
2622, 25mpteq12dv 5238 . . . 4 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓𝑥)𝑅(𝑔𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))))
27 df-of 7666 . . . 4 f 𝑅 = (𝑓 ∈ V, 𝑔 ∈ V ↦ (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓𝑥)𝑅(𝑔𝑥))))
2826, 27ovmpoga 7558 . . 3 ((𝐹 ∈ V ∧ 𝐺 ∈ V ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) ∈ V) → (𝐹f 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))))
294, 8, 19, 28syl3anc 1371 . 2 (𝜑 → (𝐹f 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))))
3012eleq2i 2825 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝑆)
31 elin 3963 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
3230, 31bitr3i 276 . . . 4 (𝑥𝑆 ↔ (𝑥𝐴𝑥𝐵))
33 offval.6 . . . . . 6 ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐶)
3433adantrr 715 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑥𝐵)) → (𝐹𝑥) = 𝐶)
35 offval.7 . . . . . 6 ((𝜑𝑥𝐵) → (𝐺𝑥) = 𝐷)
3635adantrl 714 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑥𝐵)) → (𝐺𝑥) = 𝐷)
3734, 36oveq12d 7423 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑥𝐵)) → ((𝐹𝑥)𝑅(𝐺𝑥)) = (𝐶𝑅𝐷))
3832, 37sylan2b 594 . . 3 ((𝜑𝑥𝑆) → ((𝐹𝑥)𝑅(𝐺𝑥)) = (𝐶𝑅𝐷))
3938mpteq2dva 5247 . 2 (𝜑 → (𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) = (𝑥𝑆 ↦ (𝐶𝑅𝐷)))
4029, 14, 393eqtrd 2776 1 (𝜑 → (𝐹f 𝑅𝐺) = (𝑥𝑆 ↦ (𝐶𝑅𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  Vcvv 3474  cin 3946  cmpt 5230  dom cdm 5675   Fn wfn 6535  cfv 6540  (class class class)co 7405  f cof 7664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7666
This theorem is referenced by:  ofval  7677  offn  7679  offval2f  7681  off  7684  ofres  7685  offval2  7686  ofco  7689  offveqb  7691  suppssof1  8180  o1rlimmul  15559  frlmipval  21325  frlmphllem  21326  frlmphl  21327  gsumbagdiaglemOLD  21482  gsumbagdiaglem  21485  evlslem1  21636  mhpmulcl  21683  psrplusgpropd  21749  mat1dimscm  21968  rrxcph  24900  rrxds  24901  mbfadd  25169  mbfsub  25170  mbfmullem2  25233  mbfmul  25235  bddmulibl  25347  dvcmulf  25453  ofrn2  31852  off2  31853  ofresid  31854  islinds5  32468  ellspds  32469  evls1fpws  32634  ply1gsumz  32657  ofcof  33093  plymul02  33545  signsplypnf  33549  signsply0  33550  matunitlindflem1  36472  matunitlindflem2  36473  poimirlem3  36479  poimirlem4  36480  poimirlem16  36492  poimirlem19  36495  poimirlem28  36504  broucube  36510  itg2addnc  36530  ftc1anclem8  36556  evlsvvval  41132  dflinc2  47044  fdivmpt  47179
  Copyright terms: Public domain W3C validator