xpima

Description: Direct image by a Cartesian product. (Contributed by Thierry Arnoux, 4-Feb-2017)

		Ref	Expression
	Assertion	xpima	$⊢ (A \times B) [C] = if (A \cap C = \emptyset, \emptyset, B)$

Proof

Step	Hyp	Ref	Expression
1		exmid	$⊢ (A \cap C = \emptyset \lor \neg A \cap C = \emptyset)$
2		df-ima	$⊢ (A \times B) [C] = ran ({(A \times B) ↾}_{C})$
3		df-res	$⊢ {(A \times B) ↾}_{C} = (A \times B) \cap (C \times V)$
4	3	rneqi	$⊢ ran ({(A \times B) ↾}_{C}) = ran ((A \times B) \cap (C \times V))$
5	2 4	eqtri	$⊢ (A \times B) [C] = ran ((A \times B) \cap (C \times V))$
6		inxp	$⊢ (A \times B) \cap (C \times V) = (A \cap C) \times (B \cap V)$
7	6	rneqi	$⊢ ran ((A \times B) \cap (C \times V)) = ran ((A \cap C) \times (B \cap V))$
8		inv1	$⊢ B \cap V = B$
9	8	xpeq2i	$⊢ (A \cap C) \times (B \cap V) = (A \cap C) \times B$
10	9	rneqi	$⊢ ran ((A \cap C) \times (B \cap V)) = ran ((A \cap C) \times B)$
11	5 7 10	3eqtri	$⊢ (A \times B) [C] = ran ((A \cap C) \times B)$
12		xpeq1	$⊢ A \cap C = \emptyset \to (A \cap C) \times B = \emptyset \times B$
13		0xp	$⊢ \emptyset \times B = \emptyset$
14	12 13	syl6eq	$⊢ A \cap C = \emptyset \to (A \cap C) \times B = \emptyset$
15	14	rneqd	$⊢ A \cap C = \emptyset \to ran ((A \cap C) \times B) = ran \emptyset$
16		rn0	$⊢ ran \emptyset = \emptyset$
17	15 16	syl6eq	$⊢ A \cap C = \emptyset \to ran ((A \cap C) \times B) = \emptyset$
18	11 17	syl5eq	$⊢ A \cap C = \emptyset \to (A \times B) [C] = \emptyset$
19	18	ancli	$⊢ A \cap C = \emptyset \to (A \cap C = \emptyset \land (A \times B) [C] = \emptyset)$
20		df-ne	$⊢ A \cap C \neq \emptyset \leftrightarrow \neg A \cap C = \emptyset$
21		rnxp	$⊢ A \cap C \neq \emptyset \to ran ((A \cap C) \times B) = B$
22	20 21	sylbir	$⊢ \neg A \cap C = \emptyset \to ran ((A \cap C) \times B) = B$
23	11 22	syl5eq	$⊢ \neg A \cap C = \emptyset \to (A \times B) [C] = B$
24	23	ancli	$⊢ \neg A \cap C = \emptyset \to (\neg A \cap C = \emptyset \land (A \times B) [C] = B)$
25	19 24	orim12i	$⊢ (A \cap C = \emptyset \lor \neg A \cap C = \emptyset) \to ((A \cap C = \emptyset \land (A \times B) [C] = \emptyset) \lor (\neg A \cap C = \emptyset \land (A \times B) [C] = B))$
26	1 25	ax-mp	$⊢ ((A \cap C = \emptyset \land (A \times B) [C] = \emptyset) \lor (\neg A \cap C = \emptyset \land (A \times B) [C] = B))$
27		eqif	$⊢ (A \times B) [C] = if (A \cap C = \emptyset, \emptyset, B) \leftrightarrow ((A \cap C = \emptyset \land (A \times B) [C] = \emptyset) \lor (\neg A \cap C = \emptyset \land (A \times B) [C] = B))$
28	26 27	mpbir	$⊢ (A \times B) [C] = if (A \cap C = \emptyset, \emptyset, B)$

Metamath Proof Explorer

Theorem xpima

Proof