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 e. V /\ S C_ T /\ T e. W ) -> ( ( J |`t T ) |`t S ) = ( J |`t S ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	|- ( ( J e. V /\ S C_ T /\ T e. W ) -> J e. V )
2		simp3	|- ( ( J e. V /\ S C_ T /\ T e. W ) -> T e. W )
3		ssexg	|- ( ( S C_ T /\ T e. W ) -> S e. _V )
4	3	3adant1	|- ( ( J e. V /\ S C_ T /\ T e. W ) -> S e. _V )
5		restco	|- ( ( J e. V /\ T e. W /\ S e. _V ) -> ( ( J |`t T ) |`t S ) = ( J |`t ( T i^i S ) ) )
6	1 2 4 5	syl3anc	|- ( ( J e. V /\ S C_ T /\ T e. W ) -> ( ( J |`t T ) |`t S ) = ( J |`t ( T i^i S ) ) )
7		simp2	|- ( ( J e. V /\ S C_ T /\ T e. W ) -> S C_ T )
8		sseqin2	|- ( S C_ T <-> ( T i^i S ) = S )
9	7 8	sylib	|- ( ( J e. V /\ S C_ T /\ T e. W ) -> ( T i^i S ) = S )
10	9	oveq2d	|- ( ( J e. V /\ S C_ T /\ T e. W ) -> ( J |`t ( T i^i S ) ) = ( J |`t S ) )
11	6 10	eqtrd	|- ( ( J e. V /\ S C_ T /\ T e. W ) -> ( ( J |`t T ) |`t S ) = ( J |`t S ) )