xrsadd

Description: The addition operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015)

		Ref	Expression
	Assertion	xrsadd	$⊢ +_{𝑒} = +_{ℝ_{𝑠}^{*}}$

Step	Hyp	Ref	Expression
1		xaddf	$⊢ +_{𝑒} : ℝ^{} \times ℝ^{} ⟶ ℝ^{*}$
2		xrex	$⊢ ℝ^{*} \in V$
3	2 2	xpex	$⊢ ℝ^{} \times ℝ^{} \in V$
4		fex2	$⊢ (+_{𝑒} : ℝ^{} \times ℝ^{} ⟶ ℝ^{} \land ℝ^{} \times ℝ^{} \in V \land ℝ^{} \in V) \to +_{𝑒} \in V$
5	1 3 2 4	mp3an	$⊢ +_{𝑒} \in V$
6		df-xrs	$⊢ ℝ_{𝑠}^{} = \{⟨{Base}_{ndx}, ℝ^{}⟩, ⟨+_{ndx}, +_{𝑒}⟩, ⟨\cdot_{ndx}, \cdot_{𝑒}⟩\} \cup \{⟨TopSet (ndx), ordTop (\leq)⟩, ⟨\leq_{ndx} \leq⟩, ⟨dist (ndx), (x \in ℝ^{}, y \in ℝ^{} ⟼ if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)))⟩\}$
7	6	odrngplusg	$⊢ +_{𝑒} \in V \to +_{𝑒} = +_{ℝ_{𝑠}^{*}}$
8	5 7	ax-mp	$⊢ +_{𝑒} = +_{ℝ_{𝑠}^{*}}$

Metamath Proof Explorer