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

Axiom ax-xrssca 31913
Description: Assume the scalar component of the extended real structure is the field of the real numbers (this has to be defined in the main body of set.mm). (Contributed by Thierry Arnoux, 22-Oct-2017.)
Assertion
Ref Expression
ax-xrssca fld = (Scalar‘ℝ*𝑠)

Detailed syntax breakdown of Axiom ax-xrssca
StepHypRef Expression
1 crefld 21024 . 2 class fld
2 cxrs 17387 . . 3 class *𝑠
3 csca 17141 . . 3 class Scalar
42, 3cfv 6497 . 2 class (Scalar‘ℝ*𝑠)
51, 4wceq 1542 1 wff fld = (Scalar‘ℝ*𝑠)
Colors of variables: wff setvar class
This axiom is referenced by:  xrge0slmod  32187  sitmcl  33008
  Copyright terms: Public domain W3C validator