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, +∞) \in SRing$

Proof

Step	Hyp	Ref	Expression
1		cnring	$⊢ ℂ_{fld} \in Ring$
2		ringcmn	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in CMnd$
3	1 2	ax-mp	$⊢ ℂ_{fld} \in CMnd$
4		rege0subm	$⊢ [0, +∞) \in SubMnd (ℂ_{fld})$
5		eqid	$⊢ ℂ_{fld} ↾_{𝑠} [0, +∞) = ℂ_{fld} ↾_{𝑠} [0, +∞)$
6	5	submcmn	$⊢ (ℂ_{fld} \in CMnd \land [0, +∞) \in SubMnd (ℂ_{fld})) \to ℂ_{fld} ↾_{𝑠} [0, +∞) \in CMnd$
7	3 4 6	mp2an	$⊢ ℂ_{fld} ↾_{𝑠} [0, +∞) \in CMnd$
8		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
9		ax-resscn	$⊢ ℝ \subseteq ℂ$
10	8 9	sstri	$⊢ [0, +∞) \subseteq ℂ$
11		1re	$⊢ 1 \in ℝ$
12		0le1	$⊢ 0 \leq 1$
13		ltpnf	$⊢ 1 \in ℝ \to 1 < +∞$
14	11 13	ax-mp	$⊢ 1 < +∞$
15		0re	$⊢ 0 \in ℝ$
16		pnfxr	$⊢ +∞ \in ℝ^{*}$
17		elico2	$⊢ (0 \in ℝ \land +∞ \in ℝ^{*}) \to (1 \in [0, +∞) \leftrightarrow (1 \in ℝ \land 0 \leq 1 \land 1 < +∞))$
18	15 16 17	mp2an	$⊢ 1 \in [0, +∞) \leftrightarrow (1 \in ℝ \land 0 \leq 1 \land 1 < +∞)$
19	11 12 14 18	mpbir3an	$⊢ 1 \in [0, +∞)$
20		ge0mulcl	$⊢ (x \in [0, +∞) \land y \in [0, +∞)) \to x y \in [0, +∞)$
21	20	rgen2	$⊢ \forall x \in [0, +∞) \forall y \in [0, +∞) x y \in [0, +∞)$
22		eqid	$⊢ {mulGrp}_{ℂ_{fld}} = {mulGrp}_{ℂ_{fld}}$
23	22	ringmgp	$⊢ ℂ_{fld} \in Ring \to {mulGrp}_{ℂ_{fld}} \in 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	$⊢ \times = \cdot_{ℂ_{fld}}$
29	22 28	mgpplusg	$⊢ \times = +_{{mulGrp}_{ℂ_{fld}}}$
30	25 27 29	issubm	$⊢ {mulGrp}_{ℂ_{fld}} \in Mnd \to ([0, +∞) \in SubMnd ({mulGrp}_{ℂ_{fld}}) \leftrightarrow ([0, +∞) \subseteq ℂ \land 1 \in [0, +∞) \land \forall x \in [0, +∞) \forall y \in [0, +∞) x y \in [0, +∞)))$
31	1 23 30	mp2b	$⊢ [0, +∞) \in SubMnd ({mulGrp}_{ℂ_{fld}}) \leftrightarrow ([0, +∞) \subseteq ℂ \land 1 \in [0, +∞) \land \forall x \in [0, +∞) \forall y \in [0, +∞) x y \in [0, +∞))$
32	10 19 21 31	mpbir3an	$⊢ [0, +∞) \in SubMnd ({mulGrp}_{ℂ_{fld}})$
33		eqid	$⊢ {mulGrp}_{ℂ_{fld}} ↾_{𝑠} [0, +∞) = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} [0, +∞)$
34	33	submmnd	$⊢ [0, +∞) \in SubMnd ({mulGrp}_{ℂ_{fld}}) \to {mulGrp}_{ℂ_{fld}} ↾_{𝑠} [0, +∞) \in Mnd$
35	32 34	ax-mp	$⊢ {mulGrp}_{ℂ_{fld}} ↾_{𝑠} [0, +∞) \in Mnd$
36		simpll	$⊢ ((x \in [0, +∞) \land y \in [0, +∞)) \land z \in [0, +∞)) \to x \in [0, +∞)$
37	10 36	sselid	$⊢ ((x \in [0, +∞) \land y \in [0, +∞)) \land z \in [0, +∞)) \to x \in ℂ$
38		simplr	$⊢ ((x \in [0, +∞) \land y \in [0, +∞)) \land z \in [0, +∞)) \to y \in [0, +∞)$
39	10 38	sselid	$⊢ ((x \in [0, +∞) \land y \in [0, +∞)) \land z \in [0, +∞)) \to y \in ℂ$
40		simpr	$⊢ ((x \in [0, +∞) \land y \in [0, +∞)) \land z \in [0, +∞)) \to z \in [0, +∞)$
41	10 40	sselid	$⊢ ((x \in [0, +∞) \land y \in [0, +∞)) \land z \in [0, +∞)) \to z \in ℂ$
42	37 39 41	adddid	$⊢ ((x \in [0, +∞) \land y \in [0, +∞)) \land z \in [0, +∞)) \to x (y + z) = x y + x z$
43	37 39 41	adddird	$⊢ ((x \in [0, +∞) \land y \in [0, +∞)) \land z \in [0, +∞)) \to (x + y) z = x z + y z$
44	42 43	jca	$⊢ ((x \in [0, +∞) \land y \in [0, +∞)) \land z \in [0, +∞)) \to (x (y + z) = x y + x z \land (x + y) z = x z + y z)$
45	44	ralrimiva	$⊢ (x \in [0, +∞) \land y \in [0, +∞)) \to \forall z \in [0, +∞) (x (y + z) = x y + x z \land (x + y) z = x z + y z)$
46	45	ralrimiva	$⊢ x \in [0, +∞) \to \forall y \in [0, +∞) \forall z \in [0, +∞) (x (y + z) = x y + x z \land (x + y) z = x z + y z)$
47	10	sseli	$⊢ x \in [0, +∞) \to x \in ℂ$
48	47	mul02d	$⊢ x \in [0, +∞) \to 0 \cdot x = 0$
49	47	mul01d	$⊢ x \in [0, +∞) \to x \cdot 0 = 0$
50	46 48 49	jca32	$⊢ x \in [0, +∞) \to (\forall y \in [0, +∞) \forall z \in [0, +∞) (x (y + z) = x y + x z \land (x + y) z = x z + y z) \land (0 \cdot x = 0 \land x \cdot 0 = 0))$
51	50	rgen	$⊢ \forall x \in [0, +∞) (\forall y \in [0, +∞) \forall z \in [0, +∞) (x (y + z) = x y + x z \land (x + y) z = x z + y z) \land (0 \cdot x = 0 \land x \cdot 0 = 0))$
52	5 24	ressbas2	$⊢ [0, +∞) \subseteq ℂ \to [0, +∞) = {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
53	10 52	ax-mp	$⊢ [0, +∞) = {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
54		cnfldex	$⊢ ℂ_{fld} \in V$
55		ovex	$⊢ [0, +∞) \in V$
56	5 22	mgpress	$⊢ (ℂ_{fld} \in V \land [0, +∞) \in V) \to {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, +∞) \in V \to + = +_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
60	55 59	ax-mp	$⊢ + = +_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
61	5 28	ressmulr	$⊢ [0, +∞) \in V \to \times = \cdot_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
62	55 61	ax-mp	$⊢ \times = \cdot_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
63		ringmnd	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in Mnd$
64	1 63	ax-mp	$⊢ ℂ_{fld} \in Mnd$
65		0e0icopnf	$⊢ 0 \in [0, +∞)$
66		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
67	5 24 66	ress0g	$⊢ (ℂ_{fld} \in Mnd \land 0 \in [0, +∞) \land [0, +∞) \subseteq ℂ) \to 0 = 0_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
68	64 65 10 67	mp3an	$⊢ 0 = 0_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
69	53 57 60 62 68	issrg	$⊢ ℂ_{fld} ↾_{𝑠} [0, +∞) \in SRing \leftrightarrow (ℂ_{fld} ↾_{𝑠} [0, +∞) \in CMnd \land {mulGrp}_{ℂ_{fld}} ↾_{𝑠} [0, +∞) \in Mnd \land \forall x \in [0, +∞) (\forall y \in [0, +∞) \forall z \in [0, +∞) (x (y + z) = x y + x z \land (x + y) z = x z + y z) \land (0 \cdot x = 0 \land x \cdot 0 = 0)))$
70	7 35 51 69	mpbir3an	$⊢ ℂ_{fld} ↾_{𝑠} [0, +∞) \in SRing$

Metamath Proof Explorer

Theorem rge0srg

Proof