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 29801
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 19998 . 2 class fld
2 cxrs 16207 . . 3 class *𝑠
3 csca 15991 . . 3 class Scalar
42, 3cfv 5926 . 2 class (Scalar‘ℝ*𝑠)
51, 4wceq 1523 1 wff fld = (Scalar‘ℝ*𝑠)
Colors of variables: wff setvar class
This axiom is referenced by:  xrge0slmod  29972  sitmcl  30541
  Copyright terms: Public domain W3C validator