Theorem pcorev

Description: Concatenation with the reverse path. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 20-Dec-2013)

	Ref	Expression
Hypotheses	pcorev.1	⊢ 𝐺 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 1 − 𝑥 ) ) )
	pcorev.2	⊢ 𝑃 = ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 1 ) } )
Assertion	pcorev	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → ( 𝐺 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ( ≃ph ‘ 𝐽 ) 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		pcorev.1	⊢ 𝐺 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 1 − 𝑥 ) ) )
2		pcorev.2	⊢ 𝑃 = ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 1 ) } )
3		eqid	⊢ ( 𝑠 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ if ( 𝑠 ≤ ( 1 / 2 ) , ( 1 − ( ( 1 − 𝑡 ) · ( 2 · 𝑠 ) ) ) , ( 1 − ( ( 1 − 𝑡 ) · ( 1 − ( ( 2 · 𝑠 ) − 1 ) ) ) ) ) ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ if ( 𝑠 ≤ ( 1 / 2 ) , ( 1 − ( ( 1 − 𝑡 ) · ( 2 · 𝑠 ) ) ) , ( 1 − ( ( 1 − 𝑡 ) · ( 1 − ( ( 2 · 𝑠 ) − 1 ) ) ) ) ) ) )
4	1 2 3	pcorevlem	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → ( ( 𝑠 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ if ( 𝑠 ≤ ( 1 / 2 ) , ( 1 − ( ( 1 − 𝑡 ) · ( 2 · 𝑠 ) ) ) , ( 1 − ( ( 1 − 𝑡 ) · ( 1 − ( ( 2 · 𝑠 ) − 1 ) ) ) ) ) ) ) ∈ ( ( 𝐺 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ( PHtpy ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐺 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) )
5	4	simprd	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → ( 𝐺 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ( ≃ph ‘ 𝐽 ) 𝑃 )