![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > restabs | Structured version Visualization version GIF version |
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 |
---|---|
restabs | ⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑇 ∧ 𝑇 ∈ 𝑊) → ((𝐽 ↾t 𝑇) ↾t 𝑆) = (𝐽 ↾t 𝑆)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 1116 | . . 3 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑇 ∧ 𝑇 ∈ 𝑊) → 𝐽 ∈ 𝑉) | |
2 | simp3 1118 | . . 3 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑇 ∧ 𝑇 ∈ 𝑊) → 𝑇 ∈ 𝑊) | |
3 | ssexg 5077 | . . . 4 ⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ∈ 𝑊) → 𝑆 ∈ V) | |
4 | 3 | 3adant1 1110 | . . 3 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑇 ∧ 𝑇 ∈ 𝑊) → 𝑆 ∈ V) |
5 | restco 21466 | . . 3 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊 ∧ 𝑆 ∈ V) → ((𝐽 ↾t 𝑇) ↾t 𝑆) = (𝐽 ↾t (𝑇 ∩ 𝑆))) | |
6 | 1, 2, 4, 5 | syl3anc 1351 | . 2 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑇 ∧ 𝑇 ∈ 𝑊) → ((𝐽 ↾t 𝑇) ↾t 𝑆) = (𝐽 ↾t (𝑇 ∩ 𝑆))) |
7 | simp2 1117 | . . . 4 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑇 ∧ 𝑇 ∈ 𝑊) → 𝑆 ⊆ 𝑇) | |
8 | sseqin2 4074 | . . . 4 ⊢ (𝑆 ⊆ 𝑇 ↔ (𝑇 ∩ 𝑆) = 𝑆) | |
9 | 7, 8 | sylib 210 | . . 3 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑇 ∧ 𝑇 ∈ 𝑊) → (𝑇 ∩ 𝑆) = 𝑆) |
10 | 9 | oveq2d 6986 | . 2 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑇 ∧ 𝑇 ∈ 𝑊) → (𝐽 ↾t (𝑇 ∩ 𝑆)) = (𝐽 ↾t 𝑆)) |
11 | 6, 10 | eqtrd 2808 | 1 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑇 ∧ 𝑇 ∈ 𝑊) → ((𝐽 ↾t 𝑇) ↾t 𝑆) = (𝐽 ↾t 𝑆)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1068 = wceq 1507 ∈ wcel 2048 Vcvv 3409 ∩ cin 3824 ⊆ wss 3825 (class class class)co 6970 ↾t crest 16540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2745 ax-rep 5043 ax-sep 5054 ax-nul 5061 ax-pr 5180 ax-un 7273 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-ral 3087 df-rex 3088 df-reu 3089 df-rab 3091 df-v 3411 df-sbc 3678 df-csb 3783 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-nul 4174 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4707 df-iun 4788 df-br 4924 df-opab 4986 df-mpt 5003 df-id 5305 df-xp 5406 df-rel 5407 df-cnv 5408 df-co 5409 df-dm 5410 df-rn 5411 df-res 5412 df-ima 5413 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-ov 6973 df-oprab 6974 df-mpo 6975 df-rest 16542 |
This theorem is referenced by: restcnrm 21664 fiuncmp 21706 subislly 21783 restnlly 21784 islly2 21786 llyrest 21787 nllyrest 21788 llyidm 21790 nllyidm 21791 cldllycmp 21797 txkgen 21954 rerest 23105 xrrest 23108 cnmpopc 23225 cnheiborlem 23251 pcoass 23321 limcres 24177 perfdvf 24194 dvreslem 24200 dvres2lem 24201 dvaddbr 24228 dvmulbr 24229 dvcnvrelem2 24308 psercn 24707 abelth 24722 cxpcn2 25018 cxpcn3 25020 lmlimxrge0 30792 pnfneige0 30795 cvmsss2 32066 cvmliftlem8 32084 cvmliftlem10 32086 cvmlift2lem9 32103 ivthALT 33144 limcresiooub 41300 limcresioolb 41301 cncfuni 41545 cncfiooicclem1 41552 itgsubsticclem 41636 dirkercncflem4 41768 fourierdlem32 41801 fourierdlem33 41802 fourierdlem62 41830 fouriersw 41893 smfco 42454 |
Copyright terms: Public domain | W3C validator |