Theorem ofval 7675

Description: Evaluate a function operation at a point. (Contributed by Mario Carneiro, 20-Jul-2014.)

Hypotheses

Ref	Expression
offval.1	⊢ (𝜑 → 𝐹 Fn 𝐴)
offval.2	⊢ (𝜑 → 𝐺 Fn 𝐵)
offval.3	⊢ (𝜑 → 𝐴 ∈ 𝑉)
offval.4	⊢ (𝜑 → 𝐵 ∈ 𝑊)
offval.5	⊢ (𝐴 ∩ 𝐵) = 𝑆
ofval.6	⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶)
ofval.7	⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐺‘𝑋) = 𝐷)

Assertion

Ref	Expression
ofval	⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = (𝐶𝑅𝐷))

Proof of Theorem ofval

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		offval.1	. . . . 5 ⊢ (𝜑 → 𝐹 Fn 𝐴)
2		offval.2	. . . . 5 ⊢ (𝜑 → 𝐺 Fn 𝐵)
3		offval.3	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
4		offval.4	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
5		offval.5	. . . . 5 ⊢ (𝐴 ∩ 𝐵) = 𝑆
6		eqidd 2766	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐹‘𝑥))
7		eqidd 2766	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = (𝐺‘𝑥))
8	1, 2, 3, 4, 5, 6, 7	offval 7673	. . . 4 ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))))
9	8	fveq1d 6873	. . 3 ⊢ (𝜑 → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = ((𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))‘𝑋))
10	9	adantr 485	. 2 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = ((𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))‘𝑋))
11		fveq2 6871	. . . . 5 ⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋))
12		fveq2 6871	. . . . 5 ⊢ (𝑥 = 𝑋 → (𝐺‘𝑥) = (𝐺‘𝑋))
13	11, 12	oveq12d 7418	. . . 4 ⊢ (𝑥 = 𝑋 → ((𝐹‘𝑥)𝑅(𝐺‘𝑥)) = ((𝐹‘𝑋)𝑅(𝐺‘𝑋)))
14		eqid 2765	. . . 4 ⊢ (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) = (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))
15		ovex 7433	. . . 4 ⊢ ((𝐹‘𝑋)𝑅(𝐺‘𝑋)) ∈ V
16	13, 14, 15	fvmpt 6979	. . 3 ⊢ (𝑋 ∈ 𝑆 → ((𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))‘𝑋) = ((𝐹‘𝑋)𝑅(𝐺‘𝑋)))
17	16	adantl 486	. 2 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))‘𝑋) = ((𝐹‘𝑋)𝑅(𝐺‘𝑋)))
18		inss1 4191	. . . . . 6 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴
19	5, 18	eqsstrri 3986	. . . . 5 ⊢ 𝑆 ⊆ 𝐴
20	19	sseli 3935	. . . 4 ⊢ (𝑋 ∈ 𝑆 → 𝑋 ∈ 𝐴)
21		ofval.6	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶)
22	20, 21	sylan2 604	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) = 𝐶)
23		inss2 4192	. . . . . 6 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵
24	5, 23	eqsstrri 3986	. . . . 5 ⊢ 𝑆 ⊆ 𝐵
25	24	sseli 3935	. . . 4 ⊢ (𝑋 ∈ 𝑆 → 𝑋 ∈ 𝐵)
26		ofval.7	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐺‘𝑋) = 𝐷)
27	25, 26	sylan2 604	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → (𝐺‘𝑋) = 𝐷)
28	22, 27	oveq12d 7418	. 2 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹‘𝑋)𝑅(𝐺‘𝑋)) = (𝐶𝑅𝐷))
29	10, 17, 28	3eqtrd 2804	1 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = (𝐶𝑅𝐷))

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145   ∩ cin 3906   ↦ cmpt 5186   Fn wfn 6520  ‘cfv 6525  (class class class)co 7400   ∘_f cof 7662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5232  ax-sep 5251  ax-nul 5261  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-of 7664

This theorem is referenced by:  fnfvof  7681  offveq  7690  ofc1  7692  ofc2  7693  suppofss1d  8188  suppofss2d  8189  ofsubeq0  12206  ofnegsub  12207  ofsubge0  12208  seqof  14086  o1of2  15654  mndpsuppss  18813  gsumzaddlem  19982  pwspjmhmmgpd  20400  psrbagcon  22035  psrbagleadd1  22038  psrbagconf1o  22039  psrdi  22074  psrdir  22075  mplsubglem  22108  mplmapghm  22233  psdmplcl  22285  psdadd  22286  psdmul  22289  psdmvr  22292  matplusgcell  22551  matsubgcell  22552  rrxcph  25512  mbfaddlem  25780  i1faddlem  25813  i1fmullem  25814  itg1lea  25832  mbfi1flimlem  25842  itg2split  25869  itg2monolem1  25870  itg2addlem  25878  dvaddbr  26058  dvmulbr  26059  plyaddlem1  26331  coeeulem  26342  coeaddlem  26367  dgradd2  26386  dgrcolem2  26392  ofmulrt  26401  plydivlem3  26417  plydivlem4  26418  plydiveu  26420  plyrem  26427  vieta1lem2  26433  elqaalem3  26443  qaa  26445  basellem7  27209  basellem9  27211  elrgspnlem1  33475  0mplrim  33821  selvply1rhmlemb  33826  selvply1rhmlem4  33830  ply1degltdimlem  33929  circlemethhgt  34947  poimirlem1  38132  poimirlem2  38133  poimirlem6  38137  poimirlem7  38138  poimirlem10  38141  poimirlem11  38142  poimirlem12  38143  poimirlem17  38148  poimirlem20  38151  poimirlem23  38154  poimirlem29  38160  poimirlem31  38162  poimirlem32  38163  broucube  38165  itg2addnclem3  38184  itg2addnc  38185  ftc1anclem5  38208  lfladdcl  39707  ldualvaddval  39767  ofun  42866  fsuppind  43184  dgrsub2  43724  mpaaeu  43739  caofcan  44897  ofmul12  44899  ofdivrec  44900  ofdivcan4  44901  ofdivdiv2  44902  binomcxplemrat  44924  binomcxplemnotnn0  44930  amgmwlem  50431