Theorem offval 7675

Description: Value of an operation applied to two functions. (Contributed by Mario Carneiro, 20-Jul-2014.)

Hypotheses

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

Assertion

Ref	Expression
offval	⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝑆 ↦ (𝐶𝑅𝐷)))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐹   𝑥,𝐺   𝜑,𝑥   𝑥,𝑆   𝑥,𝑅

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝐷(𝑥)   𝑉(𝑥)   𝑊(𝑥)

Proof of Theorem offval

Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		offval.1	. . . 4 ⊢ (𝜑 → 𝐹 Fn 𝐴)
2		offval.3	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3		fnex 7215	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V)
4	1, 2, 3	syl2anc 584	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
5		offval.2	. . . 4 ⊢ (𝜑 → 𝐺 Fn 𝐵)
6		offval.4	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
7		fnex 7215	. . . 4 ⊢ ((𝐺 Fn 𝐵 ∧ 𝐵 ∈ 𝑊) → 𝐺 ∈ V)
8	5, 6, 7	syl2anc 584	. . 3 ⊢ (𝜑 → 𝐺 ∈ V)
9	1	fndmd 6651	. . . . . . 7 ⊢ (𝜑 → dom 𝐹 = 𝐴)
10	5	fndmd 6651	. . . . . . 7 ⊢ (𝜑 → dom 𝐺 = 𝐵)
11	9, 10	ineq12d 4212	. . . . . 6 ⊢ (𝜑 → (dom 𝐹 ∩ dom 𝐺) = (𝐴 ∩ 𝐵))
12		offval.5	. . . . . 6 ⊢ (𝐴 ∩ 𝐵) = 𝑆
13	11, 12	eqtrdi 2788	. . . . 5 ⊢ (𝜑 → (dom 𝐹 ∩ dom 𝐺) = 𝑆)
14	13	mpteq1d 5242	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) = (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))))
15		inex1g 5318	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)
16	12, 15	eqeltrrid 2838	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → 𝑆 ∈ V)
17		mptexg 7219	. . . . 5 ⊢ (𝑆 ∈ V → (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) ∈ V)
18	2, 16, 17	3syl 18	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) ∈ V)
19	14, 18	eqeltrd 2833	. . 3 ⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) ∈ V)
20		dmeq 5901	. . . . . 6 ⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
21		dmeq 5901	. . . . . 6 ⊢ (𝑔 = 𝐺 → dom 𝑔 = dom 𝐺)
22	20, 21	ineqan12d 4213	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (dom 𝑓 ∩ dom 𝑔) = (dom 𝐹 ∩ dom 𝐺))
23		fveq1 6887	. . . . . 6 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑥) = (𝐹‘𝑥))
24		fveq1 6887	. . . . . 6 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑥) = (𝐺‘𝑥))
25	23, 24	oveqan12d 7424	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑓‘𝑥)𝑅(𝑔‘𝑥)) = ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))
26	22, 25	mpteq12dv 5238	. . . 4 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓‘𝑥)𝑅(𝑔‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))))
27		df-of 7666	. . . 4 ⊢ ∘f 𝑅 = (𝑓 ∈ V, 𝑔 ∈ V ↦ (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓‘𝑥)𝑅(𝑔‘𝑥))))
28	26, 27	ovmpoga 7558	. . 3 ⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) ∈ V) → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))))
29	4, 8, 19, 28	syl3anc 1371	. 2 ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))))
30	12	eleq2i 2825	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ 𝑥 ∈ 𝑆)
31		elin 3963	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
32	30, 31	bitr3i 276	. . . 4 ⊢ (𝑥 ∈ 𝑆 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
33		offval.6	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐶)
34	33	adantrr 715	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) → (𝐹‘𝑥) = 𝐶)
35		offval.7	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐷)
36	35	adantrl 714	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) → (𝐺‘𝑥) = 𝐷)
37	34, 36	oveq12d 7423	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) → ((𝐹‘𝑥)𝑅(𝐺‘𝑥)) = (𝐶𝑅𝐷))
38	32, 37	sylan2b 594	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝐹‘𝑥)𝑅(𝐺‘𝑥)) = (𝐶𝑅𝐷))
39	38	mpteq2dva 5247	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) = (𝑥 ∈ 𝑆 ↦ (𝐶𝑅𝐷)))
40	29, 14, 39	3eqtrd 2776	1 ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝑆 ↦ (𝐶𝑅𝐷)))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  Vcvv 3474   ∩ cin 3946   ↦ cmpt 5230  dom cdm 5675   Fn wfn 6535  ‘cfv 6540  (class class class)co 7405   ∘_f cof 7664

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7666

This theorem is referenced by:  ofval  7677  offn  7679  offval2f  7681  off  7684  ofres  7685  offval2  7686  ofco  7689  offveqb  7691  suppssof1  8180  o1rlimmul  15559  frlmipval  21325  frlmphllem  21326  frlmphl  21327  gsumbagdiaglemOLD  21482  gsumbagdiaglem  21485  evlslem1  21636  mhpmulcl  21683  psrplusgpropd  21749  mat1dimscm  21968  rrxcph  24900  rrxds  24901  mbfadd  25169  mbfsub  25170  mbfmullem2  25233  mbfmul  25235  bddmulibl  25347  dvcmulf  25453  ofrn2  31852  off2  31853  ofresid  31854  islinds5  32468  ellspds  32469  evls1fpws  32634  ply1gsumz  32657  ofcof  33093  plymul02  33545  signsplypnf  33549  signsply0  33550  matunitlindflem1  36472  matunitlindflem2  36473  poimirlem3  36479  poimirlem4  36480  poimirlem16  36492  poimirlem19  36495  poimirlem28  36504  broucube  36510  itg2addnc  36530  ftc1anclem8  36556  evlsvvval  41132  dflinc2  47044  fdivmpt  47179