Metamath Proof Explorer

Theorem rge0srg

Description: The nonnegative real numbers form a semiring (commutative by subcmn ). (Contributed by Thierry Arnoux, 6-Sep-2018)

Ref Expression
Assertion rge0srg ( ℂfld ↾s ( 0 [,) +∞ ) ) ∈ SRing

Proof

Step Hyp Ref Expression
1 cnring ⊢ ℂfld ∈ Ring
2 ringcmn ⊢ ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
3 1 2 ax-mp ⊢ ℂfld ∈ CMnd
4 rege0subm ⊢ ( 0 [,) +∞ ) ∈ ( SubMnd ‘ ℂfld )
5 eqid ⊢ ( ℂfld ↾s ( 0 [,) +∞ ) ) = ( ℂfld ↾s ( 0 [,) +∞ ) )
6 5 submcmn ⊢ ( ( ℂfld ∈ CMnd ∧ ( 0 [,) +∞ ) ∈ ( SubMnd ‘ ℂfld ) ) → ( ℂfld ↾s ( 0 [,) +∞ ) ) ∈ CMnd )
7 3 4 6 mp2an ⊢ ( ℂfld ↾s ( 0 [,) +∞ ) ) ∈ CMnd
8 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
9 ax-resscn ⊢ ℝ ⊆ ℂ
10 8 9 sstri ⊢ ( 0 [,) +∞ ) ⊆ ℂ
11 1re ⊢ 1 ∈ ℝ
12 0le1 ⊢ 0 ≤ 1
13 ltpnf ⊢ ( 1 ∈ ℝ → 1 < +∞ )
14 11 13 ax-mp ⊢ 1 < +∞
15 0re ⊢ 0 ∈ ℝ
16 pnfxr ⊢ +∞ ∈ ℝ*
17 elico2 ⊢ ( ( 0 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( 1 ∈ ( 0 [,) +∞ ) ↔ ( 1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 < +∞ ) ) )
18 15 16 17 mp2an ⊢ ( 1 ∈ ( 0 [,) +∞ ) ↔ ( 1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 < +∞ ) )
19 11 12 14 18 mpbir3an ⊢ 1 ∈ ( 0 [,) +∞ )
20 ge0mulcl ⊢ ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 · 𝑦 ) ∈ ( 0 [,) +∞ ) )
21 20 rgen2 ⊢ ∀ 𝑥 ∈ ( 0 [,) +∞ ) ∀ 𝑦 ∈ ( 0 [,) +∞ ) ( 𝑥 · 𝑦 ) ∈ ( 0 [,) +∞ )
22 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
23 22 ringmgp ⊢ ( ℂfld ∈ Ring → ( mulGrp ‘ ℂfld ) ∈ Mnd )
24 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
25 22 24 mgpbas ⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
26 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
27 22 26 ringidval ⊢ 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
28 cnfldmul ⊢ · = ( .r ‘ ℂfld )
29 22 28 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
30 25 27 29 issubm ⊢ ( ( mulGrp ‘ ℂfld ) ∈ Mnd → ( ( 0 [,) +∞ ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ↔ ( ( 0 [,) +∞ ) ⊆ ℂ ∧ 1 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑥 ∈ ( 0 [,) +∞ ) ∀ 𝑦 ∈ ( 0 [,) +∞ ) ( 𝑥 · 𝑦 ) ∈ ( 0 [,) +∞ ) ) ) )
31 1 23 30 mp2b ⊢ ( ( 0 [,) +∞ ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ↔ ( ( 0 [,) +∞ ) ⊆ ℂ ∧ 1 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑥 ∈ ( 0 [,) +∞ ) ∀ 𝑦 ∈ ( 0 [,) +∞ ) ( 𝑥 · 𝑦 ) ∈ ( 0 [,) +∞ ) ) )
32 10 19 21 31 mpbir3an ⊢ ( 0 [,) +∞ ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) )
33 eqid ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,) +∞ ) ) = ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,) +∞ ) )
34 33 submmnd ⊢ ( ( 0 [,) +∞ ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) → ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,) +∞ ) ) ∈ Mnd )
35 32 34 ax-mp ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,) +∞ ) ) ∈ Mnd
36 simpll ⊢ ( ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ∧ 𝑧 ∈ ( 0 [,) +∞ ) ) → 𝑥 ∈ ( 0 [,) +∞ ) )
37 10 36 sselid ⊢ ( ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ∧ 𝑧 ∈ ( 0 [,) +∞ ) ) → 𝑥 ∈ ℂ )
38 simplr ⊢ ( ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ∧ 𝑧 ∈ ( 0 [,) +∞ ) ) → 𝑦 ∈ ( 0 [,) +∞ ) )
39 10 38 sselid ⊢ ( ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ∧ 𝑧 ∈ ( 0 [,) +∞ ) ) → 𝑦 ∈ ℂ )
40 simpr ⊢ ( ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ∧ 𝑧 ∈ ( 0 [,) +∞ ) ) → 𝑧 ∈ ( 0 [,) +∞ ) )
41 10 40 sselid ⊢ ( ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ∧ 𝑧 ∈ ( 0 [,) +∞ ) ) → 𝑧 ∈ ℂ )
42 37 39 41 adddid ⊢ ( ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ∧ 𝑧 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
43 37 39 41 adddird ⊢ ( ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ∧ 𝑧 ∈ ( 0 [,) +∞ ) ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
44 42 43 jca ⊢ ( ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ∧ 𝑧 ∈ ( 0 [,) +∞ ) ) → ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) )
45 44 ralrimiva ⊢ ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ∀ 𝑧 ∈ ( 0 [,) +∞ ) ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) )
46 45 ralrimiva ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) → ∀ 𝑦 ∈ ( 0 [,) +∞ ) ∀ 𝑧 ∈ ( 0 [,) +∞ ) ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) )
47 10 sseli ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) → 𝑥 ∈ ℂ )
48 47 mul02d ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) → ( 0 · 𝑥 ) = 0 )
49 47 mul01d ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) → ( 𝑥 · 0 ) = 0 )
50 46 48 49 jca32 ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) → ( ∀ 𝑦 ∈ ( 0 [,) +∞ ) ∀ 𝑧 ∈ ( 0 [,) +∞ ) ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) ) )
51 50 rgen ⊢ ∀ 𝑥 ∈ ( 0 [,) +∞ ) ( ∀ 𝑦 ∈ ( 0 [,) +∞ ) ∀ 𝑧 ∈ ( 0 [,) +∞ ) ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) )
52 5 24 ressbas2 ⊢ ( ( 0 [,) +∞ ) ⊆ ℂ → ( 0 [,) +∞ ) = ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
53 10 52 ax-mp ⊢ ( 0 [,) +∞ ) = ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) )
54 cnfldex ⊢ ℂfld ∈ V
55 ovex ⊢ ( 0 [,) +∞ ) ∈ V
56 5 22 mgpress ⊢ ( ( ℂfld ∈ V ∧ ( 0 [,) +∞ ) ∈ V ) → ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,) +∞ ) ) = ( mulGrp ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
57 54 55 56 mp2an ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,) +∞ ) ) = ( mulGrp ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) )
58 cnfldadd ⊢ + = ( +g ‘ ℂfld )
59 5 58 ressplusg ⊢ ( ( 0 [,) +∞ ) ∈ V → + = ( +g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
60 55 59 ax-mp ⊢ + = ( +g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) )
61 5 28 ressmulr ⊢ ( ( 0 [,) +∞ ) ∈ V → · = ( .r ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
62 55 61 ax-mp ⊢ · = ( .r ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) )
63 ringmnd ⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
64 1 63 ax-mp ⊢ ℂfld ∈ Mnd
65 0e0icopnf ⊢ 0 ∈ ( 0 [,) +∞ )
66 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
67 5 24 66 ress0g ⊢ ( ( ℂfld ∈ Mnd ∧ 0 ∈ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℂ ) → 0 = ( 0g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
68 64 65 10 67 mp3an ⊢ 0 = ( 0g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) )
69 53 57 60 62 68 issrg ⊢ ( ( ℂfld ↾s ( 0 [,) +∞ ) ) ∈ SRing ↔ ( ( ℂfld ↾s ( 0 [,) +∞ ) ) ∈ CMnd ∧ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,) +∞ ) ) ∈ Mnd ∧ ∀ 𝑥 ∈ ( 0 [,) +∞ ) ( ∀ 𝑦 ∈ ( 0 [,) +∞ ) ∀ 𝑧 ∈ ( 0 [,) +∞ ) ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) ) ) )
70 7 35 51 69 mpbir3an ⊢ ( ℂfld ↾s ( 0 [,) +∞ ) ) ∈ SRing