Metamath Proof Explorer


Theorem xrsadd

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

Ref Expression
Assertion xrsadd +๐‘’ = ( +g โ€˜ โ„*๐‘  )

Proof

Step Hyp Ref Expression
1 xaddf โŠข +๐‘’ : ( โ„* ร— โ„* ) โŸถ โ„*
2 xrex โŠข โ„* โˆˆ V
3 2 2 xpex โŠข ( โ„* ร— โ„* ) โˆˆ V
4 fex2 โŠข ( ( +๐‘’ : ( โ„* ร— โ„* ) โŸถ โ„* โˆง ( โ„* ร— โ„* ) โˆˆ V โˆง โ„* โˆˆ V ) โ†’ +๐‘’ โˆˆ V )
5 1 3 2 4 mp3an โŠข +๐‘’ โˆˆ V
6 df-xrs โŠข โ„*๐‘  = ( { โŸจ ( Base โ€˜ ndx ) , โ„* โŸฉ , โŸจ ( +g โ€˜ ndx ) , +๐‘’ โŸฉ , โŸจ ( .r โ€˜ ndx ) , ยทe โŸฉ } โˆช { โŸจ ( TopSet โ€˜ ndx ) , ( ordTop โ€˜ โ‰ค ) โŸฉ , โŸจ ( le โ€˜ ndx ) , โ‰ค โŸฉ , โŸจ ( dist โ€˜ ndx ) , ( ๐‘ฅ โˆˆ โ„* , ๐‘ฆ โˆˆ โ„* โ†ฆ if ( ๐‘ฅ โ‰ค ๐‘ฆ , ( ๐‘ฆ +๐‘’ -๐‘’ ๐‘ฅ ) , ( ๐‘ฅ +๐‘’ -๐‘’ ๐‘ฆ ) ) ) โŸฉ } )
7 6 odrngplusg โŠข ( +๐‘’ โˆˆ V โ†’ +๐‘’ = ( +g โ€˜ โ„*๐‘  ) )
8 5 7 ax-mp โŠข +๐‘’ = ( +g โ€˜ โ„*๐‘  )