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 19570 | . 2 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) | |
2 | lmodvacl.v | . . 3 ⊢ 𝑉 = (Base‘𝑊) | |
3 | lmodvacl.a | . . 3 ⊢ + = (+g‘𝑊) | |
4 | 2, 3 | grpcl 18049 | . 2 ⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉) |
5 | 1, 4 | syl3an1 1155 | 1 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1079 = wceq 1528 ∈ wcel 2105 ‘cfv 6348 (class class class)co 7145 Basecbs 16471 +gcplusg 16553 Grpcgrp 18041 LModclmod 19563 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-nul 5201 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-sbc 3770 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-iota 6307 df-fv 6356 df-ov 7148 df-mgm 17840 df-sgrp 17889 df-mnd 17900 df-grp 18044 df-lmod 19565 |
This theorem is referenced by: lmodcom 19609 lmodvsghm 19624 lss1 19639 lspprabs 19796 lspabs2 19821 lspabs3 19822 lspfixed 19829 lspexch 19830 lspsolvlem 19843 ipdir 20711 ipdi 20712 ip2di 20713 ocvlss 20744 frlmphl 20853 frlmup1 20870 nmparlem 23769 minveclem2 23956 lsatfixedN 36025 lfl0f 36085 lfladdcl 36087 lflnegcl 36091 lflvscl 36093 lkrlss 36111 lshpkrlem5 36130 lshpkrlem6 36131 dvh3dim2 38464 dvh3dim3N 38465 lcfrlem17 38575 lcfrlem19 38577 lcfrlem20 38578 lcfrlem23 38581 baerlem3lem1 38723 baerlem5alem1 38724 baerlem5blem1 38725 baerlem5alem2 38727 baerlem5blem2 38728 mapdindp0 38735 mapdindp2 38737 mapdindp4 38739 mapdh6lem2N 38750 mapdh6aN 38751 mapdh6dN 38755 mapdh6eN 38756 mapdh6hN 38759 hdmap1l6lem2 38824 hdmap1l6a 38825 hdmap1l6d 38829 hdmap1l6e 38830 hdmap1l6h 38833 hdmap11lem1 38857 hdmap11lem2 38858 hdmapneg 38862 hdmaprnlem3N 38866 hdmaprnlem3uN 38867 hdmaprnlem6N 38870 hdmaprnlem7N 38871 hdmaprnlem9N 38873 hdmaprnlem3eN 38874 hdmap14lem10 38893 hdmapinvlem3 38936 hdmapinvlem4 38937 hdmapglem7b 38944 hlhilphllem 38975 frlmsnic 39027 lincsumcl 44414 |
Copyright terms: Public domain | W3C validator |