Theorem xrge0slmod

Description: The extended nonnegative real numbers form a semiring left module. One could also have used subringAlg to get the same structure. (Contributed by Thierry Arnoux, 6-Sep-2018)

	Ref	Expression
Hypotheses	xrge0slmod.1	⊢ 𝐺 = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
	xrge0slmod.2	⊢ 𝑊 = ( 𝐺 ↾v ( 0 [,) +∞ ) )
Assertion	xrge0slmod	⊢ 𝑊 ∈ SLMod

Proof

Step	Hyp	Ref	Expression
1		xrge0slmod.1	⊢ 𝐺 = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
2		xrge0slmod.2	⊢ 𝑊 = ( 𝐺 ↾v ( 0 [,) +∞ ) )
3		xrge0cmn	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
4	1 3	eqeltri	⊢ 𝐺 ∈ CMnd
5		ovex	⊢ ( 0 [,) +∞ ) ∈ V
6	2	resvcmn	⊢ ( ( 0 [,) +∞ ) ∈ V → ( 𝐺 ∈ CMnd ↔ 𝑊 ∈ CMnd ) )
7	5 6	ax-mp	⊢ ( 𝐺 ∈ CMnd ↔ 𝑊 ∈ CMnd )
8	4 7	mpbi	⊢ 𝑊 ∈ CMnd
9		rge0srg	⊢ ( ℂfld ↾s ( 0 [,) +∞ ) ) ∈ SRing
10		icossicc	⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
11		simplr	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑟 ∈ ( 0 [,) +∞ ) )
12	10 11	sselid	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑟 ∈ ( 0 [,] +∞ ) )
13		simprr	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑤 ∈ ( 0 [,] +∞ ) )
14		ge0xmulcl	⊢ ( ( 𝑟 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) → ( 𝑟 ·e 𝑤 ) ∈ ( 0 [,] +∞ ) )
15	12 13 14	syl2anc	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑟 ·e 𝑤 ) ∈ ( 0 [,] +∞ ) )
16		simprl	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑥 ∈ ( 0 [,] +∞ ) )
17		xrge0adddi	⊢ ( ( 𝑤 ∈ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑟 ∈ ( 0 [,] +∞ ) ) → ( 𝑟 ·e ( 𝑤 +𝑒 𝑥 ) ) = ( ( 𝑟 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑥 ) ) )
18	13 16 12 17	syl3anc	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑟 ·e ( 𝑤 +𝑒 𝑥 ) ) = ( ( 𝑟 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑥 ) ) )
19		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
20		simpll	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑞 ∈ ( 0 [,) +∞ ) )
21	19 20	sselid	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑞 ∈ ℝ )
22	19 11	sselid	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑟 ∈ ℝ )
23		rexadd	⊢ ( ( 𝑞 ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( 𝑞 +𝑒 𝑟 ) = ( 𝑞 + 𝑟 ) )
24	21 22 23	syl2anc	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑞 +𝑒 𝑟 ) = ( 𝑞 + 𝑟 ) )
25	24	oveq1d	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( ( 𝑞 +𝑒 𝑟 ) ·e 𝑤 ) = ( ( 𝑞 + 𝑟 ) ·e 𝑤 ) )
26	10 20	sselid	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑞 ∈ ( 0 [,] +∞ ) )
27		xrge0adddir	⊢ ( ( 𝑞 ∈ ( 0 [,] +∞ ) ∧ 𝑟 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) → ( ( 𝑞 +𝑒 𝑟 ) ·e 𝑤 ) = ( ( 𝑞 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑤 ) ) )
28	26 12 13 27	syl3anc	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( ( 𝑞 +𝑒 𝑟 ) ·e 𝑤 ) = ( ( 𝑞 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑤 ) ) )
29	25 28	eqtr3d	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( ( 𝑞 + 𝑟 ) ·e 𝑤 ) = ( ( 𝑞 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑤 ) ) )
30	15 18 29	3jca	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( ( 𝑟 ·e 𝑤 ) ∈ ( 0 [,] +∞ ) ∧ ( 𝑟 ·e ( 𝑤 +𝑒 𝑥 ) ) = ( ( 𝑟 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑥 ) ) ∧ ( ( 𝑞 + 𝑟 ) ·e 𝑤 ) = ( ( 𝑞 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑤 ) ) ) )
31		rexmul	⊢ ( ( 𝑞 ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( 𝑞 ·e 𝑟 ) = ( 𝑞 · 𝑟 ) )
32	21 22 31	syl2anc	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑞 ·e 𝑟 ) = ( 𝑞 · 𝑟 ) )
33	32	oveq1d	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( ( 𝑞 ·e 𝑟 ) ·e 𝑤 ) = ( ( 𝑞 · 𝑟 ) ·e 𝑤 ) )
34	21	rexrd	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑞 ∈ ℝ* )
35	22	rexrd	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑟 ∈ ℝ* )
36		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
37	36 13	sselid	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑤 ∈ ℝ* )
38		xmulass	⊢ ( ( 𝑞 ∈ ℝ* ∧ 𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( 𝑞 ·e 𝑟 ) ·e 𝑤 ) = ( 𝑞 ·e ( 𝑟 ·e 𝑤 ) ) )
39	34 35 37 38	syl3anc	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( ( 𝑞 ·e 𝑟 ) ·e 𝑤 ) = ( 𝑞 ·e ( 𝑟 ·e 𝑤 ) ) )
40	33 39	eqtr3d	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( ( 𝑞 · 𝑟 ) ·e 𝑤 ) = ( 𝑞 ·e ( 𝑟 ·e 𝑤 ) ) )
41		xmullid	⊢ ( 𝑤 ∈ ℝ* → ( 1 ·e 𝑤 ) = 𝑤 )
42	37 41	syl	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( 1 ·e 𝑤 ) = 𝑤 )
43		xmul02	⊢ ( 𝑤 ∈ ℝ* → ( 0 ·e 𝑤 ) = 0 )
44	37 43	syl	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( 0 ·e 𝑤 ) = 0 )
45	40 42 44	3jca	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( ( ( 𝑞 · 𝑟 ) ·e 𝑤 ) = ( 𝑞 ·e ( 𝑟 ·e 𝑤 ) ) ∧ ( 1 ·e 𝑤 ) = 𝑤 ∧ ( 0 ·e 𝑤 ) = 0 ) )
46	30 45	jca	⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( ( ( 𝑟 ·e 𝑤 ) ∈ ( 0 [,] +∞ ) ∧ ( 𝑟 ·e ( 𝑤 +𝑒 𝑥 ) ) = ( ( 𝑟 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑥 ) ) ∧ ( ( 𝑞 + 𝑟 ) ·e 𝑤 ) = ( ( 𝑞 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑤 ) ) ) ∧ ( ( ( 𝑞 · 𝑟 ) ·e 𝑤 ) = ( 𝑞 ·e ( 𝑟 ·e 𝑤 ) ) ∧ ( 1 ·e 𝑤 ) = 𝑤 ∧ ( 0 ·e 𝑤 ) = 0 ) ) )
47	46	ralrimivva	⊢ ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) → ∀ 𝑥 ∈ ( 0 [,] +∞ ) ∀ 𝑤 ∈ ( 0 [,] +∞ ) ( ( ( 𝑟 ·e 𝑤 ) ∈ ( 0 [,] +∞ ) ∧ ( 𝑟 ·e ( 𝑤 +𝑒 𝑥 ) ) = ( ( 𝑟 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑥 ) ) ∧ ( ( 𝑞 + 𝑟 ) ·e 𝑤 ) = ( ( 𝑞 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑤 ) ) ) ∧ ( ( ( 𝑞 · 𝑟 ) ·e 𝑤 ) = ( 𝑞 ·e ( 𝑟 ·e 𝑤 ) ) ∧ ( 1 ·e 𝑤 ) = 𝑤 ∧ ( 0 ·e 𝑤 ) = 0 ) ) )
48	47	rgen2	⊢ ∀ 𝑞 ∈ ( 0 [,) +∞ ) ∀ 𝑟 ∈ ( 0 [,) +∞ ) ∀ 𝑥 ∈ ( 0 [,] +∞ ) ∀ 𝑤 ∈ ( 0 [,] +∞ ) ( ( ( 𝑟 ·e 𝑤 ) ∈ ( 0 [,] +∞ ) ∧ ( 𝑟 ·e ( 𝑤 +𝑒 𝑥 ) ) = ( ( 𝑟 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑥 ) ) ∧ ( ( 𝑞 + 𝑟 ) ·e 𝑤 ) = ( ( 𝑞 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑤 ) ) ) ∧ ( ( ( 𝑞 · 𝑟 ) ·e 𝑤 ) = ( 𝑞 ·e ( 𝑟 ·e 𝑤 ) ) ∧ ( 1 ·e 𝑤 ) = 𝑤 ∧ ( 0 ·e 𝑤 ) = 0 ) )
49		xrge0base	⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
50	1	fveq2i	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
51	49 50	eqtr4i	⊢ ( 0 [,] +∞ ) = ( Base ‘ 𝐺 )
52	2 51	resvbas	⊢ ( ( 0 [,) +∞ ) ∈ V → ( 0 [,] +∞ ) = ( Base ‘ 𝑊 ) )
53	5 52	ax-mp	⊢ ( 0 [,] +∞ ) = ( Base ‘ 𝑊 )
54		xrge0plusg	⊢ +𝑒 = ( +g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
55	1	fveq2i	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
56	54 55	eqtr4i	⊢ +𝑒 = ( +g ‘ 𝐺 )
57	2 56	resvplusg	⊢ ( ( 0 [,) +∞ ) ∈ V → +𝑒 = ( +g ‘ 𝑊 ) )
58	5 57	ax-mp	⊢ +𝑒 = ( +g ‘ 𝑊 )
59		ovex	⊢ ( 0 [,] +∞ ) ∈ V
60		ax-xrsvsca	⊢ ·e = ( ·𝑠 ‘ ℝ*𝑠 )
61	1 60	ressvsca	⊢ ( ( 0 [,] +∞ ) ∈ V → ·e = ( ·𝑠 ‘ 𝐺 ) )
62	59 61	ax-mp	⊢ ·e = ( ·𝑠 ‘ 𝐺 )
63	2 62	resvvsca	⊢ ( ( 0 [,) +∞ ) ∈ V → ·e = ( ·𝑠 ‘ 𝑊 ) )
64	5 63	ax-mp	⊢ ·e = ( ·𝑠 ‘ 𝑊 )
65		xrge00	⊢ 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
66	1	fveq2i	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
67	65 66	eqtr4i	⊢ 0 = ( 0g ‘ 𝐺 )
68	2 67	resv0g	⊢ ( ( 0 [,) +∞ ) ∈ V → 0 = ( 0g ‘ 𝑊 ) )
69	5 68	ax-mp	⊢ 0 = ( 0g ‘ 𝑊 )
70		df-refld	⊢ ℝfld = ( ℂfld ↾s ℝ )
71	70	oveq1i	⊢ ( ℝfld ↾s ( 0 [,) +∞ ) ) = ( ( ℂfld ↾s ℝ ) ↾s ( 0 [,) +∞ ) )
72		reex	⊢ ℝ ∈ V
73		ressress	⊢ ( ( ℝ ∈ V ∧ ( 0 [,) +∞ ) ∈ V ) → ( ( ℂfld ↾s ℝ ) ↾s ( 0 [,) +∞ ) ) = ( ℂfld ↾s ( ℝ ∩ ( 0 [,) +∞ ) ) ) )
74	72 5 73	mp2an	⊢ ( ( ℂfld ↾s ℝ ) ↾s ( 0 [,) +∞ ) ) = ( ℂfld ↾s ( ℝ ∩ ( 0 [,) +∞ ) ) )
75	71 74	eqtri	⊢ ( ℝfld ↾s ( 0 [,) +∞ ) ) = ( ℂfld ↾s ( ℝ ∩ ( 0 [,) +∞ ) ) )
76		ax-xrssca	⊢ ℝfld = ( Scalar ‘ ℝ*𝑠 )
77	1 76	resssca	⊢ ( ( 0 [,] +∞ ) ∈ V → ℝfld = ( Scalar ‘ 𝐺 ) )
78	59 77	ax-mp	⊢ ℝfld = ( Scalar ‘ 𝐺 )
79		rebase	⊢ ℝ = ( Base ‘ ℝfld )
80	2 78 79	resvsca	⊢ ( ( 0 [,) +∞ ) ∈ V → ( ℝfld ↾s ( 0 [,) +∞ ) ) = ( Scalar ‘ 𝑊 ) )
81	5 80	ax-mp	⊢ ( ℝfld ↾s ( 0 [,) +∞ ) ) = ( Scalar ‘ 𝑊 )
82		incom	⊢ ( ( 0 [,) +∞ ) ∩ ℝ ) = ( ℝ ∩ ( 0 [,) +∞ ) )
83		df-ss	⊢ ( ( 0 [,) +∞ ) ⊆ ℝ ↔ ( ( 0 [,) +∞ ) ∩ ℝ ) = ( 0 [,) +∞ ) )
84	19 83	mpbi	⊢ ( ( 0 [,) +∞ ) ∩ ℝ ) = ( 0 [,) +∞ )
85	82 84	eqtr3i	⊢ ( ℝ ∩ ( 0 [,) +∞ ) ) = ( 0 [,) +∞ )
86	85	oveq2i	⊢ ( ℂfld ↾s ( ℝ ∩ ( 0 [,) +∞ ) ) ) = ( ℂfld ↾s ( 0 [,) +∞ ) )
87	75 81 86	3eqtr3ri	⊢ ( ℂfld ↾s ( 0 [,) +∞ ) ) = ( Scalar ‘ 𝑊 )
88		ax-resscn	⊢ ℝ ⊆ ℂ
89	19 88	sstri	⊢ ( 0 [,) +∞ ) ⊆ ℂ
90		eqid	⊢ ( ℂfld ↾s ( 0 [,) +∞ ) ) = ( ℂfld ↾s ( 0 [,) +∞ ) )
91		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
92	90 91	ressbas2	⊢ ( ( 0 [,) +∞ ) ⊆ ℂ → ( 0 [,) +∞ ) = ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
93	89 92	ax-mp	⊢ ( 0 [,) +∞ ) = ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) )
94		cnfldadd	⊢ + = ( +g ‘ ℂfld )
95	90 94	ressplusg	⊢ ( ( 0 [,) +∞ ) ∈ V → + = ( +g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
96	5 95	ax-mp	⊢ + = ( +g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) )
97		cnfldmul	⊢ · = ( .r ‘ ℂfld )
98	90 97	ressmulr	⊢ ( ( 0 [,) +∞ ) ∈ V → · = ( .r ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
99	5 98	ax-mp	⊢ · = ( .r ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) )
100		cndrng	⊢ ℂfld ∈ DivRing
101		drngring	⊢ ( ℂfld ∈ DivRing → ℂfld ∈ Ring )
102	100 101	ax-mp	⊢ ℂfld ∈ Ring
103		1re	⊢ 1 ∈ ℝ
104		0le1	⊢ 0 ≤ 1
105		ltpnf	⊢ ( 1 ∈ ℝ → 1 < +∞ )
106	103 105	ax-mp	⊢ 1 < +∞
107	103 104 106	3pm3.2i	⊢ ( 1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 < +∞ )
108		0re	⊢ 0 ∈ ℝ
109		pnfxr	⊢ +∞ ∈ ℝ*
110		elico2	⊢ ( ( 0 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( 1 ∈ ( 0 [,) +∞ ) ↔ ( 1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 < +∞ ) ) )
111	108 109 110	mp2an	⊢ ( 1 ∈ ( 0 [,) +∞ ) ↔ ( 1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 < +∞ ) )
112	107 111	mpbir	⊢ 1 ∈ ( 0 [,) +∞ )
113		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
114	90 91 113	ress1r	⊢ ( ( ℂfld ∈ Ring ∧ 1 ∈ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℂ ) → 1 = ( 1r ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
115	102 112 89 114	mp3an	⊢ 1 = ( 1r ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) )
116		ringmnd	⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
117	100 101 116	mp2b	⊢ ℂfld ∈ Mnd
118		0e0icopnf	⊢ 0 ∈ ( 0 [,) +∞ )
119		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
120	90 91 119	ress0g	⊢ ( ( ℂfld ∈ Mnd ∧ 0 ∈ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℂ ) → 0 = ( 0g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
121	117 118 89 120	mp3an	⊢ 0 = ( 0g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) )
122	53 58 64 69 87 93 96 99 115 121	isslmd	⊢ ( 𝑊 ∈ SLMod ↔ ( 𝑊 ∈ CMnd ∧ ( ℂfld ↾s ( 0 [,) +∞ ) ) ∈ SRing ∧ ∀ 𝑞 ∈ ( 0 [,) +∞ ) ∀ 𝑟 ∈ ( 0 [,) +∞ ) ∀ 𝑥 ∈ ( 0 [,] +∞ ) ∀ 𝑤 ∈ ( 0 [,] +∞ ) ( ( ( 𝑟 ·e 𝑤 ) ∈ ( 0 [,] +∞ ) ∧ ( 𝑟 ·e ( 𝑤 +𝑒 𝑥 ) ) = ( ( 𝑟 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑥 ) ) ∧ ( ( 𝑞 + 𝑟 ) ·e 𝑤 ) = ( ( 𝑞 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑤 ) ) ) ∧ ( ( ( 𝑞 · 𝑟 ) ·e 𝑤 ) = ( 𝑞 ·e ( 𝑟 ·e 𝑤 ) ) ∧ ( 1 ·e 𝑤 ) = 𝑤 ∧ ( 0 ·e 𝑤 ) = 0 ) ) ) )
123	8 9 48 122	mpbir3an	⊢ 𝑊 ∈ SLMod