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 28811
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 19679 . 2 class fld
2 cxrs 15871 . . 3 class *𝑠
3 csca 15659 . . 3 class Scalar
42, 3cfv 5689 . 2 class (Scalar‘ℝ*𝑠)
51, 4wceq 1474 1 wff fld = (Scalar‘ℝ*𝑠)
Colors of variables: wff setvar class
This axiom is referenced by:  xrge0slmod  28982  sitmcl  29558
  Copyright terms: Public domain W3C validator