restco

Description: Composition of subspaces. (Contributed by Mario Carneiro, 15-Dec-2013) (Revised by Mario Carneiro, 1-May-2015)

		Ref	Expression
	Assertion	restco	$⊢ (J \in V \land A \in W \land B \in X) \to (J ↾_{𝑡} A) ↾_{𝑡} B = J ↾_{𝑡} (A \cap B)$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ y \in V$
2	1	inex1	$⊢ y \cap A \in V$
3		ineq1	$⊢ x = y \cap A \to x \cap B = (y \cap A) \cap B$
4		inass	$⊢ (y \cap A) \cap B = y \cap (A \cap B)$
5	3 4	eqtrdi	$⊢ x = y \cap A \to x \cap B = y \cap (A \cap B)$
6	2 5	abrexco	$⊢ \{z \| \exists x \in \{w \| \exists y \in J w = y \cap A\} z = x \cap B\} = \{z \| \exists y \in J z = y \cap (A \cap B)\}$
7		eqid	$⊢ (y \in J ⟼ y \cap A) = (y \in J ⟼ y \cap A)$
8	7	rnmpt	$⊢ ran (y \in J ⟼ y \cap A) = \{w \| \exists y \in J w = y \cap A\}$
9	8	mpteq1i	$⊢ (x \in ran (y \in J ⟼ y \cap A) ⟼ x \cap B) = (x \in \{w \| \exists y \in J w = y \cap A\} ⟼ x \cap B)$
10	9	rnmpt	$⊢ ran (x \in ran (y \in J ⟼ y \cap A) ⟼ x \cap B) = \{z \| \exists x \in \{w \| \exists y \in J w = y \cap A\} z = x \cap B\}$
11		eqid	$⊢ (y \in J ⟼ y \cap (A \cap B)) = (y \in J ⟼ y \cap (A \cap B))$
12	11	rnmpt	$⊢ ran (y \in J ⟼ y \cap (A \cap B)) = \{z \| \exists y \in J z = y \cap (A \cap B)\}$
13	6 10 12	3eqtr4i	$⊢ ran (x \in ran (y \in J ⟼ y \cap A) ⟼ x \cap B) = ran (y \in J ⟼ y \cap (A \cap B))$
14		restval	$⊢ (J \in V \land A \in W) \to J ↾_{𝑡} A = ran (y \in J ⟼ y \cap A)$
15	14	3adant3	$⊢ (J \in V \land A \in W \land B \in X) \to J ↾_{𝑡} A = ran (y \in J ⟼ y \cap A)$
16	15	oveq1d	$⊢ (J \in V \land A \in W \land B \in X) \to (J ↾_{𝑡} A) ↾_{𝑡} B = ran (y \in J ⟼ y \cap A) ↾_{𝑡} B$
17		ovex	$⊢ J ↾_{𝑡} A \in V$
18	15 17	eqeltrrdi	$⊢ (J \in V \land A \in W \land B \in X) \to ran (y \in J ⟼ y \cap A) \in V$
19		simp3	$⊢ (J \in V \land A \in W \land B \in X) \to B \in X$
20		restval	$⊢ (ran (y \in J ⟼ y \cap A) \in V \land B \in X) \to ran (y \in J ⟼ y \cap A) ↾_{𝑡} B = ran (x \in ran (y \in J ⟼ y \cap A) ⟼ x \cap B)$
21	18 19 20	syl2anc	$⊢ (J \in V \land A \in W \land B \in X) \to ran (y \in J ⟼ y \cap A) ↾_{𝑡} B = ran (x \in ran (y \in J ⟼ y \cap A) ⟼ x \cap B)$
22	16 21	eqtrd	$⊢ (J \in V \land A \in W \land B \in X) \to (J ↾_{𝑡} A) ↾_{𝑡} B = ran (x \in ran (y \in J ⟼ y \cap A) ⟼ x \cap B)$
23		simp1	$⊢ (J \in V \land A \in W \land B \in X) \to J \in V$
24		inex1g	$⊢ A \in W \to A \cap B \in V$
25	24	3ad2ant2	$⊢ (J \in V \land A \in W \land B \in X) \to A \cap B \in V$
26		restval	$⊢ (J \in V \land A \cap B \in V) \to J ↾_{𝑡} (A \cap B) = ran (y \in J ⟼ y \cap (A \cap B))$
27	23 25 26	syl2anc	$⊢ (J \in V \land A \in W \land B \in X) \to J ↾_{𝑡} (A \cap B) = ran (y \in J ⟼ y \cap (A \cap B))$
28	13 22 27	3eqtr4a	$⊢ (J \in V \land A \in W \land B \in X) \to (J ↾_{𝑡} A) ↾_{𝑡} B = J ↾_{𝑡} (A \cap B)$

Metamath Proof Explorer

Theorem restco

Proof