![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lmod0vs | Structured version Visualization version GIF version |
Description: Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (ax-hvmul0 30530 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
Ref | Expression |
---|---|
lmod0vs.v | β’ π = (Baseβπ) |
lmod0vs.f | β’ πΉ = (Scalarβπ) |
lmod0vs.s | β’ Β· = ( Β·π βπ) |
lmod0vs.o | β’ π = (0gβπΉ) |
lmod0vs.z | β’ 0 = (0gβπ) |
Ref | Expression |
---|---|
lmod0vs | β’ ((π β LMod β§ π β π) β (π Β· π) = 0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 481 | . . . . 5 β’ ((π β LMod β§ π β π) β π β LMod) | |
2 | lmod0vs.f | . . . . . . . 8 β’ πΉ = (Scalarβπ) | |
3 | 2 | lmodring 20622 | . . . . . . 7 β’ (π β LMod β πΉ β Ring) |
4 | 3 | adantr 479 | . . . . . 6 β’ ((π β LMod β§ π β π) β πΉ β Ring) |
5 | eqid 2730 | . . . . . . 7 β’ (BaseβπΉ) = (BaseβπΉ) | |
6 | lmod0vs.o | . . . . . . 7 β’ π = (0gβπΉ) | |
7 | 5, 6 | ring0cl 20155 | . . . . . 6 β’ (πΉ β Ring β π β (BaseβπΉ)) |
8 | 4, 7 | syl 17 | . . . . 5 β’ ((π β LMod β§ π β π) β π β (BaseβπΉ)) |
9 | simpr 483 | . . . . 5 β’ ((π β LMod β§ π β π) β π β π) | |
10 | lmod0vs.v | . . . . . 6 β’ π = (Baseβπ) | |
11 | eqid 2730 | . . . . . 6 β’ (+gβπ) = (+gβπ) | |
12 | lmod0vs.s | . . . . . 6 β’ Β· = ( Β·π βπ) | |
13 | eqid 2730 | . . . . . 6 β’ (+gβπΉ) = (+gβπΉ) | |
14 | 10, 11, 2, 12, 5, 13 | lmodvsdir 20640 | . . . . 5 β’ ((π β LMod β§ (π β (BaseβπΉ) β§ π β (BaseβπΉ) β§ π β π)) β ((π(+gβπΉ)π) Β· π) = ((π Β· π)(+gβπ)(π Β· π))) |
15 | 1, 8, 8, 9, 14 | syl13anc 1370 | . . . 4 β’ ((π β LMod β§ π β π) β ((π(+gβπΉ)π) Β· π) = ((π Β· π)(+gβπ)(π Β· π))) |
16 | ringgrp 20132 | . . . . . . 7 β’ (πΉ β Ring β πΉ β Grp) | |
17 | 4, 16 | syl 17 | . . . . . 6 β’ ((π β LMod β§ π β π) β πΉ β Grp) |
18 | 5, 13, 6 | grplid 18888 | . . . . . 6 β’ ((πΉ β Grp β§ π β (BaseβπΉ)) β (π(+gβπΉ)π) = π) |
19 | 17, 8, 18 | syl2anc 582 | . . . . 5 β’ ((π β LMod β§ π β π) β (π(+gβπΉ)π) = π) |
20 | 19 | oveq1d 7426 | . . . 4 β’ ((π β LMod β§ π β π) β ((π(+gβπΉ)π) Β· π) = (π Β· π)) |
21 | 15, 20 | eqtr3d 2772 | . . 3 β’ ((π β LMod β§ π β π) β ((π Β· π)(+gβπ)(π Β· π)) = (π Β· π)) |
22 | 10, 2, 12, 5 | lmodvscl 20632 | . . . . 5 β’ ((π β LMod β§ π β (BaseβπΉ) β§ π β π) β (π Β· π) β π) |
23 | 1, 8, 9, 22 | syl3anc 1369 | . . . 4 β’ ((π β LMod β§ π β π) β (π Β· π) β π) |
24 | lmod0vs.z | . . . . 5 β’ 0 = (0gβπ) | |
25 | 10, 11, 24 | lmod0vid 20648 | . . . 4 β’ ((π β LMod β§ (π Β· π) β π) β (((π Β· π)(+gβπ)(π Β· π)) = (π Β· π) β 0 = (π Β· π))) |
26 | 23, 25 | syldan 589 | . . 3 β’ ((π β LMod β§ π β π) β (((π Β· π)(+gβπ)(π Β· π)) = (π Β· π) β 0 = (π Β· π))) |
27 | 21, 26 | mpbid 231 | . 2 β’ ((π β LMod β§ π β π) β 0 = (π Β· π)) |
28 | 27 | eqcomd 2736 | 1 β’ ((π β LMod β§ π β π) β (π Β· π) = 0 ) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β wb 205 β§ wa 394 = wceq 1539 β wcel 2104 βcfv 6542 (class class class)co 7411 Basecbs 17148 +gcplusg 17201 Scalarcsca 17204 Β·π cvsca 17205 0gc0g 17389 Grpcgrp 18855 Ringcrg 20127 LModclmod 20614 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-sep 5298 ax-nul 5305 ax-pr 5426 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-iota 6494 df-fun 6544 df-fv 6550 df-riota 7367 df-ov 7414 df-0g 17391 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-grp 18858 df-ring 20129 df-lmod 20616 |
This theorem is referenced by: lmodvs0 20650 lmodvsmmulgdi 20651 lcomfsupp 20656 lmodvneg1 20659 mptscmfsupp0 20681 lvecvs0or 20866 lssvs0or 20868 lspsneleq 20873 lspdisj 20883 lspfixed 20886 lspexch 20887 lspsolvlem 20900 lspsolv 20901 uvcresum 21567 frlmsslsp 21570 frlmup1 21572 frlmup2 21573 ascl0 21657 mplcoe1 21811 mplbas2 21816 ply10s0 21998 ply1scl0OLD 22033 gsummoncoe1 22048 pmatcollpwscmatlem1 22511 idpm2idmp 22523 mp2pm2mplem4 22531 pm2mpmhmlem1 22540 monmat2matmon 22546 cpmidpmatlem3 22594 clm0vs 24842 plypf1 25961 lmodslmd 32619 evls1fpws 32920 r1p0 32951 ply1degltdimlem 32995 lbsdiflsp0 32999 fedgmullem2 33003 lshpkrlem1 38283 ldual0vs 38333 lclkrlem1 40680 lcd0vs 40789 baerlem3lem1 40881 baerlem5blem1 40883 hdmap14lem2a 41041 hdmap14lem4a 41045 hdmap14lem6 41047 hgmapval0 41066 selvvvval 41459 prjspersym 41651 prjspreln0 41653 prjspner1 41670 lmod0rng 46908 scmsuppss 47136 lmodvsmdi 47146 ply1mulgsumlem4 47157 lincval1 47187 lincvalsc0 47189 linc0scn0 47191 linc1 47193 ldepsprlem 47240 |
Copyright terms: Public domain | W3C validator |