offres

Description: Pointwise combination commutes with restriction. (Contributed by Stefan O'Rear, 24-Jan-2015)

		Ref	Expression
	Assertion	offres	$⊢ (F \in V \land G \in W) \to {(F R_{f} G) ↾}_{D} = ({F ↾}_{D}) R_{f} ({G ↾}_{D})$

Proof

Step	Hyp	Ref	Expression
1		elinel2	$⊢ x \in ((dom F \cap dom G) \cap D) \to x \in D$
2		fvres	$⊢ x \in D \to ({F ↾}_{D}) (x) = F (x)$
3		fvres	$⊢ x \in D \to ({G ↾}_{D}) (x) = G (x)$
4	2 3	oveq12d	$⊢ x \in D \to ({F ↾}_{D}) (x) R ({G ↾}_{D}) (x) = F (x) R G (x)$
5	1 4	syl	$⊢ x \in ((dom F \cap dom G) \cap D) \to ({F ↾}_{D}) (x) R ({G ↾}_{D}) (x) = F (x) R G (x)$
6	5	mpteq2ia	$⊢ (x \in ((dom F \cap dom G) \cap D) ⟼ ({F ↾}_{D}) (x) R ({G ↾}_{D}) (x)) = (x \in ((dom F \cap dom G) \cap D) ⟼ F (x) R G (x))$
7		inindi	$⊢ D \cap (dom F \cap dom G) = (D \cap dom F) \cap (D \cap dom G)$
8		incom	$⊢ (dom F \cap dom G) \cap D = D \cap (dom F \cap dom G)$
9		dmres	$⊢ dom ({F ↾}_{D}) = D \cap dom F$
10		dmres	$⊢ dom ({G ↾}_{D}) = D \cap dom G$
11	9 10	ineq12i	$⊢ dom ({F ↾}_{D}) \cap dom ({G ↾}_{D}) = (D \cap dom F) \cap (D \cap dom G)$
12	7 8 11	3eqtr4ri	$⊢ dom ({F ↾}_{D}) \cap dom ({G ↾}_{D}) = (dom F \cap dom G) \cap D$
13	12	mpteq1i	$⊢ (x \in (dom ({F ↾}_{D}) \cap dom ({G ↾}_{D})) ⟼ ({F ↾}_{D}) (x) R ({G ↾}_{D}) (x)) = (x \in ((dom F \cap dom G) \cap D) ⟼ ({F ↾}_{D}) (x) R ({G ↾}_{D}) (x))$
14		resmpt3	$⊢ {(x \in (dom F \cap dom G) ⟼ F (x) R G (x)) ↾}_{D} = (x \in ((dom F \cap dom G) \cap D) ⟼ F (x) R G (x))$
15	6 13 14	3eqtr4ri	$⊢ {(x \in (dom F \cap dom G) ⟼ F (x) R G (x)) ↾}_{D} = (x \in (dom ({F ↾}_{D}) \cap dom ({G ↾}_{D})) ⟼ ({F ↾}_{D}) (x) R ({G ↾}_{D}) (x))$
16		offval3	$⊢ (F \in V \land G \in W) \to F R_{f} G = (x \in (dom F \cap dom G) ⟼ F (x) R G (x))$
17	16	reseq1d	$⊢ (F \in V \land G \in W) \to {(F R_{f} G) ↾}_{D} = {(x \in (dom F \cap dom G) ⟼ F (x) R G (x)) ↾}_{D}$
18		resexg	$⊢ F \in V \to {F ↾}_{D} \in V$
19		resexg	$⊢ G \in W \to {G ↾}_{D} \in V$
20		offval3	$⊢ ({F ↾}_{D} \in V \land {G ↾}_{D} \in V) \to ({F ↾}_{D}) R_{f} ({G ↾}_{D}) = (x \in (dom ({F ↾}_{D}) \cap dom ({G ↾}_{D})) ⟼ ({F ↾}_{D}) (x) R ({G ↾}_{D}) (x))$
21	18 19 20	syl2an	$⊢ (F \in V \land G \in W) \to ({F ↾}_{D}) R_{f} ({G ↾}_{D}) = (x \in (dom ({F ↾}_{D}) \cap dom ({G ↾}_{D})) ⟼ ({F ↾}_{D}) (x) R ({G ↾}_{D}) (x))$
22	15 17 21	3eqtr4a	$⊢ (F \in V \land G \in W) \to {(F R_{f} G) ↾}_{D} = ({F ↾}_{D}) R_{f} ({G ↾}_{D})$

Metamath Proof Explorer

Theorem offres

Proof