Theorem fnfvof 7673

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 4193	. . 3 ⊢ (𝐴 ∩ 𝐴) = 𝐴
5		eqidd 2731	. . 3 ⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ 𝐴 ∈ 𝑉) ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = (𝐹‘𝑋))
6		eqidd 2731	. . 3 ⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ 𝐴 ∈ 𝑉) ∧ 𝑋 ∈ 𝐴) → (𝐺‘𝑋) = (𝐺‘𝑋))
7	1, 2, 3, 3, 4, 5, 6	ofval 7667	. 2 ⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ 𝐴 ∈ 𝑉) ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = ((𝐹‘𝑋)𝑅(𝐺‘𝑋)))
8	7	anasss 466	1 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴)) → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = ((𝐹‘𝑋)𝑅(𝐺‘𝑋)))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   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:  suppofssd  8185  ofccat  14942  ghmplusg  19783  lcomfsupp  20815  lmhmplusg  20958  frlmvplusgvalc  21683  frlmvscaval  21684  frlmsslsp  21712  frlmup1  21714  frlmup2  21715  islindf4  21754  evlslem3  21994  evlslem1  21996  coe1addfv  22158  evl1addd  22235  evl1subd  22236  evl1muld  22237  mamudi  22297  mamudir  22298  mdetrlin  22496  nmotri  24634  mdegaddle  25986  ply1rem  26078  fta1glem2  26081  fta1blem  26083  plyexmo  26228  ulmdvlem1  26316  jensen  26906  dchrmulcl  27167  dchrinv  27179  sumdchr2  27188  dchr2sum  27191  evlsaddval  42563  evlsmulval  42564  evladdval  42570  evlmulval  42571  mzpsubst  42743  mzpcong  42968  rngunsnply  43165  ofoafg  43350  ofoafo  43352  ofoaid1  43354  ofoaid2  43355  ofoaass  43356  ofoacom  43357  naddcnff  43358  naddcnffo  43360  naddcnfcom  43362  naddcnfid1  43363  naddcnfass  43365  lincsum  48422