resundi

Description: Distributive law for restriction over union. Theorem 31 of Suppes p. 65. (Contributed by NM, 30-Sep-2002)

		Ref	Expression
	Assertion	resundi	$⊢ {A ↾}_{(B \cup C)} = ({A ↾}_{B}) \cup ({A ↾}_{C})$

Step	Hyp	Ref	Expression
1		xpundir	$⊢ (B \cup C) \times V = (B \times V) \cup (C \times V)$
2	1	ineq2i	$⊢ A \cap ((B \cup C) \times V) = A \cap ((B \times V) \cup (C \times V))$
3		indi	$⊢ A \cap ((B \times V) \cup (C \times V)) = (A \cap (B \times V)) \cup (A \cap (C \times V))$
4	2 3	eqtri	$⊢ A \cap ((B \cup C) \times V) = (A \cap (B \times V)) \cup (A \cap (C \times V))$
5		df-res	$⊢ {A ↾}_{(B \cup C)} = A \cap ((B \cup C) \times V)$
6		df-res	$⊢ {A ↾}_{B} = A \cap (B \times V)$
7		df-res	$⊢ {A ↾}_{C} = A \cap (C \times V)$
8	6 7	uneq12i	$⊢ ({A ↾}_{B}) \cup ({A ↾}_{C}) = (A \cap (B \times V)) \cup (A \cap (C \times V))$
9	4 5 8	3eqtr4i	$⊢ {A ↾}_{(B \cup C)} = ({A ↾}_{B}) \cup ({A ↾}_{C})$

Metamath Proof Explorer