ofresid

Description: Applying an operation restricted to the range of the functions does not change the function operation. (Contributed by Thierry Arnoux, 14-Feb-2018)

	Ref	Expression
Hypotheses	ofresid.1	$⊢ φ \to F : A ⟶ B$
	ofresid.2	$⊢ φ \to G : A ⟶ B$
	ofresid.3	$⊢ φ \to A \in V$
Assertion	ofresid	$⊢ φ \to F R_{f} G = F {({R ↾}_{(B \times B)})}_{f} G$

Proof

Step	Hyp	Ref	Expression
1		ofresid.1	$⊢ φ \to F : A ⟶ B$
2		ofresid.2	$⊢ φ \to G : A ⟶ B$
3		ofresid.3	$⊢ φ \to A \in V$
4	1	ffvelrnda	$⊢ (φ \land x \in A) \to F (x) \in B$
5	2	ffvelrnda	$⊢ (φ \land x \in A) \to G (x) \in B$
6	4 5	opelxpd	$⊢ (φ \land x \in A) \to ⟨F (x), G (x)⟩ \in (B \times B)$
7	6	fvresd	$⊢ (φ \land x \in A) \to ({R ↾}_{(B \times B)}) (⟨F (x), G (x)⟩) = R (⟨F (x), G (x)⟩)$
8	7	eqcomd	$⊢ (φ \land x \in A) \to R (⟨F (x), G (x)⟩) = ({R ↾}_{(B \times B)}) (⟨F (x), G (x)⟩)$
9		df-ov	$⊢ F (x) R G (x) = R (⟨F (x), G (x)⟩)$
10		df-ov	$⊢ F (x) ({R ↾}_{(B \times B)}) G (x) = ({R ↾}_{(B \times B)}) (⟨F (x), G (x)⟩)$
11	8 9 10	3eqtr4g	$⊢ (φ \land x \in A) \to F (x) R G (x) = F (x) ({R ↾}_{(B \times B)}) G (x)$
12	11	mpteq2dva	$⊢ φ \to (x \in A ⟼ F (x) R G (x)) = (x \in A ⟼ F (x) ({R ↾}_{(B \times B)}) G (x))$
13	1	ffnd	$⊢ φ \to F Fn A$
14	2	ffnd	$⊢ φ \to G Fn A$
15		inidm	$⊢ A \cap A = A$
16		eqidd	$⊢ (φ \land x \in A) \to F (x) = F (x)$
17		eqidd	$⊢ (φ \land x \in A) \to G (x) = G (x)$
18	13 14 3 3 15 16 17	offval	$⊢ φ \to F R_{f} G = (x \in A ⟼ F (x) R G (x))$
19	13 14 3 3 15 16 17	offval	$⊢ φ \to F {({R ↾}_{(B \times B)})}_{f} G = (x \in A ⟼ F (x) ({R ↾}_{(B \times B)}) G (x))$
20	12 18 19	3eqtr4d	$⊢ φ \to F R_{f} G = F {({R ↾}_{(B \times B)})}_{f} G$

Metamath Proof Explorer

Theorem ofresid

Proof