Theorem lmod0vs 19786

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.)

Hypotheses

Ref	Expression
lmod0vs.v	⊢ 𝑉 = (Base‘𝑊)
lmod0vs.f	⊢ 𝐹 = (Scalar‘𝑊)
lmod0vs.s	⊢ · = ( ·𝑠 ‘𝑊)
lmod0vs.o	⊢ 𝑂 = (0g‘𝐹)
lmod0vs.z	⊢ 0 = (0g‘𝑊)

Assertion

Ref	Expression
lmod0vs	⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑂 · 𝑋) = 0 )

Proof of Theorem lmod0vs

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 )

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  0_gc0g 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