![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lmodvacl | Structured version Visualization version GIF version |
Description: Closure of vector addition for a left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
Ref | Expression |
---|---|
lmodvacl.v | ⊢ 𝑉 = (Base‘𝑊) |
lmodvacl.a | ⊢ + = (+g‘𝑊) |
Ref | Expression |
---|---|
lmodvacl | ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lmodgrp 20276 | . 2 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) | |
2 | lmodvacl.v | . . 3 ⊢ 𝑉 = (Base‘𝑊) | |
3 | lmodvacl.a | . . 3 ⊢ + = (+g‘𝑊) | |
4 | 2, 3 | grpcl 18710 | . 2 ⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉) |
5 | 1, 4 | syl3an1 1163 | 1 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ‘cfv 6493 (class class class)co 7351 Basecbs 17037 +gcplusg 17087 Grpcgrp 18702 LModclmod 20269 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 ax-nul 5261 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-sbc 3738 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-iota 6445 df-fv 6501 df-ov 7354 df-mgm 18451 df-sgrp 18500 df-mnd 18511 df-grp 18705 df-lmod 20271 |
This theorem is referenced by: lmodcom 20315 lmodvsghm 20330 lss1 20346 lspprabs 20503 lspabs2 20528 lspabs3 20529 lspfixed 20536 lspexch 20537 lspsolvlem 20550 ipdir 20990 ipdi 20991 ip2di 20992 ocvlss 21023 frlmphl 21134 frlmup1 21151 nmparlem 24549 minveclem2 24736 lsatfixedN 37403 lfl0f 37463 lfladdcl 37465 lflnegcl 37469 lflvscl 37471 lkrlss 37489 lshpkrlem5 37508 lshpkrlem6 37509 dvh3dim2 39843 dvh3dim3N 39844 lcfrlem17 39954 lcfrlem19 39956 lcfrlem20 39957 lcfrlem23 39960 baerlem3lem1 40102 baerlem5alem1 40103 baerlem5blem1 40104 baerlem5alem2 40106 baerlem5blem2 40107 mapdindp0 40114 mapdindp2 40116 mapdindp4 40118 mapdh6lem2N 40129 mapdh6aN 40130 mapdh6dN 40134 mapdh6eN 40135 mapdh6hN 40138 hdmap1l6lem2 40203 hdmap1l6a 40204 hdmap1l6d 40208 hdmap1l6e 40209 hdmap1l6h 40212 hdmap11lem1 40236 hdmap11lem2 40237 hdmapneg 40241 hdmaprnlem3N 40245 hdmaprnlem3uN 40246 hdmaprnlem6N 40249 hdmaprnlem7N 40250 hdmaprnlem9N 40252 hdmaprnlem3eN 40253 hdmap14lem10 40272 hdmapinvlem3 40315 hdmapinvlem4 40316 hdmapglem7b 40323 hlhilphllem 40358 frlmsnic 40654 lincsumcl 46407 |
Copyright terms: Public domain | W3C validator |