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 = ( x e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) )
	xrge0iifhmeo.k	|- J = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
Assertion	xrge0iif1	|- ( F ` 1 ) = 0

Proof

Step	Hyp	Ref	Expression
1		xrge0iifhmeo.1	|- F = ( x e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) )
2		xrge0iifhmeo.k	|- J = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
3		1elunit	|- 1 e. ( 0 [,] 1 )
4		ax-1ne0	|- 1 =/= 0
5		neeq1	|- ( x = 1 -> ( x =/= 0 <-> 1 =/= 0 ) )
6	4 5	mpbiri	|- ( x = 1 -> x =/= 0 )
7	6	neneqd	|- ( x = 1 -> -. x = 0 )
8	7	iffalsed	|- ( x = 1 -> if ( x = 0 , +oo , -u ( log ` x ) ) = -u ( log ` x ) )
9		fveq2	|- ( x = 1 -> ( log ` x ) = ( log ` 1 ) )
10	9	negeqd	|- ( x = 1 -> -u ( log ` x ) = -u ( log ` 1 ) )
11		log1	|- ( log ` 1 ) = 0
12	11	negeqi	|- -u ( log ` 1 ) = -u 0
13		neg0	|- -u 0 = 0
14	12 13	eqtri	|- -u ( log ` 1 ) = 0
15	14	a1i	|- ( x = 1 -> -u ( log ` 1 ) = 0 )
16	8 10 15	3eqtrd	|- ( x = 1 -> if ( x = 0 , +oo , -u ( log ` x ) ) = 0 )
17		c0ex	|- 0 e. _V
18	16 1 17	fvmpt	|- ( 1 e. ( 0 [,] 1 ) -> ( F ` 1 ) = 0 )
19	3 18	ax-mp	|- ( F ` 1 ) = 0