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 ∈ V ∧ S ⊆ T ∧ T ∈ W → J ↾ 𝑡 T ↾ 𝑡 S = J ↾ 𝑡 S

Proof

Step Hyp Ref Expression
1 simp1 ⊢ J ∈ V ∧ S ⊆ T ∧ T ∈ W → J ∈ V
2 simp3 ⊢ J ∈ V ∧ S ⊆ T ∧ T ∈ W → T ∈ W
3 ssexg ⊢ S ⊆ T ∧ T ∈ W → S ∈ V
4 3 3adant1 ⊢ J ∈ V ∧ S ⊆ T ∧ T ∈ W → S ∈ V
5 restco ⊢ J ∈ V ∧ T ∈ W ∧ S ∈ V → J ↾ 𝑡 T ↾ 𝑡 S = J ↾ 𝑡 T ∩ S
6 1 2 4 5 syl3anc ⊢ J ∈ V ∧ S ⊆ T ∧ T ∈ W → J ↾ 𝑡 T ↾ 𝑡 S = J ↾ 𝑡 T ∩ S
7 simp2 ⊢ J ∈ V ∧ S ⊆ T ∧ T ∈ W → S ⊆ T
8 sseqin2 ⊢ S ⊆ T ↔ T ∩ S = S
9 7 8 sylib ⊢ J ∈ V ∧ S ⊆ T ∧ T ∈ W → T ∩ S = S
10 9 oveq2d ⊢ J ∈ V ∧ S ⊆ T ∧ T ∈ W → J ↾ 𝑡 T ∩ S = J ↾ 𝑡 S
11 6 10 eqtrd ⊢ J ∈ V ∧ S ⊆ T ∧ T ∈ W → J ↾ 𝑡 T ↾ 𝑡 S = J ↾ 𝑡 S