Metamath Proof Explorer

Theorem restabs

Description: Equivalence of being a subspace of a subspace and being a subspace of the original. (Contributed by Jeff Hankins, 11-Jul-2009) (Proof shortened by Mario Carneiro, 1-May-2015)

		Ref	Expression
	Assertion	restabs	$⊢ (J \in V \land S \subseteq T \land T \in W) \to (J ↾_{𝑡} T) ↾_{𝑡} S = J ↾_{𝑡} S$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (J \in V \land S \subseteq T \land T \in W) \to J \in V$
2		simp3	$⊢ (J \in V \land S \subseteq T \land T \in W) \to T \in W$
3		ssexg	$⊢ (S \subseteq T \land T \in W) \to S \in V$
4	3	3adant1	$⊢ (J \in V \land S \subseteq T \land T \in W) \to S \in V$
5		restco	$⊢ (J \in V \land T \in W \land S \in V) \to (J ↾_{𝑡} T) ↾_{𝑡} S = J ↾_{𝑡} (T \cap S)$
6	1 2 4 5	syl3anc	$⊢ (J \in V \land S \subseteq T \land T \in W) \to (J ↾_{𝑡} T) ↾_{𝑡} S = J ↾_{𝑡} (T \cap S)$
7		simp2	$⊢ (J \in V \land S \subseteq T \land T \in W) \to S \subseteq T$
8		sseqin2	$⊢ S \subseteq T \leftrightarrow T \cap S = S$
9	7 8	sylib	$⊢ (J \in V \land S \subseteq T \land T \in W) \to T \cap S = S$
10	9	oveq2d	$⊢ (J \in V \land S \subseteq T \land T \in W) \to J ↾_{𝑡} (T \cap S) = J ↾_{𝑡} S$
11	6 10	eqtrd	$⊢ (J \in V \land S \subseteq T \land T \in W) \to (J ↾_{𝑡} T) ↾_{𝑡} S = J ↾_{𝑡} S$