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 
|- ( CCfld |`s ( 0 [,) +oo ) ) e. SRing

Proof

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