txrest

Description: The subspace of a topological product space induced by a subset with a Cartesian product representation is a topological product of the subspaces induced by the subspaces of the terms of the products. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 2-Sep-2015)

		Ref	Expression
	Assertion	txrest	$⊢ ((R \in V \land S \in W) \land (A \in X \land B \in Y)) \to (R \times_{t} S) ↾_{𝑡} (A \times B) = (R ↾_{𝑡} A) \times_{t} (S ↾_{𝑡} B)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ran (r \in R, s \in S ⟼ r \times s) = ran (r \in R, s \in S ⟼ r \times s)$
2	1	txval	$⊢ (R \in V \land S \in W) \to R \times_{t} S = topGen (ran (r \in R, s \in S ⟼ r \times s))$
3	2	adantr	$⊢ ((R \in V \land S \in W) \land (A \in X \land B \in Y)) \to R \times_{t} S = topGen (ran (r \in R, s \in S ⟼ r \times s))$
4	3	oveq1d	$⊢ ((R \in V \land S \in W) \land (A \in X \land B \in Y)) \to (R \times_{t} S) ↾_{𝑡} (A \times B) = topGen (ran (r \in R, s \in S ⟼ r \times s)) ↾_{𝑡} (A \times B)$
5	1	txbasex	$⊢ (R \in V \land S \in W) \to ran (r \in R, s \in S ⟼ r \times s) \in V$
6		xpexg	$⊢ (A \in X \land B \in Y) \to A \times B \in V$
7		tgrest	$⊢ (ran (r \in R, s \in S ⟼ r \times s) \in V \land A \times B \in V) \to topGen (ran (r \in R, s \in S ⟼ r \times s) ↾_{𝑡} (A \times B)) = topGen (ran (r \in R, s \in S ⟼ r \times s)) ↾_{𝑡} (A \times B)$
8	5 6 7	syl2an	$⊢ ((R \in V \land S \in W) \land (A \in X \land B \in Y)) \to topGen (ran (r \in R, s \in S ⟼ r \times s) ↾_{𝑡} (A \times B)) = topGen (ran (r \in R, s \in S ⟼ r \times s)) ↾_{𝑡} (A \times B)$
9		elrest	$⊢ (ran (r \in R, s \in S ⟼ r \times s) \in V \land A \times B \in V) \to (x \in (ran (r \in R, s \in S ⟼ r \times s) ↾_{𝑡} (A \times B)) \leftrightarrow \exists w \in ran (r \in R, s \in S ⟼ r \times s) x = w \cap (A \times B))$
10	5 6 9	syl2an	$⊢ ((R \in V \land S \in W) \land (A \in X \land B \in Y)) \to (x \in (ran (r \in R, s \in S ⟼ r \times s) ↾_{𝑡} (A \times B)) \leftrightarrow \exists w \in ran (r \in R, s \in S ⟼ r \times s) x = w \cap (A \times B))$
11		vex	$⊢ r \in V$
12	11	inex1	$⊢ r \cap A \in V$
13	12	a1i	$⊢ (((R \in V \land S \in W) \land (A \in X \land B \in Y)) \land r \in R) \to r \cap A \in V$
14		elrest	$⊢ (R \in V \land A \in X) \to (u \in (R ↾_{𝑡} A) \leftrightarrow \exists r \in R u = r \cap A)$
15	14	ad2ant2r	$⊢ ((R \in V \land S \in W) \land (A \in X \land B \in Y)) \to (u \in (R ↾_{𝑡} A) \leftrightarrow \exists r \in R u = r \cap A)$
16		xpeq1	$⊢ u = r \cap A \to u \times v = (r \cap A) \times v$
17	16	eqeq2d	$⊢ u = r \cap A \to (x = u \times v \leftrightarrow x = (r \cap A) \times v)$
18	17	rexbidv	$⊢ u = r \cap A \to (\exists v \in (S ↾_{𝑡} B) x = u \times v \leftrightarrow \exists v \in (S ↾_{𝑡} B) x = (r \cap A) \times v)$
19		vex	$⊢ s \in V$
20	19	inex1	$⊢ s \cap B \in V$
21	20	a1i	$⊢ (((R \in V \land S \in W) \land (A \in X \land B \in Y)) \land s \in S) \to s \cap B \in V$
22		elrest	$⊢ (S \in W \land B \in Y) \to (v \in (S ↾_{𝑡} B) \leftrightarrow \exists s \in S v = s \cap B)$
23	22	ad2ant2l	$⊢ ((R \in V \land S \in W) \land (A \in X \land B \in Y)) \to (v \in (S ↾_{𝑡} B) \leftrightarrow \exists s \in S v = s \cap B)$
24		xpeq2	$⊢ v = s \cap B \to (r \cap A) \times v = (r \cap A) \times (s \cap B)$
25	24	eqeq2d	$⊢ v = s \cap B \to (x = (r \cap A) \times v \leftrightarrow x = (r \cap A) \times (s \cap B))$
26	25	adantl	$⊢ (((R \in V \land S \in W) \land (A \in X \land B \in Y)) \land v = s \cap B) \to (x = (r \cap A) \times v \leftrightarrow x = (r \cap A) \times (s \cap B))$
27	21 23 26	rexxfr2d	$⊢ ((R \in V \land S \in W) \land (A \in X \land B \in Y)) \to (\exists v \in (S ↾_{𝑡} B) x = (r \cap A) \times v \leftrightarrow \exists s \in S x = (r \cap A) \times (s \cap B))$
28	18 27	sylan9bbr	$⊢ (((R \in V \land S \in W) \land (A \in X \land B \in Y)) \land u = r \cap A) \to (\exists v \in (S ↾_{𝑡} B) x = u \times v \leftrightarrow \exists s \in S x = (r \cap A) \times (s \cap B))$
29	13 15 28	rexxfr2d	$⊢ ((R \in V \land S \in W) \land (A \in X \land B \in Y)) \to (\exists u \in (R ↾_{𝑡} A) \exists v \in (S ↾_{𝑡} B) x = u \times v \leftrightarrow \exists r \in R \exists s \in S x = (r \cap A) \times (s \cap B))$
30	11 19	xpex	$⊢ r \times s \in V$
31	30	rgen2w	$⊢ \forall r \in R \forall s \in S r \times s \in V$
32		eqid	$⊢ (r \in R, s \in S ⟼ r \times s) = (r \in R, s \in S ⟼ r \times s)$
33		ineq1	$⊢ w = r \times s \to w \cap (A \times B) = (r \times s) \cap (A \times B)$
34		inxp	$⊢ (r \times s) \cap (A \times B) = (r \cap A) \times (s \cap B)$
35	33 34	syl6eq	$⊢ w = r \times s \to w \cap (A \times B) = (r \cap A) \times (s \cap B)$
36	35	eqeq2d	$⊢ w = r \times s \to (x = w \cap (A \times B) \leftrightarrow x = (r \cap A) \times (s \cap B))$
37	32 36	rexrnmpo	$⊢ \forall r \in R \forall s \in S r \times s \in V \to (\exists w \in ran (r \in R, s \in S ⟼ r \times s) x = w \cap (A \times B) \leftrightarrow \exists r \in R \exists s \in S x = (r \cap A) \times (s \cap B))$
38	31 37	ax-mp	$⊢ \exists w \in ran (r \in R, s \in S ⟼ r \times s) x = w \cap (A \times B) \leftrightarrow \exists r \in R \exists s \in S x = (r \cap A) \times (s \cap B)$
39	29 38	syl6bbr	$⊢ ((R \in V \land S \in W) \land (A \in X \land B \in Y)) \to (\exists u \in (R ↾_{𝑡} A) \exists v \in (S ↾_{𝑡} B) x = u \times v \leftrightarrow \exists w \in ran (r \in R, s \in S ⟼ r \times s) x = w \cap (A \times B))$
40	10 39	bitr4d	$⊢ ((R \in V \land S \in W) \land (A \in X \land B \in Y)) \to (x \in (ran (r \in R, s \in S ⟼ r \times s) ↾_{𝑡} (A \times B)) \leftrightarrow \exists u \in (R ↾_{𝑡} A) \exists v \in (S ↾_{𝑡} B) x = u \times v)$
41	40	abbi2dv	$⊢ ((R \in V \land S \in W) \land (A \in X \land B \in Y)) \to ran (r \in R, s \in S ⟼ r \times s) ↾_{𝑡} (A \times B) = \{x \| \exists u \in (R ↾_{𝑡} A) \exists v \in (S ↾_{𝑡} B) x = u \times v\}$
42		eqid	$⊢ (u \in (R ↾_{𝑡} A), v \in (S ↾_{𝑡} B) ⟼ u \times v) = (u \in (R ↾_{𝑡} A), v \in (S ↾_{𝑡} B) ⟼ u \times v)$
43	42	rnmpo	$⊢ ran (u \in (R ↾_{𝑡} A), v \in (S ↾_{𝑡} B) ⟼ u \times v) = \{x \| \exists u \in (R ↾_{𝑡} A) \exists v \in (S ↾_{𝑡} B) x = u \times v\}$
44	41 43	syl6eqr	$⊢ ((R \in V \land S \in W) \land (A \in X \land B \in Y)) \to ran (r \in R, s \in S ⟼ r \times s) ↾_{𝑡} (A \times B) = ran (u \in (R ↾_{𝑡} A), v \in (S ↾_{𝑡} B) ⟼ u \times v)$
45	44	fveq2d	$⊢ ((R \in V \land S \in W) \land (A \in X \land B \in Y)) \to topGen (ran (r \in R, s \in S ⟼ r \times s) ↾_{𝑡} (A \times B)) = topGen (ran (u \in (R ↾_{𝑡} A), v \in (S ↾_{𝑡} B) ⟼ u \times v))$
46	4 8 45	3eqtr2d	$⊢ ((R \in V \land S \in W) \land (A \in X \land B \in Y)) \to (R \times_{t} S) ↾_{𝑡} (A \times B) = topGen (ran (u \in (R ↾_{𝑡} A), v \in (S ↾_{𝑡} B) ⟼ u \times v))$
47		ovex	$⊢ R ↾_{𝑡} A \in V$
48		ovex	$⊢ S ↾_{𝑡} B \in V$
49		eqid	$⊢ ran (u \in (R ↾_{𝑡} A), v \in (S ↾_{𝑡} B) ⟼ u \times v) = ran (u \in (R ↾_{𝑡} A), v \in (S ↾_{𝑡} B) ⟼ u \times v)$
50	49	txval	$⊢ (R ↾_{𝑡} A \in V \land S ↾_{𝑡} B \in V) \to (R ↾_{𝑡} A) \times_{t} (S ↾_{𝑡} B) = topGen (ran (u \in (R ↾_{𝑡} A), v \in (S ↾_{𝑡} B) ⟼ u \times v))$
51	47 48 50	mp2an	$⊢ (R ↾_{𝑡} A) \times_{t} (S ↾_{𝑡} B) = topGen (ran (u \in (R ↾_{𝑡} A), v \in (S ↾_{𝑡} B) ⟼ u \times v))$
52	46 51	syl6eqr	$⊢ ((R \in V \land S \in W) \land (A \in X \land B \in Y)) \to (R \times_{t} S) ↾_{𝑡} (A \times B) = (R ↾_{𝑡} A) \times_{t} (S ↾_{𝑡} B)$

Metamath Proof Explorer

Theorem txrest

Proof