Theorem xrsadd

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

	Ref	Expression
Assertion	xrsadd	⊢ +e = ( +g ‘ ℝ*𝑠 )

Proof

Step	Hyp	Ref	Expression
1		xaddf	⊢ +e : ( ℝ* × ℝ* ) ⟶ ℝ*
2		xrex	⊢ ℝ* ∈ V
3	2 2	xpex	⊢ ( ℝ* × ℝ* ) ∈ V
4		fex2	⊢ ( ( +e : ( ℝ* × ℝ* ) ⟶ ℝ* ∧ ( ℝ* × ℝ* ) ∈ V ∧ ℝ* ∈ V ) → +e ∈ V )
5	1 3 2 4	mp3an	⊢ +e ∈ V
6		df-xrs	⊢ ℝ*𝑠 = ( { ⟨ ( Base ‘ ndx ) , ℝ* ⟩ , ⟨ ( +g ‘ ndx ) , +e ⟩ , ⟨ ( .r ‘ ndx ) , ·e ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +e -e 𝑥 ) , ( 𝑥 +e -e 𝑦 ) ) ) ⟩ } )
7	6	odrngplusg	⊢ ( +e ∈ V → +e = ( +g ‘ ℝ*𝑠 ) )
8	5 7	ax-mp	⊢ +e = ( +g ‘ ℝ*𝑠 )