Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > lsssn0 | Structured version Visualization version GIF version |
Description: The singleton of the zero vector is a subspace. (Contributed by NM, 13-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
Ref | Expression |
---|---|
lss0cl.z | ⊢ 0 = (0g‘𝑊) |
lss0cl.s | ⊢ 𝑆 = (LSubSp‘𝑊) |
Ref | Expression |
---|---|
lsssn0 | ⊢ (𝑊 ∈ LMod → { 0 } ∈ 𝑆) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqidd 2737 | . 2 ⊢ (𝑊 ∈ LMod → (Scalar‘𝑊) = (Scalar‘𝑊)) | |
2 | eqidd 2737 | . 2 ⊢ (𝑊 ∈ LMod → (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))) | |
3 | eqidd 2737 | . 2 ⊢ (𝑊 ∈ LMod → (Base‘𝑊) = (Base‘𝑊)) | |
4 | eqidd 2737 | . 2 ⊢ (𝑊 ∈ LMod → (+g‘𝑊) = (+g‘𝑊)) | |
5 | eqidd 2737 | . 2 ⊢ (𝑊 ∈ LMod → ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)) | |
6 | lss0cl.s | . . 3 ⊢ 𝑆 = (LSubSp‘𝑊) | |
7 | 6 | a1i 11 | . 2 ⊢ (𝑊 ∈ LMod → 𝑆 = (LSubSp‘𝑊)) |
8 | eqid 2736 | . . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊) | |
9 | lss0cl.z | . . . 4 ⊢ 0 = (0g‘𝑊) | |
10 | 8, 9 | lmod0vcl 20232 | . . 3 ⊢ (𝑊 ∈ LMod → 0 ∈ (Base‘𝑊)) |
11 | 10 | snssd 4753 | . 2 ⊢ (𝑊 ∈ LMod → { 0 } ⊆ (Base‘𝑊)) |
12 | 9 | fvexi 6825 | . . . 4 ⊢ 0 ∈ V |
13 | 12 | snnz 4721 | . . 3 ⊢ { 0 } ≠ ∅ |
14 | 13 | a1i 11 | . 2 ⊢ (𝑊 ∈ LMod → { 0 } ≠ ∅) |
15 | simpr2 1194 | . . . . . . . 8 ⊢ ((𝑊 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 })) → 𝑎 ∈ { 0 }) | |
16 | elsni 4587 | . . . . . . . 8 ⊢ (𝑎 ∈ { 0 } → 𝑎 = 0 ) | |
17 | 15, 16 | syl 17 | . . . . . . 7 ⊢ ((𝑊 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 })) → 𝑎 = 0 ) |
18 | 17 | oveq2d 7332 | . . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 })) → (𝑥( ·𝑠 ‘𝑊)𝑎) = (𝑥( ·𝑠 ‘𝑊) 0 )) |
19 | eqid 2736 | . . . . . . . 8 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊) | |
20 | eqid 2736 | . . . . . . . 8 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊) | |
21 | eqid 2736 | . . . . . . . 8 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | |
22 | 19, 20, 21, 9 | lmodvs0 20237 | . . . . . . 7 ⊢ ((𝑊 ∈ LMod ∧ 𝑥 ∈ (Base‘(Scalar‘𝑊))) → (𝑥( ·𝑠 ‘𝑊) 0 ) = 0 ) |
23 | 22 | 3ad2antr1 1187 | . . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 })) → (𝑥( ·𝑠 ‘𝑊) 0 ) = 0 ) |
24 | 18, 23 | eqtrd 2776 | . . . . 5 ⊢ ((𝑊 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 })) → (𝑥( ·𝑠 ‘𝑊)𝑎) = 0 ) |
25 | simpr3 1195 | . . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 })) → 𝑏 ∈ { 0 }) | |
26 | elsni 4587 | . . . . . 6 ⊢ (𝑏 ∈ { 0 } → 𝑏 = 0 ) | |
27 | 25, 26 | syl 17 | . . . . 5 ⊢ ((𝑊 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 })) → 𝑏 = 0 ) |
28 | 24, 27 | oveq12d 7334 | . . . 4 ⊢ ((𝑊 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 })) → ((𝑥( ·𝑠 ‘𝑊)𝑎)(+g‘𝑊)𝑏) = ( 0 (+g‘𝑊) 0 )) |
29 | eqid 2736 | . . . . . . 7 ⊢ (+g‘𝑊) = (+g‘𝑊) | |
30 | 8, 29, 9 | lmod0vlid 20233 | . . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ 0 ∈ (Base‘𝑊)) → ( 0 (+g‘𝑊) 0 ) = 0 ) |
31 | 10, 30 | mpdan 684 | . . . . 5 ⊢ (𝑊 ∈ LMod → ( 0 (+g‘𝑊) 0 ) = 0 ) |
32 | 31 | adantr 481 | . . . 4 ⊢ ((𝑊 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 })) → ( 0 (+g‘𝑊) 0 ) = 0 ) |
33 | 28, 32 | eqtrd 2776 | . . 3 ⊢ ((𝑊 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 })) → ((𝑥( ·𝑠 ‘𝑊)𝑎)(+g‘𝑊)𝑏) = 0 ) |
34 | ovex 7349 | . . . 4 ⊢ ((𝑥( ·𝑠 ‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ V | |
35 | 34 | elsn 4585 | . . 3 ⊢ (((𝑥( ·𝑠 ‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ { 0 } ↔ ((𝑥( ·𝑠 ‘𝑊)𝑎)(+g‘𝑊)𝑏) = 0 ) |
36 | 33, 35 | sylibr 233 | . 2 ⊢ ((𝑊 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 })) → ((𝑥( ·𝑠 ‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ { 0 }) |
37 | 1, 2, 3, 4, 5, 7, 11, 14, 36 | islssd 20277 | 1 ⊢ (𝑊 ∈ LMod → { 0 } ∈ 𝑆) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1086 = wceq 1540 ∈ wcel 2105 ≠ wne 2940 ∅c0 4266 {csn 4570 ‘cfv 6465 (class class class)co 7316 Basecbs 16986 +gcplusg 17036 Scalarcsca 17039 ·𝑠 cvsca 17040 0gc0g 17224 LModclmod 20203 LSubSpclss 20273 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-sep 5237 ax-nul 5244 ax-pow 5302 ax-pr 5366 ax-un 7629 ax-cnex 11006 ax-resscn 11007 ax-1cn 11008 ax-icn 11009 ax-addcl 11010 ax-addrcl 11011 ax-mulcl 11012 ax-mulrcl 11013 ax-mulcom 11014 ax-addass 11015 ax-mulass 11016 ax-distr 11017 ax-i2m1 11018 ax-1ne0 11019 ax-1rid 11020 ax-rnegex 11021 ax-rrecex 11022 ax-cnre 11023 ax-pre-lttri 11024 ax-pre-lttrn 11025 ax-pre-ltadd 11026 ax-pre-mulgt0 11027 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3349 df-reu 3350 df-rab 3404 df-v 3442 df-sbc 3726 df-csb 3842 df-dif 3899 df-un 3901 df-in 3903 df-ss 3913 df-pss 3915 df-nul 4267 df-if 4471 df-pw 4546 df-sn 4571 df-pr 4573 df-op 4577 df-uni 4850 df-iun 4938 df-br 5087 df-opab 5149 df-mpt 5170 df-tr 5204 df-id 5506 df-eprel 5512 df-po 5520 df-so 5521 df-fr 5562 df-we 5564 df-xp 5613 df-rel 5614 df-cnv 5615 df-co 5616 df-dm 5617 df-rn 5618 df-res 5619 df-ima 5620 df-pred 6224 df-ord 6291 df-on 6292 df-lim 6293 df-suc 6294 df-iota 6417 df-fun 6467 df-fn 6468 df-f 6469 df-f1 6470 df-fo 6471 df-f1o 6472 df-fv 6473 df-riota 7273 df-ov 7319 df-oprab 7320 df-mpo 7321 df-om 7759 df-2nd 7878 df-frecs 8145 df-wrecs 8176 df-recs 8250 df-rdg 8289 df-er 8547 df-en 8783 df-dom 8784 df-sdom 8785 df-pnf 11090 df-mnf 11091 df-xr 11092 df-ltxr 11093 df-le 11094 df-sub 11286 df-neg 11287 df-nn 12053 df-2 12115 df-sets 16939 df-slot 16957 df-ndx 16969 df-base 16987 df-plusg 17049 df-0g 17226 df-mgm 18400 df-sgrp 18449 df-mnd 18460 df-grp 18653 df-mgp 19793 df-ring 19857 df-lmod 20205 df-lss 20274 |
This theorem is referenced by: lspsn0 20350 lsp0 20351 lmhmkerlss 20393 lidl0 20570 lsatcv0 37270 lsatcveq0 37271 lsat0cv 37272 lsatcv0eq 37286 dochsat 39623 mapd0 39905 mapdcnvatN 39906 mapdat 39907 mapdn0 39909 hdmapeq0 40084 |
Copyright terms: Public domain | W3C validator |