Theorem lmod0vs 21175

Description: Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (ax-hvmul0 31617 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 488	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑊 ∈ LMod)
2		lmod0vs.f	. . . . . . . 8 ⊢ 𝐹 = (Scalar‘𝑊)
3	2	lmodring 21148	. . . . . . 7 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring)
4	3	adantr 486	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝐹 ∈ Ring)
5		eqid 2760	. . . . . . 7 ⊢ (Base‘𝐹) = (Base‘𝐹)
6		lmod0vs.o	. . . . . . 7 ⊢ 𝑂 = (0g‘𝐹)
7	5, 6	ring0cl 20501	. . . . . 6 ⊢ (𝐹 ∈ Ring → 𝑂 ∈ (Base‘𝐹))
8	4, 7	syl 18	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑂 ∈ (Base‘𝐹))
9		simpr 490	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉)
10		lmod0vs.v	. . . . . 6 ⊢ 𝑉 = (Base‘𝑊)
11		eqid 2760	. . . . . 6 ⊢ (+g‘𝑊) = (+g‘𝑊)
12		lmod0vs.s	. . . . . 6 ⊢ · = ( ·𝑠 ‘𝑊)
13		eqid 2760	. . . . . 6 ⊢ (+g‘𝐹) = (+g‘𝐹)
14	10, 11, 2, 12, 5, 13	lmodvsdir 21166	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ (𝑂 ∈ (Base‘𝐹) ∧ 𝑂 ∈ (Base‘𝐹) ∧ 𝑋 ∈ 𝑉)) → ((𝑂(+g‘𝐹)𝑂) · 𝑋) = ((𝑂 · 𝑋)(+g‘𝑊)(𝑂 · 𝑋)))
15	1, 8, 8, 9, 14	syl13anc 1399	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑂(+g‘𝐹)𝑂) · 𝑋) = ((𝑂 · 𝑋)(+g‘𝑊)(𝑂 · 𝑋)))
16		ringgrp 20469	. . . . . . 7 ⊢ (𝐹 ∈ Ring → 𝐹 ∈ Grp)
17	4, 16	syl 18	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝐹 ∈ Grp)
18	5, 13, 6	grplid 19183	. . . . . 6 ⊢ ((𝐹 ∈ Grp ∧ 𝑂 ∈ (Base‘𝐹)) → (𝑂(+g‘𝐹)𝑂) = 𝑂)
19	17, 8, 18	syl2anc 596	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑂(+g‘𝐹)𝑂) = 𝑂)
20	19	oveq1d 7435	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑂(+g‘𝐹)𝑂) · 𝑋) = (𝑂 · 𝑋))
21	15, 20	eqtr3d 2797	. . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑂 · 𝑋)(+g‘𝑊)(𝑂 · 𝑋)) = (𝑂 · 𝑋))
22	10, 2, 12, 5	lmodvscl 21158	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑂 ∈ (Base‘𝐹) ∧ 𝑋 ∈ 𝑉) → (𝑂 · 𝑋) ∈ 𝑉)
23	1, 8, 9, 22	syl3anc 1398	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑂 · 𝑋) ∈ 𝑉)
24		lmod0vs.z	. . . . 5 ⊢ 0 = (0g‘𝑊)
25	10, 11, 24	lmod0vid 21174	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ (𝑂 · 𝑋) ∈ 𝑉) → (((𝑂 · 𝑋)(+g‘𝑊)(𝑂 · 𝑋)) = (𝑂 · 𝑋) ↔ 0 = (𝑂 · 𝑋)))
26	23, 25	syldan 603	. . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (((𝑂 · 𝑋)(+g‘𝑊)(𝑂 · 𝑋)) = (𝑂 · 𝑋) ↔ 0 = (𝑂 · 𝑋)))
27	21, 26	mpbid 235	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 0 = (𝑂 · 𝑋))
28	27	eqcomd 2766	1 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑂 · 𝑋) = 0 )

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ‘cfv 6538  (class class class)co 7420  Basecbs 17392  +_gcplusg 17433  Scalarcsca 17436   ·_𝑠 cvsca 17437  0_gc0g 17615  Grpcgrp 19149  Ringcrg 20464  LModclmod 21140

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-iota 6494  df-fun 6540  df-fv 6546  df-riota 7377  df-ov 7423  df-0g 17617  df-mgm 18821  df-sgrp 18913  df-mnd 18929  df-grp 19152  df-ring 20466  df-lmod 21142

This theorem is used by:  lmodvs0  21176  lmodvsmmulgdi  21177  lcomfsupp  21182  lmodvneg1  21185  mptscmfsupp0  21207  lvecvs0or  21391  lssvs0or  21393  lspsneleq  21398  lspdisj  21408  lspfixed  21411  lspexch  21412  lspsolvlem  21425  lspsolv  21426  uvcresum  22104  frlmsslsp  22107  frlmup1  22109  frlmup2  22110  ascl0  22197  mplcoe1  22351  mplbas2  22356  selvvvval  22456  ply10s0  22580  gsummoncoe1  22631  evls1fpws  22692  pmatcollpwscmatlem1  23112  idpm2idmp  23124  mp2pm2mplem4  23132  pm2mpmhmlem1  23141  monmat2matmon  23147  cpmidpmatlem3  23195  clm0vs  25421  plypf1  26536  lmodslmd  33811  ply1coedeg  34167  r1p0  34184  ply1degltdimlem  34300  lbsdiflsp0  34304  fedgmullem2  34308  extdgfialglem2  34371  lshpkrlem1  40260  ldual0vs  40310  lclkrlem1  42656  lcd0vs  42765  baerlem3lem1  42857  baerlem5blem1  42859  hdmap14lem2a  43017  hdmap14lem4a  43021  hdmap14lem6  43023  hgmapval0  43042  lmod0vsd  43682  prjspersym  43728  prjspreln0  43730  lmod0rng  49419  scmsuppss  49576  lmodvsmdi  49584  ply1mulgsumlem4  49594  lincval1  49624  lincvalsc0  49626  linc0scn0  49628  linc1  49630  ldepsprlem  49677