offval

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

	Ref	Expression
Hypotheses	offval.1	$⊢ φ \to F Fn A$
	offval.2	$⊢ φ \to G Fn B$
	offval.3	$⊢ φ \to A \in V$
	offval.4	$⊢ φ \to B \in W$
	offval.5	$⊢ A \cap B = S$
	offval.6	$⊢ (φ \land x \in A) \to F (x) = C$
	offval.7	$⊢ (φ \land x \in B) \to G (x) = D$
Assertion	offval	$⊢ φ \to F R_{f} G = (x \in S ⟼ C R D)$

Proof

Step	Hyp	Ref	Expression
1		offval.1	$⊢ φ \to F Fn A$
2		offval.2	$⊢ φ \to G Fn B$
3		offval.3	$⊢ φ \to A \in V$
4		offval.4	$⊢ φ \to B \in W$
5		offval.5	$⊢ A \cap B = S$
6		offval.6	$⊢ (φ \land x \in A) \to F (x) = C$
7		offval.7	$⊢ (φ \land x \in B) \to G (x) = D$
8		fnex	$⊢ (F Fn A \land A \in V) \to F \in V$
9	1 3 8	syl2anc	$⊢ φ \to F \in V$
10		fnex	$⊢ (G Fn B \land B \in W) \to G \in V$
11	2 4 10	syl2anc	$⊢ φ \to G \in V$
12	1	fndmd	$⊢ φ \to dom F = A$
13	2	fndmd	$⊢ φ \to dom G = B$
14	12 13	ineq12d	$⊢ φ \to dom F \cap dom G = A \cap B$
15	14 5	eqtrdi	$⊢ φ \to dom F \cap dom G = S$
16	15	mpteq1d	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ F (x) R G (x)) = (x \in S ⟼ F (x) R G (x))$
17		inex1g	$⊢ A \in V \to A \cap B \in V$
18	5 17	eqeltrrid	$⊢ A \in V \to S \in V$
19		mptexg	$⊢ S \in V \to (x \in S ⟼ F (x) R G (x)) \in V$
20	3 18 19	3syl	$⊢ φ \to (x \in S ⟼ F (x) R G (x)) \in V$
21	16 20	eqeltrd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ F (x) R G (x)) \in V$
22		dmeq	$⊢ f = F \to dom f = dom F$
23		dmeq	$⊢ g = G \to dom g = dom G$
24	22 23	ineqan12d	$⊢ (f = F \land g = G) \to dom f \cap dom g = dom F \cap dom G$
25		fveq1	$⊢ f = F \to f (x) = F (x)$
26		fveq1	$⊢ g = G \to g (x) = G (x)$
27	25 26	oveqan12d	$⊢ (f = F \land g = G) \to f (x) R g (x) = F (x) R G (x)$
28	24 27	mpteq12dv	$⊢ (f = F \land g = G) \to (x \in (dom f \cap dom g) ⟼ f (x) R g (x)) = (x \in (dom F \cap dom G) ⟼ F (x) R G (x))$
29		df-of	$⊢ \circ_{f} R = (f \in V, g \in V ⟼ (x \in (dom f \cap dom g) ⟼ f (x) R g (x)))$
30	28 29	ovmpoga	$⊢ (F \in V \land G \in V \land (x \in (dom F \cap dom G) ⟼ F (x) R G (x)) \in V) \to F R_{f} G = (x \in (dom F \cap dom G) ⟼ F (x) R G (x))$
31	9 11 21 30	syl3anc	$⊢ φ \to F R_{f} G = (x \in (dom F \cap dom G) ⟼ F (x) R G (x))$
32	5	eleq2i	$⊢ x \in (A \cap B) \leftrightarrow x \in S$
33		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
34	32 33	bitr3i	$⊢ x \in S \leftrightarrow (x \in A \land x \in B)$
35	6	adantrr	$⊢ (φ \land (x \in A \land x \in B)) \to F (x) = C$
36	7	adantrl	$⊢ (φ \land (x \in A \land x \in B)) \to G (x) = D$
37	35 36	oveq12d	$⊢ (φ \land (x \in A \land x \in B)) \to F (x) R G (x) = C R D$
38	34 37	sylan2b	$⊢ (φ \land x \in S) \to F (x) R G (x) = C R D$
39	38	mpteq2dva	$⊢ φ \to (x \in S ⟼ F (x) R G (x)) = (x \in S ⟼ C R D)$
40	31 16 39	3eqtrd	$⊢ φ \to F R_{f} G = (x \in S ⟼ C R D)$

Metamath Proof Explorer

Theorem offval

Proof