![]() |
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 30126 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 483 | . . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑊 ∈ LMod) | |
2 | lmod0vs.f | . . . . . . . 8 ⊢ 𝐹 = (Scalar‘𝑊) | |
3 | 2 | lmodring 20428 | . . . . . . 7 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring) |
4 | 3 | adantr 481 | . . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝐹 ∈ Ring) |
5 | eqid 2731 | . . . . . . 7 ⊢ (Base‘𝐹) = (Base‘𝐹) | |
6 | lmod0vs.o | . . . . . . 7 ⊢ 𝑂 = (0g‘𝐹) | |
7 | 5, 6 | ring0cl 20041 | . . . . . 6 ⊢ (𝐹 ∈ Ring → 𝑂 ∈ (Base‘𝐹)) |
8 | 4, 7 | syl 17 | . . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑂 ∈ (Base‘𝐹)) |
9 | simpr 485 | . . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉) | |
10 | lmod0vs.v | . . . . . 6 ⊢ 𝑉 = (Base‘𝑊) | |
11 | eqid 2731 | . . . . . 6 ⊢ (+g‘𝑊) = (+g‘𝑊) | |
12 | lmod0vs.s | . . . . . 6 ⊢ · = ( ·𝑠 ‘𝑊) | |
13 | eqid 2731 | . . . . . 6 ⊢ (+g‘𝐹) = (+g‘𝐹) | |
14 | 10, 11, 2, 12, 5, 13 | lmodvsdir 20445 | . . . . 5 ⊢ ((𝑊 ∈ LMod ∧ (𝑂 ∈ (Base‘𝐹) ∧ 𝑂 ∈ (Base‘𝐹) ∧ 𝑋 ∈ 𝑉)) → ((𝑂(+g‘𝐹)𝑂) · 𝑋) = ((𝑂 · 𝑋)(+g‘𝑊)(𝑂 · 𝑋))) |
15 | 1, 8, 8, 9, 14 | syl13anc 1372 | . . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑂(+g‘𝐹)𝑂) · 𝑋) = ((𝑂 · 𝑋)(+g‘𝑊)(𝑂 · 𝑋))) |
16 | ringgrp 20019 | . . . . . . 7 ⊢ (𝐹 ∈ Ring → 𝐹 ∈ Grp) | |
17 | 4, 16 | syl 17 | . . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝐹 ∈ Grp) |
18 | 5, 13, 6 | grplid 18827 | . . . . . 6 ⊢ ((𝐹 ∈ Grp ∧ 𝑂 ∈ (Base‘𝐹)) → (𝑂(+g‘𝐹)𝑂) = 𝑂) |
19 | 17, 8, 18 | syl2anc 584 | . . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑂(+g‘𝐹)𝑂) = 𝑂) |
20 | 19 | oveq1d 7408 | . . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑂(+g‘𝐹)𝑂) · 𝑋) = (𝑂 · 𝑋)) |
21 | 15, 20 | eqtr3d 2773 | . . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑂 · 𝑋)(+g‘𝑊)(𝑂 · 𝑋)) = (𝑂 · 𝑋)) |
22 | 10, 2, 12, 5 | lmodvscl 20438 | . . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑂 ∈ (Base‘𝐹) ∧ 𝑋 ∈ 𝑉) → (𝑂 · 𝑋) ∈ 𝑉) |
23 | 1, 8, 9, 22 | syl3anc 1371 | . . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑂 · 𝑋) ∈ 𝑉) |
24 | lmod0vs.z | . . . . 5 ⊢ 0 = (0g‘𝑊) | |
25 | 10, 11, 24 | lmod0vid 20453 | . . . 4 ⊢ ((𝑊 ∈ LMod ∧ (𝑂 · 𝑋) ∈ 𝑉) → (((𝑂 · 𝑋)(+g‘𝑊)(𝑂 · 𝑋)) = (𝑂 · 𝑋) ↔ 0 = (𝑂 · 𝑋))) |
26 | 23, 25 | syldan 591 | . . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (((𝑂 · 𝑋)(+g‘𝑊)(𝑂 · 𝑋)) = (𝑂 · 𝑋) ↔ 0 = (𝑂 · 𝑋))) |
27 | 21, 26 | mpbid 231 | . 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 0 = (𝑂 · 𝑋)) |
28 | 27 | eqcomd 2737 | 1 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑂 · 𝑋) = 0 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ‘cfv 6532 (class class class)co 7393 Basecbs 17126 +gcplusg 17179 Scalarcsca 17182 ·𝑠 cvsca 17183 0gc0g 17367 Grpcgrp 18794 Ringcrg 20014 LModclmod 20420 |
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-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-sep 5292 ax-nul 5299 ax-pr 5420 |
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-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3774 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4523 df-sn 4623 df-pr 4625 df-op 4629 df-uni 4902 df-br 5142 df-opab 5204 df-mpt 5225 df-id 5567 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-iota 6484 df-fun 6534 df-fv 6540 df-riota 7349 df-ov 7396 df-0g 17369 df-mgm 18543 df-sgrp 18592 df-mnd 18603 df-grp 18797 df-ring 20016 df-lmod 20422 |
This theorem is referenced by: lmodvs0 20455 lmodvsmmulgdi 20456 lcomfsupp 20461 lmodvneg1 20464 mptscmfsupp0 20486 lvecvs0or 20670 lssvs0or 20672 lspsneleq 20677 lspdisj 20687 lspfixed 20690 lspexch 20691 lspsolvlem 20704 lspsolv 20705 uvcresum 21281 frlmsslsp 21284 frlmup1 21286 frlmup2 21287 ascl0 21369 mplcoe1 21520 mplbas2 21525 ply10s0 21709 ply1scl0 21743 gsummoncoe1 21757 pmatcollpwscmatlem1 22220 idpm2idmp 22232 mp2pm2mplem4 22240 pm2mpmhmlem1 22249 monmat2matmon 22255 cpmidpmatlem3 22303 clm0vs 24540 plypf1 25655 lmodslmd 32220 evls1fpws 32487 ply1degltdimlem 32543 lbsdiflsp0 32547 fedgmullem2 32551 lshpkrlem1 37783 ldual0vs 37833 lclkrlem1 40180 lcd0vs 40289 baerlem3lem1 40381 baerlem5blem1 40383 hdmap14lem2a 40541 hdmap14lem4a 40545 hdmap14lem6 40547 hgmapval0 40566 prjspersym 41129 prjspreln0 41131 prjspner1 41148 lmod0rng 46412 scmsuppss 46694 lmodvsmdi 46704 ply1mulgsumlem4 46716 lincval1 46746 lincvalsc0 46748 linc0scn0 46750 linc1 46752 ldepsprlem 46799 |
Copyright terms: Public domain | W3C validator |