This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) )