Theorem pcorev2

Description: Concatenation with the reverse path. (Contributed by Mario Carneiro, 12-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		pcorev2.1	⊢ 𝐺 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 1 − 𝑥 ) ) )
2		pcorev2.2	⊢ 𝑃 = ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } )
3	1	pcorevcl	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → ( 𝐺 ∈ ( II Cn 𝐽 ) ∧ ( 𝐺 ‘ 0 ) = ( 𝐹 ‘ 1 ) ∧ ( 𝐺 ‘ 1 ) = ( 𝐹 ‘ 0 ) ) )
4	3	simp1d	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → 𝐺 ∈ ( II Cn 𝐽 ) )
5		eqid	⊢ ( 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑦 ) ) ) = ( 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑦 ) ) )
6		eqid	⊢ ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 1 ) } ) = ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 1 ) } )
7	5 6	pcorev	⊢ ( 𝐺 ∈ ( II Cn 𝐽 ) → ( ( 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑦 ) ) ) ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 1 ) } ) )
8	4 7	syl	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → ( ( 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑦 ) ) ) ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 1 ) } ) )
9		iirev	⊢ ( 𝑦 ∈ ( 0 [,] 1 ) → ( 1 − 𝑦 ) ∈ ( 0 [,] 1 ) )
10		oveq2	⊢ ( 𝑥 = ( 1 − 𝑦 ) → ( 1 − 𝑥 ) = ( 1 − ( 1 − 𝑦 ) ) )
11	10	fveq2d	⊢ ( 𝑥 = ( 1 − 𝑦 ) → ( 𝐹 ‘ ( 1 − 𝑥 ) ) = ( 𝐹 ‘ ( 1 − ( 1 − 𝑦 ) ) ) )
12		fvex	⊢ ( 𝐹 ‘ ( 1 − ( 1 − 𝑦 ) ) ) ∈ V
13	11 1 12	fvmpt	⊢ ( ( 1 − 𝑦 ) ∈ ( 0 [,] 1 ) → ( 𝐺 ‘ ( 1 − 𝑦 ) ) = ( 𝐹 ‘ ( 1 − ( 1 − 𝑦 ) ) ) )
14	9 13	syl	⊢ ( 𝑦 ∈ ( 0 [,] 1 ) → ( 𝐺 ‘ ( 1 − 𝑦 ) ) = ( 𝐹 ‘ ( 1 − ( 1 − 𝑦 ) ) ) )
15		ax-1cn	⊢ 1 ∈ ℂ
16		unitssre	⊢ ( 0 [,] 1 ) ⊆ ℝ
17	16	sseli	⊢ ( 𝑦 ∈ ( 0 [,] 1 ) → 𝑦 ∈ ℝ )
18	17	recnd	⊢ ( 𝑦 ∈ ( 0 [,] 1 ) → 𝑦 ∈ ℂ )
19		nncan	⊢ ( ( 1 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 1 − ( 1 − 𝑦 ) ) = 𝑦 )
20	15 18 19	sylancr	⊢ ( 𝑦 ∈ ( 0 [,] 1 ) → ( 1 − ( 1 − 𝑦 ) ) = 𝑦 )
21	20	fveq2d	⊢ ( 𝑦 ∈ ( 0 [,] 1 ) → ( 𝐹 ‘ ( 1 − ( 1 − 𝑦 ) ) ) = ( 𝐹 ‘ 𝑦 ) )
22	14 21	eqtrd	⊢ ( 𝑦 ∈ ( 0 [,] 1 ) → ( 𝐺 ‘ ( 1 − 𝑦 ) ) = ( 𝐹 ‘ 𝑦 ) )
23	22	mpteq2ia	⊢ ( 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑦 ) ) ) = ( 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ 𝑦 ) )
24		iiuni	⊢ ( 0 [,] 1 ) = ∪ II
25		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
26	24 25	cnf	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → 𝐹 : ( 0 [,] 1 ) ⟶ ∪ 𝐽 )
27	26	feqmptd	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → 𝐹 = ( 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ 𝑦 ) ) )
28	23 27	eqtr4id	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → ( 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑦 ) ) ) = 𝐹 )
29	28	oveq1d	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → ( ( 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑦 ) ) ) ( *𝑝 ‘ 𝐽 ) 𝐺 ) = ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) )
30	3	simp3d	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → ( 𝐺 ‘ 1 ) = ( 𝐹 ‘ 0 ) )
31	30	sneqd	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → { ( 𝐺 ‘ 1 ) } = { ( 𝐹 ‘ 0 ) } )
32	31	xpeq2d	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 1 ) } ) = ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) )
33	32 2	eqtr4di	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 1 ) } ) = 𝑃 )
34	8 29 33	3brtr3d	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( ≃ph ‘ 𝐽 ) 𝑃 )