Theorem offval2 7562

Description: The function operation expressed as a mapping. (Contributed by Mario Carneiro, 20-Jul-2014.)

Hypotheses

Ref	Expression
offval2.1	⊢ (𝜑 → 𝐴 ∈ 𝑉)
offval2.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
offval2.3	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋)
offval2.4	⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))
offval2.5	⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶))

Assertion

Ref	Expression
offval2	⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶)))

Distinct variable groups:   𝑥,𝐴   𝜑,𝑥   𝑥,𝑅

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝐹(𝑥)   𝐺(𝑥)   𝑉(𝑥)   𝑊(𝑥)   𝑋(𝑥)

Proof of Theorem offval2

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		offval2.2	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
2	1	ralrimiva 3104	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊)
3		eqid 2739	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	fnmpt 6582	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴)
5	2, 4	syl 17	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴)
6		offval2.4	. . . . 5 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))
7	6	fneq1d 6535	. . . 4 ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴))
8	5, 7	mpbird 256	. . 3 ⊢ (𝜑 → 𝐹 Fn 𝐴)
9		offval2.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋)
10	9	ralrimiva 3104	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝑋)
11		eqid 2739	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ 𝐶)
12	11	fnmpt 6582	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝑋 → (𝑥 ∈ 𝐴 ↦ 𝐶) Fn 𝐴)
13	10, 12	syl 17	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) Fn 𝐴)
14		offval2.5	. . . . 5 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶))
15	14	fneq1d 6535	. . . 4 ⊢ (𝜑 → (𝐺 Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ 𝐶) Fn 𝐴))
16	13, 15	mpbird 256	. . 3 ⊢ (𝜑 → 𝐺 Fn 𝐴)
17		offval2.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
18		inidm 4153	. . 3 ⊢ (𝐴 ∩ 𝐴) = 𝐴
19	6	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))
20	19	fveq1d 6785	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦))
21	14	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶))
22	21	fveq1d 6785	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐺‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦))
23	8, 16, 17, 17, 18, 20, 22	offval 7551	. 2 ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑦 ∈ 𝐴 ↦ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦))))
24		nffvmpt1 6794	. . . . 5 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)
25		nfcv 2908	. . . . 5 ⊢ Ⅎ𝑥𝑅
26		nffvmpt1 6794	. . . . 5 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦)
27	24, 25, 26	nfov 7314	. . . 4 ⊢ Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦))
28		nfcv 2908	. . . 4 ⊢ Ⅎ𝑦(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥))
29		fveq2 6783	. . . . 5 ⊢ (𝑦 = 𝑥 → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
30		fveq2 6783	. . . . 5 ⊢ (𝑦 = 𝑥 → ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥))
31	29, 30	oveq12d 7302	. . . 4 ⊢ (𝑦 = 𝑥 → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦)) = (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥)))
32	27, 28, 31	cbvmpt 5186	. . 3 ⊢ (𝑦 ∈ 𝐴 ↦ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦))) = (𝑥 ∈ 𝐴 ↦ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥)))
33		simpr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
34	3	fvmpt2 6895	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑊) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
35	33, 1, 34	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
36	11	fvmpt2 6895	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝑋) → ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥) = 𝐶)
37	33, 9, 36	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥) = 𝐶)
38	35, 37	oveq12d 7302	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥)) = (𝐵𝑅𝐶))
39	38	mpteq2dva 5175	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥))) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶)))
40	32, 39	eqtrid 2791	. 2 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦))) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶)))
41	23, 40	eqtrd 2779	1 ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶)))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2107  ∀wral 3065   ↦ cmpt 5158   Fn wfn 6432  ‘cfv 6437  (class class class)co 7284   ∘_f cof 7540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-ov 7287  df-oprab 7288  df-mpo 7289  df-of 7542

This theorem is referenced by:  ofmpteq  7564  ofc12  7570  caofinvl  7572  caofcom  7577  caofass  7579  caofdi  7581  caofdir  7582  caonncan  7583  offval22  7937  ofccat  14689  ofs1  14690  o1add2  15342  o1mul2  15343  o1sub2  15344  o1dif  15348  fsumo1  15533  pwsplusgval  17210  pwsmulrval  17211  pwsvscafval  17214  pwsco1mhm  18479  pwsco2mhm  18480  pwssub  18698  gsumzaddlem  19531  gsummptfsadd  19534  gsummptfidmadd2  19536  gsumzsplit  19537  gsumsub  19558  gsummptfssub  19559  dprdfadd  19632  dprdfsub  19633  dprdfeq0  19634  dprdf11  19635  lmhmvsca  20316  rrgsupp  20571  uvcresum  21009  psrbagaddclOLD  21141  psrass1lemOLD  21152  psrass1lem  21155  psrlinv  21175  psrass1  21183  psrdi  21184  psrdir  21185  psrass23l  21186  psrcom  21187  psrass23  21188  mplsubrglem  21219  mplmonmul  21246  mplcoe1  21247  mplcoe3  21248  mplcoe5  21250  mplmon2  21278  evlslem1  21301  mhpmulcl  21348  coe1sclmul  21462  coe1sclmul2  21464  grpvrinv  21554  mhmvlin  21555  mamudi  21559  mamudir  21560  mdetunilem9  21778  tsmssub  23309  tgptsmscls  23310  tsmssplit  23312  tsmsxplem2  23314  ovolctb  24663  mbfmulc2re  24821  mbfneg  24823  mbfadd  24834  mbfsub  24835  mbfmulc2  24836  mbfmul  24900  itg2const  24914  itg2mulclem  24920  itg2mulc  24921  itg2splitlem  24922  itg2monolem1  24924  i1fibl  24981  itgitg1  24982  ibladdlem  24993  ibladd  24994  itgaddlem1  24996  iblabslem  25001  iblabs  25002  iblmulc2  25004  itgmulc2lem1  25005  bddmulibl  25012  dvmulf  25116  dvcmulf  25118  dvcof  25121  dvexp  25126  dvmptadd  25133  dvmptmul  25134  dvmptco  25145  dvef  25153  dv11cn  25174  itgsubstlem  25221  mdegmullem  25252  plypf1  25382  plyaddlem1  25383  plymullem1  25384  plyco  25411  dgrcolem1  25443  dgrcolem2  25444  plydiveu  25467  plyremlem  25473  elqaalem3  25490  iaa  25494  taylply2  25536  ulmdvlem1  25568  iblulm  25575  jensenlem2  26146  amgmlem  26148  ftalem7  26237  basellem8  26246  basellem9  26247  dchrmulid2  26409  dchrinvcl  26410  dchrfi  26412  lgseisenlem3  26534  lgseisenlem4  26535  chtppilimlem2  26631  chebbnd2  26634  chto1lb  26635  chpchtlim  26636  chpo1ub  26637  vmadivsum  26639  rpvmasumlem  26644  mudivsum  26687  selberglem1  26702  selberglem2  26703  selberg2lem  26707  selberg2  26708  pntrsumo1  26722  selbergr  26725  ofoprabco  31010  pl1cn  31914  esumadd  32034  poimirlem16  35802  poimirlem19  35805  itg2addnclem  35837  itg2addnclem3  35839  ibladdnclem  35842  itgaddnclem1  35844  iblabsnclem  35849  iblabsnc  35850  iblmulc2nc  35851  itgmulc2nclem1  35852  itgmulc2nclem2  35853  itgmulc2nc  35854  itgabsnc  35855  ftc1anclem3  35861  ftc1anclem4  35862  ftc1anclem5  35863  ftc1anclem6  35864  ftc1anclem7  35865  ftc1anclem8  35866  3factsumint1  40036  mendlmod  41025  mendassa  41026  expgrowthi  41958  expgrowth  41960  binomcxplemrat  41975  mulcncff  43418  subcncff  43428  addcncff  43432  divcncff  43439  dvsubf  43462  dvdivf  43470  fourierdlem16  43671  fourierdlem21  43676  fourierdlem22  43677  fourierdlem58  43712  fourierdlem59  43713  fourierdlem72  43726  fourierdlem83  43737  offvalfv  45689  aacllem  46516  amgmwlem  46517  amgmlemALT  46518