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	⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) )
	xrge0iifhmeo.k	⊢ 𝐽 = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
Assertion	xrge0iif1	⊢ ( 𝐹 ‘ 1 ) = 0

Proof

Step	Hyp	Ref	Expression
1		xrge0iifhmeo.1	⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) )
2		xrge0iifhmeo.k	⊢ 𝐽 = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
3		1elunit	⊢ 1 ∈ ( 0 [,] 1 )
4		ax-1ne0	⊢ 1 ≠ 0
5		neeq1	⊢ ( 𝑥 = 1 → ( 𝑥 ≠ 0 ↔ 1 ≠ 0 ) )
6	4 5	mpbiri	⊢ ( 𝑥 = 1 → 𝑥 ≠ 0 )
7	6	neneqd	⊢ ( 𝑥 = 1 → ¬ 𝑥 = 0 )
8	7	iffalsed	⊢ ( 𝑥 = 1 → if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) = - ( log ‘ 𝑥 ) )
9		fveq2	⊢ ( 𝑥 = 1 → ( log ‘ 𝑥 ) = ( log ‘ 1 ) )
10	9	negeqd	⊢ ( 𝑥 = 1 → - ( log ‘ 𝑥 ) = - ( 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	⊢ ( 𝑥 = 1 → - ( log ‘ 1 ) = 0 )
16	8 10 15	3eqtrd	⊢ ( 𝑥 = 1 → if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) = 0 )
17		c0ex	⊢ 0 ∈ V
18	16 1 17	fvmpt	⊢ ( 1 ∈ ( 0 [,] 1 ) → ( 𝐹 ‘ 1 ) = 0 )
19	3 18	ax-mp	⊢ ( 𝐹 ‘ 1 ) = 0