Theorem ofval 7667

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 2731	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐹‘𝑥))
7		eqidd 2731	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = (𝐺‘𝑥))
8	1, 2, 3, 4, 5, 6, 7	offval 7665	. . . 4 ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))))
9	8	fveq1d 6863	. . 3 ⊢ (𝜑 → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = ((𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))‘𝑋))
10	9	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = ((𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))‘𝑋))
11		fveq2 6861	. . . . 5 ⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋))
12		fveq2 6861	. . . . 5 ⊢ (𝑥 = 𝑋 → (𝐺‘𝑥) = (𝐺‘𝑋))
13	11, 12	oveq12d 7408	. . . 4 ⊢ (𝑥 = 𝑋 → ((𝐹‘𝑥)𝑅(𝐺‘𝑥)) = ((𝐹‘𝑋)𝑅(𝐺‘𝑋)))
14		eqid 2730	. . . 4 ⊢ (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) = (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))
15		ovex 7423	. . . 4 ⊢ ((𝐹‘𝑋)𝑅(𝐺‘𝑋)) ∈ V
16	13, 14, 15	fvmpt 6971	. . 3 ⊢ (𝑋 ∈ 𝑆 → ((𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))‘𝑋) = ((𝐹‘𝑋)𝑅(𝐺‘𝑋)))
17	16	adantl 481	. 2 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))‘𝑋) = ((𝐹‘𝑋)𝑅(𝐺‘𝑋)))
18		inss1 4203	. . . . . 6 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴
19	5, 18	eqsstrri 3997	. . . . 5 ⊢ 𝑆 ⊆ 𝐴
20	19	sseli 3945	. . . 4 ⊢ (𝑋 ∈ 𝑆 → 𝑋 ∈ 𝐴)
21		ofval.6	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶)
22	20, 21	sylan2 593	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) = 𝐶)
23		inss2 4204	. . . . . 6 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵
24	5, 23	eqsstrri 3997	. . . . 5 ⊢ 𝑆 ⊆ 𝐵
25	24	sseli 3945	. . . 4 ⊢ (𝑋 ∈ 𝑆 → 𝑋 ∈ 𝐵)
26		ofval.7	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐺‘𝑋) = 𝐷)
27	25, 26	sylan2 593	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → (𝐺‘𝑋) = 𝐷)
28	22, 27	oveq12d 7408	. 2 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹‘𝑋)𝑅(𝐺‘𝑋)) = (𝐶𝑅𝐷))
29	10, 17, 28	3eqtrd 2769	1 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = (𝐶𝑅𝐷))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ∩ cin 3916   ↦ cmpt 5191   Fn wfn 6509  ‘cfv 6514  (class class class)co 7390   ∘_f cof 7654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-of 7656

This theorem is referenced by:  fnfvof  7673  offveq  7682  ofc1  7684  ofc2  7685  suppofss1d  8186  suppofss2d  8187  ofsubeq0  12190  ofnegsub  12191  ofsubge0  12192  seqof  14031  o1of2  15586  mndpsuppss  18699  gsumzaddlem  19858  pwspjmhmmgpd  20244  psrbagcon  21841  psrbagleadd1  21844  psrbagconf1o  21845  psrdi  21881  psrdir  21882  mplsubglem  21915  psdmplcl  22056  psdadd  22057  psdmul  22060  psdmvr  22063  matplusgcell  22327  matsubgcell  22328  rrxcph  25299  mbfaddlem  25568  i1faddlem  25601  i1fmullem  25602  itg1lea  25620  mbfi1flimlem  25630  itg2split  25657  itg2monolem1  25658  itg2addlem  25666  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  plyaddlem1  26125  coeeulem  26136  coeaddlem  26161  dgradd2  26181  dgrcolem2  26187  ofmulrt  26196  plydivlem3  26210  plydivlem4  26211  plydiveu  26213  plyrem  26220  vieta1lem2  26226  elqaalem3  26236  qaa  26238  basellem7  27004  basellem9  27006  elrgspnlem1  33200  ply1degltdimlem  33625  circlemethhgt  34641  poimirlem1  37622  poimirlem2  37623  poimirlem6  37627  poimirlem7  37628  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem17  37638  poimirlem20  37641  poimirlem23  37644  poimirlem29  37650  poimirlem31  37652  poimirlem32  37653  broucube  37655  itg2addnclem3  37674  itg2addnc  37675  ftc1anclem5  37698  lfladdcl  39071  ldualvaddval  39131  ofun  42231  mplmapghm  42551  fsuppind  42585  dgrsub2  43131  mpaaeu  43146  caofcan  44319  ofmul12  44321  ofdivrec  44322  ofdivcan4  44323  ofdivdiv2  44324  binomcxplemrat  44346  binomcxplemnotnn0  44352  amgmwlem  49795