Metamath Proof Explorer

Axiom ax-xrssca

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)

		Ref	Expression
	Assertion	ax-xrssca	⊢ ℝ_fld = ( Scalar ‘ ℝ^*_𝑠 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crefld	⊢ ℝ_fld
1		csca	⊢ Scalar
2		cxrs	⊢ ℝ^*_𝑠
3	2 1	cfv	⊢ ( Scalar ‘ ℝ^*_𝑠 )
4	0 3	wceq	⊢ ℝ_fld = ( Scalar ‘ ℝ^*_𝑠 )