MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmod0vs Structured version   Unicode version

Theorem lmod0vs 16986
Description: Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (ax-hvmul0 24417 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
Hypotheses
Ref Expression
lmod0vs.v  |-  V  =  ( Base `  W
)
lmod0vs.f  |-  F  =  (Scalar `  W )
lmod0vs.s  |-  .x.  =  ( .s `  W )
lmod0vs.o  |-  O  =  ( 0g `  F
)
lmod0vs.z  |-  .0.  =  ( 0g `  W )
Assertion
Ref Expression
lmod0vs  |-  ( ( W  e.  LMod  /\  X  e.  V )  ->  ( O  .x.  X )  =  .0.  )

Proof of Theorem lmod0vs
StepHypRef Expression
1 simpl 457 . . . . 5  |-  ( ( W  e.  LMod  /\  X  e.  V )  ->  W  e.  LMod )
2 lmod0vs.f . . . . . . . 8  |-  F  =  (Scalar `  W )
32lmodrng 16961 . . . . . . 7  |-  ( W  e.  LMod  ->  F  e. 
Ring )
43adantr 465 . . . . . 6  |-  ( ( W  e.  LMod  /\  X  e.  V )  ->  F  e.  Ring )
5 eqid 2443 . . . . . . 7  |-  ( Base `  F )  =  (
Base `  F )
6 lmod0vs.o . . . . . . 7  |-  O  =  ( 0g `  F
)
75, 6rng0cl 16671 . . . . . 6  |-  ( F  e.  Ring  ->  O  e.  ( Base `  F
) )
84, 7syl 16 . . . . 5  |-  ( ( W  e.  LMod  /\  X  e.  V )  ->  O  e.  ( Base `  F
) )
9 simpr 461 . . . . 5  |-  ( ( W  e.  LMod  /\  X  e.  V )  ->  X  e.  V )
10 lmod0vs.v . . . . . 6  |-  V  =  ( Base `  W
)
11 eqid 2443 . . . . . 6  |-  ( +g  `  W )  =  ( +g  `  W )
12 lmod0vs.s . . . . . 6  |-  .x.  =  ( .s `  W )
13 eqid 2443 . . . . . 6  |-  ( +g  `  F )  =  ( +g  `  F )
1410, 11, 2, 12, 5, 13lmodvsdir 16977 . . . . 5  |-  ( ( W  e.  LMod  /\  ( O  e.  ( Base `  F )  /\  O  e.  ( Base `  F
)  /\  X  e.  V ) )  -> 
( ( O ( +g  `  F ) O )  .x.  X
)  =  ( ( O  .x.  X ) ( +g  `  W
) ( O  .x.  X ) ) )
151, 8, 8, 9, 14syl13anc 1220 . . . 4  |-  ( ( W  e.  LMod  /\  X  e.  V )  ->  (
( O ( +g  `  F ) O ) 
.x.  X )  =  ( ( O  .x.  X ) ( +g  `  W ) ( O 
.x.  X ) ) )
16 rnggrp 16655 . . . . . . 7  |-  ( F  e.  Ring  ->  F  e. 
Grp )
174, 16syl 16 . . . . . 6  |-  ( ( W  e.  LMod  /\  X  e.  V )  ->  F  e.  Grp )
185, 13, 6grplid 15573 . . . . . 6  |-  ( ( F  e.  Grp  /\  O  e.  ( Base `  F ) )  -> 
( O ( +g  `  F ) O )  =  O )
1917, 8, 18syl2anc 661 . . . . 5  |-  ( ( W  e.  LMod  /\  X  e.  V )  ->  ( O ( +g  `  F
) O )  =  O )
2019oveq1d 6111 . . . 4  |-  ( ( W  e.  LMod  /\  X  e.  V )  ->  (
( O ( +g  `  F ) O ) 
.x.  X )  =  ( O  .x.  X
) )
2115, 20eqtr3d 2477 . . 3  |-  ( ( W  e.  LMod  /\  X  e.  V )  ->  (
( O  .x.  X
) ( +g  `  W
) ( O  .x.  X ) )  =  ( O  .x.  X
) )
2210, 2, 12, 5lmodvscl 16970 . . . . 5  |-  ( ( W  e.  LMod  /\  O  e.  ( Base `  F
)  /\  X  e.  V )  ->  ( O  .x.  X )  e.  V )
231, 8, 9, 22syl3anc 1218 . . . 4  |-  ( ( W  e.  LMod  /\  X  e.  V )  ->  ( O  .x.  X )  e.  V )
24 lmod0vs.z . . . . 5  |-  .0.  =  ( 0g `  W )
2510, 11, 24lmod0vid 16985 . . . 4  |-  ( ( W  e.  LMod  /\  ( O  .x.  X )  e.  V )  ->  (
( ( O  .x.  X ) ( +g  `  W ) ( O 
.x.  X ) )  =  ( O  .x.  X )  <->  .0.  =  ( O  .x.  X ) ) )
2623, 25syldan 470 . . 3  |-  ( ( W  e.  LMod  /\  X  e.  V )  ->  (
( ( O  .x.  X ) ( +g  `  W ) ( O 
.x.  X ) )  =  ( O  .x.  X )  <->  .0.  =  ( O  .x.  X ) ) )
2721, 26mpbid 210 . 2  |-  ( ( W  e.  LMod  /\  X  e.  V )  ->  .0.  =  ( O  .x.  X ) )
2827eqcomd 2448 1  |-  ( ( W  e.  LMod  /\  X  e.  V )  ->  ( O  .x.  X )  =  .0.  )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    e. wcel 1756   ` cfv 5423  (class class class)co 6096   Basecbs 14179   +g cplusg 14243  Scalarcsca 14246   .scvsca 14247   0gc0g 14383   Grpcgrp 15415   Ringcrg 16650   LModclmod 16953
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pow 4475  ax-pr 4536
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-ral 2725  df-rex 2726  df-reu 2727  df-rmo 2728  df-rab 2729  df-v 2979  df-sbc 3192  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-uni 4097  df-br 4298  df-opab 4356  df-mpt 4357  df-id 4641  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-iota 5386  df-fun 5425  df-fv 5431  df-riota 6057  df-ov 6099  df-0g 14385  df-mnd 15420  df-grp 15550  df-rng 16652  df-lmod 16955
This theorem is referenced by:  lmodvs0  16987  lcomfsupOLD  16989  lcomfsupp  16990  lmodvneg1  16993  mptscmfsupp0  17016  lvecvs0or  17194  lssvs0or  17196  lspsneleq  17201  lspdisj  17211  lspfixed  17214  lspexch  17215  lspsolvlem  17228  lspsolv  17229  mplcoe1  17549  mplbas2  17556  mplbas2OLD  17557  ply1scl0  17747  ply1coeOLD  17752  uvcresum  18223  frlmsslsp  18228  frlmsslspOLD  18229  frlmup1  18231  frlmup2  18232  clm0vs  20667  plypf1  21685  lmodslmd  26225  lmod0rng  30784  scmsuppss  30790  lmodvsmdi  30817  lmodvsmmulgdi  30818  ascl0  30820  gsummoncoe1  30848  ply1mulgsumlem4  30852  pmatcollpw1lem4  30907  pmatcollpw2lem  30910  idpmattoidmply1  30920  mp2pm2mplem4  30924  pmattomply1mhmlem1  30933  lincval1  30958  lincvalsc0  30960  linc0scn0  30962  linc1  30964  ldepsprlem  31011  lshpkrlem1  32760  ldual0vs  32810  lclkrlem1  35156  lcd0vs  35265  baerlem3lem1  35357  baerlem5blem1  35359  hdmap14lem2a  35520  hdmap14lem4a  35524  hdmap14lem6  35526  hgmapval0  35545
  Copyright terms: Public domain W3C validator