Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax-xrsvsca Structured version   Visualization version   GIF version

Axiom ax-xrsvsca 31914
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 ยทe = ( ยท๐‘  โ€˜โ„*๐‘ )

Detailed syntax breakdown of Axiom ax-xrsvsca
StepHypRef Expression
1 cxmu 13037 . 2 class ยทe
2 cxrs 17387 . . 3 class โ„*๐‘ 
3 cvsca 17142 . . 3 class ยท๐‘ 
42, 3cfv 6497 . 2 class ( ยท๐‘  โ€˜โ„*๐‘ )
51, 4wceq 1542 1 wff ยทe = ( ยท๐‘  โ€˜โ„*๐‘ )
Colors of variables: wff setvar class
This axiom is referenced by:  xrge0slmod  32187  sitmcl  33008
  Copyright terms: Public domain W3C validator