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 ↾ 𝑠 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 ↾ 𝑠 0 +∞ = ℂ fld ↾ 𝑠 0 +∞
6 5 submcmn ⊢ ℂ fld ∈ CMnd ∧ 0 +∞ ∈ SubMnd ⁡ ℂ fld → ℂ fld ↾ 𝑠 0 +∞ ∈ CMnd
7 3 4 6 mp2an ⊢ ℂ fld ↾ 𝑠 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 ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x ⁢ y ∈ 0 +∞
21 20 rgen2 ⊢ ∀ x ∈ 0 +∞ ∀ y ∈ 0 +∞ x ⁢ y ∈ 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 = 1 ℂ fld
27 22 26 ringidval ⊢ 1 = 0 mulGrp ℂ fld
28 cnfldmul ⊢ × = ⋅ ℂ fld
29 22 28 mgpplusg ⊢ × = + mulGrp ℂ fld
30 25 27 29 issubm ⊢ mulGrp ℂ fld ∈ Mnd → 0 +∞ ∈ SubMnd ⁡ mulGrp ℂ fld ↔ 0 +∞ ⊆ ℂ ∧ 1 ∈ 0 +∞ ∧ ∀ x ∈ 0 +∞ ∀ y ∈ 0 +∞ x ⁢ y ∈ 0 +∞
31 1 23 30 mp2b ⊢ 0 +∞ ∈ SubMnd ⁡ mulGrp ℂ fld ↔ 0 +∞ ⊆ ℂ ∧ 1 ∈ 0 +∞ ∧ ∀ x ∈ 0 +∞ ∀ y ∈ 0 +∞ x ⁢ y ∈ 0 +∞
32 10 19 21 31 mpbir3an ⊢ 0 +∞ ∈ SubMnd ⁡ mulGrp ℂ fld
33 eqid ⊢ mulGrp ℂ fld ↾ 𝑠 0 +∞ = mulGrp ℂ fld ↾ 𝑠 0 +∞
34 33 submmnd ⊢ 0 +∞ ∈ SubMnd ⁡ mulGrp ℂ fld → mulGrp ℂ fld ↾ 𝑠 0 +∞ ∈ Mnd
35 32 34 ax-mp ⊢ mulGrp ℂ fld ↾ 𝑠 0 +∞ ∈ Mnd
36 simpll ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ ∧ z ∈ 0 +∞ → x ∈ 0 +∞
37 10 36 sselid ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ ∧ z ∈ 0 +∞ → x ∈ ℂ
38 simplr ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ ∧ z ∈ 0 +∞ → y ∈ 0 +∞
39 10 38 sselid ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ ∧ z ∈ 0 +∞ → y ∈ ℂ
40 simpr ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ ∧ z ∈ 0 +∞ → z ∈ 0 +∞
41 10 40 sselid ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ ∧ z ∈ 0 +∞ → z ∈ ℂ
42 37 39 41 adddid ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ ∧ z ∈ 0 +∞ → x ⁢ y + z = x ⁢ y + x ⁢ z
43 37 39 41 adddird ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ ∧ z ∈ 0 +∞ → x + y ⁢ z = x ⁢ z + y ⁢ z
44 42 43 jca ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ ∧ z ∈ 0 +∞ → x ⁢ y + z = x ⁢ y + x ⁢ z ∧ x + y ⁢ z = x ⁢ z + y ⁢ z
45 44 ralrimiva ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → ∀ z ∈ 0 +∞ x ⁢ y + z = x ⁢ y + x ⁢ z ∧ x + y ⁢ z = x ⁢ z + y ⁢ z
46 45 ralrimiva ⊢ x ∈ 0 +∞ → ∀ y ∈ 0 +∞ ∀ z ∈ 0 +∞ x ⁢ y + z = x ⁢ y + x ⁢ z ∧ x + y ⁢ z = x ⁢ z + y ⁢ z
47 10 sseli ⊢ x ∈ 0 +∞ → x ∈ ℂ
48 47 mul02d ⊢ x ∈ 0 +∞ → 0 ⋅ x = 0
49 47 mul01d ⊢ x ∈ 0 +∞ → x ⋅ 0 = 0
50 46 48 49 jca32 ⊢ x ∈ 0 +∞ → ∀ y ∈ 0 +∞ ∀ z ∈ 0 +∞ x ⁢ y + z = x ⁢ y + x ⁢ z ∧ x + y ⁢ z = x ⁢ z + y ⁢ z ∧ 0 ⋅ x = 0 ∧ x ⋅ 0 = 0
51 50 rgen ⊢ ∀ x ∈ 0 +∞ ∀ y ∈ 0 +∞ ∀ z ∈ 0 +∞ x ⁢ y + z = x ⁢ y + x ⁢ z ∧ x + y ⁢ z = x ⁢ z + y ⁢ z ∧ 0 ⋅ x = 0 ∧ x ⋅ 0 = 0
52 5 24 ressbas2 ⊢ 0 +∞ ⊆ ℂ → 0 +∞ = Base ℂ fld ↾ 𝑠 0 +∞
53 10 52 ax-mp ⊢ 0 +∞ = Base ℂ fld ↾ 𝑠 0 +∞
54 cnfldex ⊢ ℂ fld ∈ V
55 ovex ⊢ 0 +∞ ∈ V
56 5 22 mgpress ⊢ ℂ fld ∈ V ∧ 0 +∞ ∈ V → mulGrp ℂ fld ↾ 𝑠 0 +∞ = mulGrp ℂ fld ↾ 𝑠 0 +∞
57 54 55 56 mp2an ⊢ mulGrp ℂ fld ↾ 𝑠 0 +∞ = mulGrp ℂ fld ↾ 𝑠 0 +∞
58 cnfldadd ⊢ + = + ℂ fld
59 5 58 ressplusg ⊢ 0 +∞ ∈ V → + = + ℂ fld ↾ 𝑠 0 +∞
60 55 59 ax-mp ⊢ + = + ℂ fld ↾ 𝑠 0 +∞
61 5 28 ressmulr ⊢ 0 +∞ ∈ V → × = ⋅ ℂ fld ↾ 𝑠 0 +∞
62 55 61 ax-mp ⊢ × = ⋅ ℂ fld ↾ 𝑠 0 +∞
63 ringmnd ⊢ ℂ fld ∈ Ring → ℂ fld ∈ Mnd
64 1 63 ax-mp ⊢ ℂ fld ∈ Mnd
65 0e0icopnf ⊢ 0 ∈ 0 +∞
66 cnfld0 ⊢ 0 = 0 ℂ fld
67 5 24 66 ress0g ⊢ ℂ fld ∈ Mnd ∧ 0 ∈ 0 +∞ ∧ 0 +∞ ⊆ ℂ → 0 = 0 ℂ fld ↾ 𝑠 0 +∞
68 64 65 10 67 mp3an ⊢ 0 = 0 ℂ fld ↾ 𝑠 0 +∞
69 53 57 60 62 68 issrg ⊢ ℂ fld ↾ 𝑠 0 +∞ ∈ SRing ↔ ℂ fld ↾ 𝑠 0 +∞ ∈ CMnd ∧ mulGrp ℂ fld ↾ 𝑠 0 +∞ ∈ Mnd ∧ ∀ x ∈ 0 +∞ ∀ y ∈ 0 +∞ ∀ z ∈ 0 +∞ x ⁢ y + z = x ⁢ y + x ⁢ z ∧ x + y ⁢ z = x ⁢ z + y ⁢ z ∧ 0 ⋅ x = 0 ∧ x ⋅ 0 = 0
70 7 35 51 69 mpbir3an ⊢ ℂ fld ↾ 𝑠 0 +∞ ∈ SRing