Theorem pcovalg

Description: Evaluate the concatenation of two paths. (Contributed by Mario Carneiro, 7-Jun-2014)

	Ref	Expression
Hypotheses	pcoval.2	⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
	pcoval.3	⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
Assertion	pcovalg	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 𝑋 ) = if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pcoval.2	⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
2		pcoval.3	⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
3	1 2	pcoval	⊢ ( 𝜑 → ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) )
4	3	fveq1d	⊢ ( 𝜑 → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 𝑋 ) = ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ‘ 𝑋 ) )
5		breq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ ( 1 / 2 ) ↔ 𝑋 ≤ ( 1 / 2 ) ) )
6		oveq2	⊢ ( 𝑥 = 𝑋 → ( 2 · 𝑥 ) = ( 2 · 𝑋 ) )
7	6	fveq2d	⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ ( 2 · 𝑥 ) ) = ( 𝐹 ‘ ( 2 · 𝑋 ) ) )
8	6	fvoveq1d	⊢ ( 𝑥 = 𝑋 → ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) = ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) )
9	5 7 8	ifbieq12d	⊢ ( 𝑥 = 𝑋 → if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) = if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) )
10		eqid	⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) )
11		fvex	⊢ ( 𝐹 ‘ ( 2 · 𝑋 ) ) ∈ V
12		fvex	⊢ ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ∈ V
13	11 12	ifex	⊢ if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) ∈ V
14	9 10 13	fvmpt	⊢ ( 𝑋 ∈ ( 0 [,] 1 ) → ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ‘ 𝑋 ) = if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) )
15	4 14	sylan9eq	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 𝑋 ) = if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) )