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 28945 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 486 | . . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑊 ∈ LMod) | |
2 | lmod0vs.f | . . . . . . . 8 ⊢ 𝐹 = (Scalar‘𝑊) | |
3 | 2 | lmodring 19761 | . . . . . . 7 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring) |
4 | 3 | adantr 484 | . . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝐹 ∈ Ring) |
5 | eqid 2738 | . . . . . . 7 ⊢ (Base‘𝐹) = (Base‘𝐹) | |
6 | lmod0vs.o | . . . . . . 7 ⊢ 𝑂 = (0g‘𝐹) | |
7 | 5, 6 | ring0cl 19441 | . . . . . 6 ⊢ (𝐹 ∈ Ring → 𝑂 ∈ (Base‘𝐹)) |
8 | 4, 7 | syl 17 | . . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑂 ∈ (Base‘𝐹)) |
9 | simpr 488 | . . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉) | |
10 | lmod0vs.v | . . . . . 6 ⊢ 𝑉 = (Base‘𝑊) | |
11 | eqid 2738 | . . . . . 6 ⊢ (+g‘𝑊) = (+g‘𝑊) | |
12 | lmod0vs.s | . . . . . 6 ⊢ · = ( ·𝑠 ‘𝑊) | |
13 | eqid 2738 | . . . . . 6 ⊢ (+g‘𝐹) = (+g‘𝐹) | |
14 | 10, 11, 2, 12, 5, 13 | lmodvsdir 19777 | . . . . 5 ⊢ ((𝑊 ∈ LMod ∧ (𝑂 ∈ (Base‘𝐹) ∧ 𝑂 ∈ (Base‘𝐹) ∧ 𝑋 ∈ 𝑉)) → ((𝑂(+g‘𝐹)𝑂) · 𝑋) = ((𝑂 · 𝑋)(+g‘𝑊)(𝑂 · 𝑋))) |
15 | 1, 8, 8, 9, 14 | syl13anc 1373 | . . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑂(+g‘𝐹)𝑂) · 𝑋) = ((𝑂 · 𝑋)(+g‘𝑊)(𝑂 · 𝑋))) |
16 | ringgrp 19421 | . . . . . . 7 ⊢ (𝐹 ∈ Ring → 𝐹 ∈ Grp) | |
17 | 4, 16 | syl 17 | . . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝐹 ∈ Grp) |
18 | 5, 13, 6 | grplid 18251 | . . . . . 6 ⊢ ((𝐹 ∈ Grp ∧ 𝑂 ∈ (Base‘𝐹)) → (𝑂(+g‘𝐹)𝑂) = 𝑂) |
19 | 17, 8, 18 | syl2anc 587 | . . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑂(+g‘𝐹)𝑂) = 𝑂) |
20 | 19 | oveq1d 7185 | . . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑂(+g‘𝐹)𝑂) · 𝑋) = (𝑂 · 𝑋)) |
21 | 15, 20 | eqtr3d 2775 | . . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑂 · 𝑋)(+g‘𝑊)(𝑂 · 𝑋)) = (𝑂 · 𝑋)) |
22 | 10, 2, 12, 5 | lmodvscl 19770 | . . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑂 ∈ (Base‘𝐹) ∧ 𝑋 ∈ 𝑉) → (𝑂 · 𝑋) ∈ 𝑉) |
23 | 1, 8, 9, 22 | syl3anc 1372 | . . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑂 · 𝑋) ∈ 𝑉) |
24 | lmod0vs.z | . . . . 5 ⊢ 0 = (0g‘𝑊) | |
25 | 10, 11, 24 | lmod0vid 19785 | . . . 4 ⊢ ((𝑊 ∈ LMod ∧ (𝑂 · 𝑋) ∈ 𝑉) → (((𝑂 · 𝑋)(+g‘𝑊)(𝑂 · 𝑋)) = (𝑂 · 𝑋) ↔ 0 = (𝑂 · 𝑋))) |
26 | 23, 25 | syldan 594 | . . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (((𝑂 · 𝑋)(+g‘𝑊)(𝑂 · 𝑋)) = (𝑂 · 𝑋) ↔ 0 = (𝑂 · 𝑋))) |
27 | 21, 26 | mpbid 235 | . 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 0 = (𝑂 · 𝑋)) |
28 | 27 | eqcomd 2744 | 1 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑂 · 𝑋) = 0 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1542 ∈ wcel 2114 ‘cfv 6339 (class class class)co 7170 Basecbs 16586 +gcplusg 16668 Scalarcsca 16671 ·𝑠 cvsca 16672 0gc0g 16816 Grpcgrp 18219 Ringcrg 19416 LModclmod 19753 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2710 ax-sep 5167 ax-nul 5174 ax-pr 5296 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-ral 3058 df-rex 3059 df-reu 3060 df-rmo 3061 df-rab 3062 df-v 3400 df-sbc 3681 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-nul 4212 df-if 4415 df-sn 4517 df-pr 4519 df-op 4523 df-uni 4797 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5429 df-xp 5531 df-rel 5532 df-cnv 5533 df-co 5534 df-dm 5535 df-iota 6297 df-fun 6341 df-fv 6347 df-riota 7127 df-ov 7173 df-0g 16818 df-mgm 17968 df-sgrp 18017 df-mnd 18028 df-grp 18222 df-ring 19418 df-lmod 19755 |
This theorem is referenced by: lmodvs0 19787 lmodvsmmulgdi 19788 lcomfsupp 19793 lmodvneg1 19796 mptscmfsupp0 19818 lvecvs0or 19999 lssvs0or 20001 lspsneleq 20006 lspdisj 20016 lspfixed 20019 lspexch 20020 lspsolvlem 20033 lspsolv 20034 uvcresum 20609 frlmsslsp 20612 frlmup1 20614 frlmup2 20615 ascl0 20697 mplcoe1 20848 mplbas2 20853 ply10s0 21031 ply1scl0 21065 gsummoncoe1 21079 pmatcollpwscmatlem1 21540 idpm2idmp 21552 mp2pm2mplem4 21560 pm2mpmhmlem1 21569 monmat2matmon 21575 cpmidpmatlem3 21623 clm0vs 23847 plypf1 24961 lmodslmd 31034 lbsdiflsp0 31279 fedgmullem2 31283 lshpkrlem1 36747 ldual0vs 36797 lclkrlem1 39143 lcd0vs 39252 baerlem3lem1 39344 baerlem5blem1 39346 hdmap14lem2a 39504 hdmap14lem4a 39508 hdmap14lem6 39510 hgmapval0 39529 prjspersym 40023 prjspreln0 40025 prjspner1 40040 lmod0rng 44960 scmsuppss 45242 lmodvsmdi 45252 ply1mulgsumlem4 45264 lincval1 45294 lincvalsc0 45296 linc0scn0 45298 linc1 45300 ldepsprlem 45347 |
Copyright terms: Public domain | W3C validator |