Theorem xrge0iif1

Description: Condition for the defined function, -u ( logx ) to be a monoid homomorphism. (Contributed by Thierry Arnoux, 20-Jun-2017)

	Ref	Expression
Hypotheses	xrge0iifhmeo.1	$$⊢F=\left(x\in \left[0,1\right]⟼if\left(x=0,\mathrm{+\infty },-\log x\right)\right)$$
	xrge0iifhmeo.k	$$⊢J=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,\mathrm{+\infty }\right]$$
Assertion	xrge0iif1	$$⊢F\left(1\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		xrge0iifhmeo.1	$$⊢F=\left(x\in \left[0,1\right]⟼if\left(x=0,\mathrm{+\infty },-\log x\right)\right)$$
2		xrge0iifhmeo.k	$$⊢J=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,\mathrm{+\infty }\right]$$
3		1elunit	$$⊢1\in \left[0,1\right]$$
4		ax-1ne0	$$⊢1\ne 0$$
5		neeq1	$$⊢x=1\to \left(x\ne 0\leftrightarrow 1\ne 0\right)$$
6	4 5	mpbiri	$$⊢x=1\to x\ne 0$$
7	6	neneqd	$$⊢x=1\to \neg x=0$$
8	7	iffalsed	$$⊢x=1\to if\left(x=0,\mathrm{+\infty },-\log x\right)=-\log x$$
9		fveq2	$$⊢x=1\to \log x=\log 1$$
10	9	negeqd	$$⊢x=1\to -\log x=-\log 1$$
11		log1	$$⊢\log 1=0$$
12	11	negeqi	$$⊢-\log 1=-0$$
13		neg0	$$⊢-0=0$$
14	12 13	eqtri	$$⊢-\log 1=0$$
15	14	a1i	$$⊢x=1\to -\log 1=0$$
16	8 10 15	3eqtrd	$$⊢x=1\to if\left(x=0,\mathrm{+\infty },-\log x\right)=0$$
17		c0ex	$$⊢0\in \mathrm{V}$$
18	16 1 17	fvmpt	$$⊢1\in \left[0,1\right]\to F\left(1\right)=0$$
19	3 18	ax-mp	$$⊢F\left(1\right)=0$$