Theorem fnfvof 7670

Description: Function value of a pointwise composition. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Proof shortened by Mario Carneiro, 5-Jun-2015.)

Assertion

Ref	Expression
fnfvof	⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴)) → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = ((𝐹‘𝑋)𝑅(𝐺‘𝑋)))

Proof of Theorem fnfvof

Step	Hyp	Ref	Expression
1		simpll 766	. . 3 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ 𝐴 ∈ 𝑉) → 𝐹 Fn 𝐴)
2		simplr 768	. . 3 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ 𝐴 ∈ 𝑉) → 𝐺 Fn 𝐴)
3		simpr 484	. . 3 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ 𝑉)
4		inidm 4190	. . 3 ⊢ (𝐴 ∩ 𝐴) = 𝐴
5		eqidd 2730	. . 3 ⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ 𝐴 ∈ 𝑉) ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = (𝐹‘𝑋))
6		eqidd 2730	. . 3 ⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ 𝐴 ∈ 𝑉) ∧ 𝑋 ∈ 𝐴) → (𝐺‘𝑋) = (𝐺‘𝑋))
7	1, 2, 3, 3, 4, 5, 6	ofval 7664	. 2 ⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ 𝐴 ∈ 𝑉) ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = ((𝐹‘𝑋)𝑅(𝐺‘𝑋)))
8	7	anasss 466	1 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴)) → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = ((𝐹‘𝑋)𝑅(𝐺‘𝑋)))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   Fn wfn 6506  ‘cfv 6511  (class class class)co 7387   ∘_f cof 7651

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 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-of 7653

This theorem is referenced by:  suppofssd  8182  ofccat  14935  ghmplusg  19776  lcomfsupp  20808  lmhmplusg  20951  frlmvplusgvalc  21676  frlmvscaval  21677  frlmsslsp  21705  frlmup1  21707  frlmup2  21708  islindf4  21747  evlslem3  21987  evlslem1  21989  coe1addfv  22151  evl1addd  22228  evl1subd  22229  evl1muld  22230  mamudi  22290  mamudir  22291  mdetrlin  22489  nmotri  24627  mdegaddle  25979  ply1rem  26071  fta1glem2  26074  fta1blem  26076  plyexmo  26221  ulmdvlem1  26309  jensen  26899  dchrmulcl  27160  dchrinv  27172  sumdchr2  27181  dchr2sum  27184  evlsaddval  42556  evlsmulval  42557  evladdval  42563  evlmulval  42564  mzpsubst  42736  mzpcong  42961  rngunsnply  43158  ofoafg  43343  ofoafo  43345  ofoaid1  43347  ofoaid2  43348  ofoaass  43349  ofoacom  43350  naddcnff  43351  naddcnffo  43353  naddcnfcom  43355  naddcnfid1  43356  naddcnfass  43358  cjnpoly  46890  lincsum  48418