Theorem xrsnsgrp

Description: The "additive group" of the extended reals is not a semigroup. (Contributed by AV, 30-Jan-2020)

	Ref	Expression
Assertion	xrsnsgrp	⊢ ℝ*𝑠 ∉ Smgrp

Proof

Step	Hyp	Ref	Expression
1		1xr	⊢ 1 ∈ ℝ*
2		mnfxr	⊢ -∞ ∈ ℝ*
3		pnfxr	⊢ +∞ ∈ ℝ*
4	1 2 3	3pm3.2i	⊢ ( 1 ∈ ℝ* ∧ -∞ ∈ ℝ* ∧ +∞ ∈ ℝ* )
5		xaddcom	⊢ ( ( 1 ∈ ℝ* ∧ -∞ ∈ ℝ* ) → ( 1 +𝑒 -∞ ) = ( -∞ +𝑒 1 ) )
6	1 2 5	mp2an	⊢ ( 1 +𝑒 -∞ ) = ( -∞ +𝑒 1 )
7		1re	⊢ 1 ∈ ℝ
8		renepnf	⊢ ( 1 ∈ ℝ → 1 ≠ +∞ )
9	7 8	ax-mp	⊢ 1 ≠ +∞
10		xaddmnf2	⊢ ( ( 1 ∈ ℝ* ∧ 1 ≠ +∞ ) → ( -∞ +𝑒 1 ) = -∞ )
11	1 9 10	mp2an	⊢ ( -∞ +𝑒 1 ) = -∞
12	6 11	eqtri	⊢ ( 1 +𝑒 -∞ ) = -∞
13	12	oveq1i	⊢ ( ( 1 +𝑒 -∞ ) +𝑒 +∞ ) = ( -∞ +𝑒 +∞ )
14		mnfaddpnf	⊢ ( -∞ +𝑒 +∞ ) = 0
15	13 14	eqtri	⊢ ( ( 1 +𝑒 -∞ ) +𝑒 +∞ ) = 0
16		0ne1	⊢ 0 ≠ 1
17	15 16	eqnetri	⊢ ( ( 1 +𝑒 -∞ ) +𝑒 +∞ ) ≠ 1
18	14	oveq2i	⊢ ( 1 +𝑒 ( -∞ +𝑒 +∞ ) ) = ( 1 +𝑒 0 )
19		xaddid1	⊢ ( 1 ∈ ℝ* → ( 1 +𝑒 0 ) = 1 )
20	1 19	ax-mp	⊢ ( 1 +𝑒 0 ) = 1
21	18 20	eqtri	⊢ ( 1 +𝑒 ( -∞ +𝑒 +∞ ) ) = 1
22	17 21	neeqtrri	⊢ ( ( 1 +𝑒 -∞ ) +𝑒 +∞ ) ≠ ( 1 +𝑒 ( -∞ +𝑒 +∞ ) )
23		xrsbas	⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
24		xrsadd	⊢ +𝑒 = ( +g ‘ ℝ*𝑠 )
25	23 24	isnsgrp	⊢ ( ( 1 ∈ ℝ* ∧ -∞ ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( ( 1 +𝑒 -∞ ) +𝑒 +∞ ) ≠ ( 1 +𝑒 ( -∞ +𝑒 +∞ ) ) → ℝ*𝑠 ∉ Smgrp ) )
26	4 22 25	mp2	⊢ ℝ*𝑠 ∉ Smgrp