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 30587
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 20676 . 2 class fld
2 cxrs 16761 . . 3 class *𝑠
3 csca 16556 . . 3 class Scalar
42, 3cfv 6348 . 2 class (Scalar‘ℝ*𝑠)
51, 4wceq 1528 1 wff fld = (Scalar‘ℝ*𝑠)
Colors of variables: wff setvar class
This axiom is referenced by:  xrge0slmod  30844  sitmcl  31508
  Copyright terms: Public domain W3C validator