Theorem offval2 7652

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 3130	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊)
3		eqid 2737	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	fnmpt 6640	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴)
5	2, 4	syl 17	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴)
6		offval2.4	. . . . 5 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))
7	6	fneq1d 6593	. . . 4 ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴))
8	5, 7	mpbird 257	. . 3 ⊢ (𝜑 → 𝐹 Fn 𝐴)
9		offval2.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋)
10	9	ralrimiva 3130	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝑋)
11		eqid 2737	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ 𝐶)
12	11	fnmpt 6640	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝑋 → (𝑥 ∈ 𝐴 ↦ 𝐶) Fn 𝐴)
13	10, 12	syl 17	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) Fn 𝐴)
14		offval2.5	. . . . 5 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶))
15	14	fneq1d 6593	. . . 4 ⊢ (𝜑 → (𝐺 Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ 𝐶) Fn 𝐴))
16	13, 15	mpbird 257	. . 3 ⊢ (𝜑 → 𝐺 Fn 𝐴)
17		offval2.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
18		inidm 4181	. . 3 ⊢ (𝐴 ∩ 𝐴) = 𝐴
19	6	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))
20	19	fveq1d 6844	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦))
21	14	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶))
22	21	fveq1d 6844	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐺‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦))
23	8, 16, 17, 17, 18, 20, 22	offval 7641	. 2 ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑦 ∈ 𝐴 ↦ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦))))
24		nffvmpt1 6853	. . . . 5 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)
25		nfcv 2899	. . . . 5 ⊢ Ⅎ𝑥𝑅
26		nffvmpt1 6853	. . . . 5 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦)
27	24, 25, 26	nfov 7398	. . . 4 ⊢ Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦))
28		nfcv 2899	. . . 4 ⊢ Ⅎ𝑦(((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥))
29		fveq2 6842	. . . . 5 ⊢ (𝑦 = 𝑥 → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
30		fveq2 6842	. . . . 5 ⊢ (𝑦 = 𝑥 → ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥))
31	29, 30	oveq12d 7386	. . . 4 ⊢ (𝑦 = 𝑥 → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦)) = (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥)))
32	27, 28, 31	cbvmpt 5202	. . 3 ⊢ (𝑦 ∈ 𝐴 ↦ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦))) = (𝑥 ∈ 𝐴 ↦ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥)))
33		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
34	3	fvmpt2 6961	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑊) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
35	33, 1, 34	syl2anc 585	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
36	11	fvmpt2 6961	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝑋) → ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥) = 𝐶)
37	33, 9, 36	syl2anc 585	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥) = 𝐶)
38	35, 37	oveq12d 7386	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥)) = (𝐵𝑅𝐶))
39	38	mpteq2dva 5193	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥))) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶)))
40	32, 39	eqtrid 2784	. 2 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦))) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶)))
41	23, 40	eqtrd 2772	1 ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶)))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052   ↦ cmpt 5181   Fn wfn 6495  ‘cfv 6500  (class class class)co 7368   ∘_f cof 7630

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-of 7632

This theorem is referenced by:  offvalfv  7654  ofmpteq  7655  ofc12  7662  caofinvl  7664  caofcom  7669  caofidlcan  7670  caofass  7672  caofdi  7674  caofdir  7675  caonncan  7676  offval22  8040  ofccat  14904  ofs1  14905  o1add2  15559  o1mul2  15560  o1sub2  15561  o1dif  15565  fsumo1  15747  pwsplusgval  17423  pwsmulrval  17424  pwsvscafval  17427  mhmvlin  18738  pwsco1mhm  18769  pwsco2mhm  18770  pwssub  18996  gsumzaddlem  19862  gsummptfsadd  19865  gsummptfidmadd2  19867  gsumzsplit  19868  gsumsub  19889  gsummptfssub  19890  dprdfadd  19963  dprdfsub  19964  dprdfeq0  19965  dprdf11  19966  rrgsupp  20646  lmhmvsca  21009  uvcresum  21760  psrass1lem  21900  psrlinv  21923  psrass1  21931  psrdi  21932  psrdir  21933  psrass23l  21934  psrcom  21935  psrass23  21936  mplsubrglem  21971  mplmonmul  22003  mplcoe1  22004  mplcoe3  22005  mplcoe5  22007  mplmon2  22028  evlslem1  22049  mhpmulcl  22104  coe1sclmul  22236  coe1sclmul2  22238  grpvrinv  22355  mamudi  22359  mamudir  22360  mdetunilem9  22576  tsmssub  24105  tgptsmscls  24106  tsmssplit  24108  tsmsxplem2  24110  ovolctb  25459  mbfmulc2re  25617  mbfneg  25619  mbfadd  25630  mbfsub  25631  mbfmulc2  25632  mbfmul  25695  itg2const  25709  itg2mulclem  25715  itg2mulc  25716  itg2splitlem  25717  itg2monolem1  25719  i1fibl  25777  itgitg1  25778  ibladdlem  25789  ibladd  25790  itgaddlem1  25792  iblabslem  25797  iblabs  25798  iblmulc2  25800  itgmulc2lem1  25801  bddmulibl  25808  dvmulf  25914  dvcmulf  25916  dvcof  25920  dvexp  25925  dvmptadd  25932  dvmptmul  25933  dvmptco  25944  dvef  25952  dv11cn  25974  itgsubstlem  26023  mdegmullem  26051  plypf1  26185  plyaddlem1  26186  plymullem1  26187  plyco  26214  dgrcolem1  26247  dgrcolem2  26248  plydiveu  26274  plyremlem  26280  elqaalem3  26297  iaa  26301  taylply2  26343  taylply2OLD  26344  ulmdvlem1  26377  iblulm  26384  jensenlem2  26966  amgmlem  26968  ftalem7  27057  basellem8  27066  basellem9  27067  dchrmullid  27231  dchrinvcl  27232  dchrfi  27234  lgseisenlem3  27356  lgseisenlem4  27357  chtppilimlem2  27453  chebbnd2  27456  chto1lb  27457  chpchtlim  27458  chpo1ub  27459  vmadivsum  27461  rpvmasumlem  27466  mudivsum  27509  selberglem1  27524  selberglem2  27525  selberg2lem  27529  selberg2  27530  pntrsumo1  27544  selbergr  27547  ofoprabco  32753  psrmonmul  33726  pl1cn  34132  esumadd  34234  poimirlem16  37884  poimirlem19  37887  itg2addnclem  37919  itg2addnclem3  37921  ibladdnclem  37924  itgaddnclem1  37926  iblabsnclem  37931  iblabsnc  37932  iblmulc2nc  37933  itgmulc2nclem1  37934  itgmulc2nclem2  37935  itgmulc2nc  37936  itgabsnc  37937  ftc1anclem3  37943  ftc1anclem4  37944  ftc1anclem5  37945  ftc1anclem6  37946  ftc1anclem7  37947  ftc1anclem8  37948  3factsumint1  42388  mendlmod  43543  mendassa  43544  expgrowthi  44686  expgrowth  44688  binomcxplemrat  44703  mulcncff  46225  subcncff  46235  addcncff  46239  divcncff  46246  dvsubf  46269  dvdivf  46277  fourierdlem16  46478  fourierdlem21  46483  fourierdlem22  46484  fourierdlem58  46519  fourierdlem59  46520  fourierdlem72  46533  fourierdlem83  46544  aacllem  50157  amgmwlem  50158  amgmlemALT  50159