xrge0iifhom

Description: The defined function from the closed unit interval to the extended nonnegative reals is a monoid homomorphism. (Contributed by Thierry Arnoux, 5-Apr-2017)

	Ref	Expression
Hypotheses	xrge0iifhmeo.1	$⊢ F = (x \in [0, 1] ⟼ if (x = 0, +∞, - \log x))$
	xrge0iifhmeo.k	$⊢ J = ordTop (\leq) ↾_{𝑡} [0, +∞]$
Assertion	xrge0iifhom	$⊢ (X \in [0, 1] \land Y \in [0, 1]) \to F (X Y) = F (X) +_{𝑒} F (Y)$

Proof

Step	Hyp	Ref	Expression
1		xrge0iifhmeo.1	$⊢ F = (x \in [0, 1] ⟼ if (x = 0, +∞, - \log x))$
2		xrge0iifhmeo.k	$⊢ J = ordTop (\leq) ↾_{𝑡} [0, +∞]$
3		0xr	$⊢ 0 \in ℝ^{*}$
4		1xr	$⊢ 1 \in ℝ^{*}$
5		0le1	$⊢ 0 \leq 1$
6		snunioc	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{} \land 0 \leq 1) \to \{0\} \cup (0, 1] = [0, 1]$
7	3 4 5 6	mp3an	$⊢ \{0\} \cup (0, 1] = [0, 1]$
8	7	eleq2i	$⊢ Y \in (\{0\} \cup (0, 1]) \leftrightarrow Y \in [0, 1]$
9		elun	$⊢ Y \in (\{0\} \cup (0, 1]) \leftrightarrow (Y \in \{0\} \lor Y \in (0, 1])$
10	8 9	bitr3i	$⊢ Y \in [0, 1] \leftrightarrow (Y \in \{0\} \lor Y \in (0, 1])$
11		elsni	$⊢ Y \in \{0\} \to Y = 0$
12	11	orim1i	$⊢ (Y \in \{0\} \lor Y \in (0, 1]) \to (Y = 0 \lor Y \in (0, 1])$
13	10 12	sylbi	$⊢ Y \in [0, 1] \to (Y = 0 \lor Y \in (0, 1])$
14		0elunit	$⊢ 0 \in [0, 1]$
15		iftrue	$⊢ x = 0 \to if (x = 0, +∞, - \log x) = +∞$
16		pnfex	$⊢ +∞ \in V$
17	15 1 16	fvmpt	$⊢ 0 \in [0, 1] \to F (0) = +∞$
18	14 17	ax-mp	$⊢ F (0) = +∞$
19	18	oveq2i	$⊢ F (X) +_{𝑒} F (0) = F (X) +_{𝑒} +∞$
20		eqeq1	$⊢ x = X \to (x = 0 \leftrightarrow X = 0)$
21		fveq2	$⊢ x = X \to \log x = \log X$
22	21	negeqd	$⊢ x = X \to - \log x = - \log X$
23	20 22	ifbieq2d	$⊢ x = X \to if (x = 0, +∞, - \log x) = if (X = 0, +∞, - \log X)$
24		negex	$⊢ - \log X \in V$
25	16 24	ifex	$⊢ if (X = 0, +∞, - \log X) \in V$
26	23 1 25	fvmpt	$⊢ X \in [0, 1] \to F (X) = if (X = 0, +∞, - \log X)$
27		pnfxr	$⊢ +∞ \in ℝ^{*}$
28	27	a1i	$⊢ (X \in [0, 1] \land X = 0) \to +∞ \in ℝ^{*}$
29		elunitrn	$⊢ X \in [0, 1] \to X \in ℝ$
30	29	adantr	$⊢ (X \in [0, 1] \land \neg X = 0) \to X \in ℝ$
31		elunitge0	$⊢ X \in [0, 1] \to 0 \leq X$
32	31	adantr	$⊢ (X \in [0, 1] \land \neg X = 0) \to 0 \leq X$
33		simpr	$⊢ (X \in [0, 1] \land \neg X = 0) \to \neg X = 0$
34	33	neqned	$⊢ (X \in [0, 1] \land \neg X = 0) \to X \neq 0$
35	30 32 34	ne0gt0d	$⊢ (X \in [0, 1] \land \neg X = 0) \to 0 < X$
36	30 35	elrpd	$⊢ (X \in [0, 1] \land \neg X = 0) \to X \in ℝ^{+}$
37	36	relogcld	$⊢ (X \in [0, 1] \land \neg X = 0) \to \log X \in ℝ$
38	37	renegcld	$⊢ (X \in [0, 1] \land \neg X = 0) \to - \log X \in ℝ$
39	38	rexrd	$⊢ (X \in [0, 1] \land \neg X = 0) \to - \log X \in ℝ^{*}$
40	28 39	ifclda	$⊢ X \in [0, 1] \to if (X = 0, +∞, - \log X) \in ℝ^{*}$
41	26 40	eqeltrd	$⊢ X \in [0, 1] \to F (X) \in ℝ^{*}$
42	41	adantr	$⊢ (X \in [0, 1] \land Y = 0) \to F (X) \in ℝ^{*}$
43		neeq1	$⊢ +∞ = if (X = 0, +∞, - \log X) \to (+∞ \neq −∞ \leftrightarrow if (X = 0, +∞, - \log X) \neq −∞)$
44		neeq1	$⊢ - \log X = if (X = 0, +∞, - \log X) \to (- \log X \neq −∞ \leftrightarrow if (X = 0, +∞, - \log X) \neq −∞)$
45		pnfnemnf	$⊢ +∞ \neq −∞$
46	45	a1i	$⊢ (X \in [0, 1] \land X = 0) \to +∞ \neq −∞$
47	38	renemnfd	$⊢ (X \in [0, 1] \land \neg X = 0) \to - \log X \neq −∞$
48	43 44 46 47	ifbothda	$⊢ X \in [0, 1] \to if (X = 0, +∞, - \log X) \neq −∞$
49	26 48	eqnetrd	$⊢ X \in [0, 1] \to F (X) \neq −∞$
50	49	adantr	$⊢ (X \in [0, 1] \land Y = 0) \to F (X) \neq −∞$
51		xaddpnf1	$⊢ (F (X) \in ℝ^{*} \land F (X) \neq −∞) \to F (X) +_{𝑒} +∞ = +∞$
52	42 50 51	syl2anc	$⊢ (X \in [0, 1] \land Y = 0) \to F (X) +_{𝑒} +∞ = +∞$
53	19 52	syl5eq	$⊢ (X \in [0, 1] \land Y = 0) \to F (X) +_{𝑒} F (0) = +∞$
54		unitsscn	$⊢ [0, 1] \subseteq ℂ$
55		simpl	$⊢ (X \in [0, 1] \land Y = 0) \to X \in [0, 1]$
56	54 55	sselid	$⊢ (X \in [0, 1] \land Y = 0) \to X \in ℂ$
57	56	mul01d	$⊢ (X \in [0, 1] \land Y = 0) \to X \cdot 0 = 0$
58	57	fveq2d	$⊢ (X \in [0, 1] \land Y = 0) \to F (X \cdot 0) = F (0)$
59	58 18	eqtrdi	$⊢ (X \in [0, 1] \land Y = 0) \to F (X \cdot 0) = +∞$
60	53 59	eqtr4d	$⊢ (X \in [0, 1] \land Y = 0) \to F (X) +_{𝑒} F (0) = F (X \cdot 0)$
61		simpr	$⊢ (X \in [0, 1] \land Y = 0) \to Y = 0$
62	61	fveq2d	$⊢ (X \in [0, 1] \land Y = 0) \to F (Y) = F (0)$
63	62	oveq2d	$⊢ (X \in [0, 1] \land Y = 0) \to F (X) +_{𝑒} F (Y) = F (X) +_{𝑒} F (0)$
64	61	oveq2d	$⊢ (X \in [0, 1] \land Y = 0) \to X Y = X \cdot 0$
65	64	fveq2d	$⊢ (X \in [0, 1] \land Y = 0) \to F (X Y) = F (X \cdot 0)$
66	60 63 65	3eqtr4rd	$⊢ (X \in [0, 1] \land Y = 0) \to F (X Y) = F (X) +_{𝑒} F (Y)$
67	7	eleq2i	$⊢ X \in (\{0\} \cup (0, 1]) \leftrightarrow X \in [0, 1]$
68		elun	$⊢ X \in (\{0\} \cup (0, 1]) \leftrightarrow (X \in \{0\} \lor X \in (0, 1])$
69	67 68	bitr3i	$⊢ X \in [0, 1] \leftrightarrow (X \in \{0\} \lor X \in (0, 1])$
70		elsni	$⊢ X \in \{0\} \to X = 0$
71	70	orim1i	$⊢ (X \in \{0\} \lor X \in (0, 1]) \to (X = 0 \lor X \in (0, 1])$
72	69 71	sylbi	$⊢ X \in [0, 1] \to (X = 0 \lor X \in (0, 1])$
73	18	oveq1i	$⊢ F (0) +_{𝑒} F (Y) = +∞ +_{𝑒} F (Y)$
74		simpr	$⊢ (X = 0 \land Y \in (0, 1]) \to Y \in (0, 1]$
75	1	xrge0iifcv	$⊢ Y \in (0, 1] \to F (Y) = - \log Y$
76		0le0	$⊢ 0 \leq 0$
77		1re	$⊢ 1 \in ℝ$
78		ltpnf	$⊢ 1 \in ℝ \to 1 < +∞$
79	77 78	ax-mp	$⊢ 1 < +∞$
80		iocssioo	$⊢ ((0 \in ℝ^{} \land +∞ \in ℝ^{}) \land (0 \leq 0 \land 1 < +∞)) \to (0, 1] \subseteq (0, +∞)$
81	3 27 76 79 80	mp4an	$⊢ (0, 1] \subseteq (0, +∞)$
82		ioorp	$⊢ (0, +∞) = ℝ^{+}$
83	81 82	sseqtri	$⊢ (0, 1] \subseteq ℝ^{+}$
84	83	sseli	$⊢ Y \in (0, 1] \to Y \in ℝ^{+}$
85	84	relogcld	$⊢ Y \in (0, 1] \to \log Y \in ℝ$
86	85	renegcld	$⊢ Y \in (0, 1] \to - \log Y \in ℝ$
87	75 86	eqeltrd	$⊢ Y \in (0, 1] \to F (Y) \in ℝ$
88	87	rexrd	$⊢ Y \in (0, 1] \to F (Y) \in ℝ^{*}$
89	74 88	syl	$⊢ (X = 0 \land Y \in (0, 1]) \to F (Y) \in ℝ^{*}$
90	87	renemnfd	$⊢ Y \in (0, 1] \to F (Y) \neq −∞$
91	74 90	syl	$⊢ (X = 0 \land Y \in (0, 1]) \to F (Y) \neq −∞$
92		xaddpnf2	$⊢ (F (Y) \in ℝ^{*} \land F (Y) \neq −∞) \to +∞ +_{𝑒} F (Y) = +∞$
93	89 91 92	syl2anc	$⊢ (X = 0 \land Y \in (0, 1]) \to +∞ +_{𝑒} F (Y) = +∞$
94	73 93	syl5eq	$⊢ (X = 0 \land Y \in (0, 1]) \to F (0) +_{𝑒} F (Y) = +∞$
95		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
96	83 95	sstri	$⊢ (0, 1] \subseteq ℝ$
97		ax-resscn	$⊢ ℝ \subseteq ℂ$
98	96 97	sstri	$⊢ (0, 1] \subseteq ℂ$
99	98 74	sselid	$⊢ (X = 0 \land Y \in (0, 1]) \to Y \in ℂ$
100	99	mul02d	$⊢ (X = 0 \land Y \in (0, 1]) \to 0 \cdot Y = 0$
101	100	fveq2d	$⊢ (X = 0 \land Y \in (0, 1]) \to F (0 \cdot Y) = F (0)$
102	101 18	eqtrdi	$⊢ (X = 0 \land Y \in (0, 1]) \to F (0 \cdot Y) = +∞$
103	94 102	eqtr4d	$⊢ (X = 0 \land Y \in (0, 1]) \to F (0) +_{𝑒} F (Y) = F (0 \cdot Y)$
104		simpl	$⊢ (X = 0 \land Y \in (0, 1]) \to X = 0$
105	104	fveq2d	$⊢ (X = 0 \land Y \in (0, 1]) \to F (X) = F (0)$
106	105	oveq1d	$⊢ (X = 0 \land Y \in (0, 1]) \to F (X) +_{𝑒} F (Y) = F (0) +_{𝑒} F (Y)$
107	104	fvoveq1d	$⊢ (X = 0 \land Y \in (0, 1]) \to F (X Y) = F (0 \cdot Y)$
108	103 106 107	3eqtr4rd	$⊢ (X = 0 \land Y \in (0, 1]) \to F (X Y) = F (X) +_{𝑒} F (Y)$
109		simpl	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to X \in (0, 1]$
110	83 109	sselid	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to X \in ℝ^{+}$
111	110	relogcld	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to \log X \in ℝ$
112	111	renegcld	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to - \log X \in ℝ$
113		simpr	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to Y \in (0, 1]$
114	83 113	sselid	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to Y \in ℝ^{+}$
115	114	relogcld	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to \log Y \in ℝ$
116	115	renegcld	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to - \log Y \in ℝ$
117		rexadd	$⊢ (- \log X \in ℝ \land - \log Y \in ℝ) \to (- \log X) +_{𝑒} (- \log Y) = - \log X + (- \log Y)$
118	112 116 117	syl2anc	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to (- \log X) +_{𝑒} (- \log Y) = - \log X + (- \log Y)$
119	1	xrge0iifcv	$⊢ X \in (0, 1] \to F (X) = - \log X$
120	119 75	oveqan12d	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to F (X) +_{𝑒} F (Y) = (- \log X) +_{𝑒} (- \log Y)$
121	110	rpred	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to X \in ℝ$
122	114	rpred	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to Y \in ℝ$
123	121 122	remulcld	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to X Y \in ℝ$
124	110	rpgt0d	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to 0 < X$
125	114	rpgt0d	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to 0 < Y$
126	121 122 124 125	mulgt0d	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to 0 < X Y$
127		iocssicc	$⊢ (0, 1] \subseteq [0, 1]$
128	127 109	sselid	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to X \in [0, 1]$
129	127 113	sselid	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to Y \in [0, 1]$
130		iimulcl	$⊢ (X \in [0, 1] \land Y \in [0, 1]) \to X Y \in [0, 1]$
131	128 129 130	syl2anc	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to X Y \in [0, 1]$
132		elicc01	$⊢ X Y \in [0, 1] \leftrightarrow (X Y \in ℝ \land 0 \leq X Y \land X Y \leq 1)$
133	132	simp3bi	$⊢ X Y \in [0, 1] \to X Y \leq 1$
134	131 133	syl	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to X Y \leq 1$
135		elioc2	$⊢ (0 \in ℝ^{*} \land 1 \in ℝ) \to (X Y \in (0, 1] \leftrightarrow (X Y \in ℝ \land 0 < X Y \land X Y \leq 1))$
136	3 77 135	mp2an	$⊢ X Y \in (0, 1] \leftrightarrow (X Y \in ℝ \land 0 < X Y \land X Y \leq 1)$
137	123 126 134 136	syl3anbrc	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to X Y \in (0, 1]$
138	1	xrge0iifcv	$⊢ X Y \in (0, 1] \to F (X Y) = - \log X Y$
139	137 138	syl	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to F (X Y) = - \log X Y$
140	110 114	relogmuld	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to \log X Y = \log X + \log Y$
141	140	negeqd	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to - \log X Y = - (\log X + \log Y)$
142	111	recnd	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to \log X \in ℂ$
143	115	recnd	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to \log Y \in ℂ$
144	142 143	negdid	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to - (\log X + \log Y) = - \log X + (- \log Y)$
145	139 141 144	3eqtrd	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to F (X Y) = - \log X + (- \log Y)$
146	118 120 145	3eqtr4rd	$⊢ (X \in (0, 1] \land Y \in (0, 1]) \to F (X Y) = F (X) +_{𝑒} F (Y)$
147	108 146	jaoian	$⊢ ((X = 0 \lor X \in (0, 1]) \land Y \in (0, 1]) \to F (X Y) = F (X) +_{𝑒} F (Y)$
148	72 147	sylan	$⊢ (X \in [0, 1] \land Y \in (0, 1]) \to F (X Y) = F (X) +_{𝑒} F (Y)$
149	66 148	jaodan	$⊢ (X \in [0, 1] \land (Y = 0 \lor Y \in (0, 1])) \to F (X Y) = F (X) +_{𝑒} F (Y)$
150	13 149	sylan2	$⊢ (X \in [0, 1] \land Y \in [0, 1]) \to F (X Y) = F (X) +_{𝑒} F (Y)$

Metamath Proof Explorer

Theorem xrge0iifhom

Proof