Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax-xrsvsca Structured version   Visualization version   Unicode version
Axiom ax-xrsvsca 29674
Description: Assume the scalar product of the extended real structure is the extended real number multiplication operation (this has to be defined in the main body of set.mm). (Contributed by Thierry Arnoux, 22-Oct-2017.)
Assertion
Ref Expression
ax-xrsvsca |- xe = ( .s ` RR*s )
Detailed syntax breakdown of Axiom ax-xrsvsca
StepHypRef Expression
1 cxmu 11945 . 2 class xe
2 cxrs 16160 . . 3 class RR*s
3 cvsca 15945 . . 3 class .s
42, 3cfv 5888 . 2 class ( .s ` RR*s )
51, 4wceq 1483 1 wff xe = ( .s ` RR*s )
Colors of variables: wff setvar class
This axiom is referenced by:  xrge0slmod  29844  sitmcl  30413
  Copyright terms: Public domain W3C validator