Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  slmdvscl Structured version   Unicode version

Theorem slmdvscl 27407
 Description: Closure of scalar product for a semiring left module. (hvmulcl 25594 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.)
Hypotheses
Ref Expression
slmdvscl.v
slmdvscl.f Scalar
slmdvscl.s
slmdvscl.k
Assertion
Ref Expression
slmdvscl SLMod

Proof of Theorem slmdvscl
StepHypRef Expression
1 biid 236 . 2 SLMod SLMod
2 pm4.24 643 . 2
3 pm4.24 643 . 2
4 slmdvscl.v . . . . 5
5 eqid 2462 . . . . 5
6 slmdvscl.s . . . . 5
7 eqid 2462 . . . . 5
8 slmdvscl.f . . . . 5 Scalar
9 slmdvscl.k . . . . 5
10 eqid 2462 . . . . 5
11 eqid 2462 . . . . 5
12 eqid 2462 . . . . 5
13 eqid 2462 . . . . 5
144, 5, 6, 7, 8, 9, 10, 11, 12, 13slmdlema 27396 . . . 4 SLMod
1514simpld 459 . . 3 SLMod
1615simp1d 1003 . 2 SLMod
171, 2, 3, 16syl3anb 1266 1 SLMod
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   w3a 968   wceq 1374   wcel 1762  cfv 5581  (class class class)co 6277  cbs 14481   cplusg 14546  cmulr 14547  Scalarcsca 14549  cvsca 14550  c0g 14686  cur 16938  SLModcslmd 27393 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-nul 4571 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2274  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-ral 2814  df-rex 2815  df-rab 2818  df-v 3110  df-sbc 3327  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-uni 4241  df-br 4443  df-iota 5544  df-fv 5589  df-ov 6280  df-slmd 27394 This theorem is referenced by:  gsumvsca1  27424  gsumvsca2  27425
 Copyright terms: Public domain W3C validator