Metamath Proof Explorer

Theorem pcovalg

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

Ref Expression
Hypotheses pcoval.2 ⊢ φ → F ∈ II Cn J
pcoval.3 ⊢ φ → G ∈ II Cn J
Assertion pcovalg ⊢ φ ∧ X ∈ 0 1 → F * 𝑝 ⁡ J G ⁡ X = if X ≤ 1 2 F ⁡ 2 ⁢ X G ⁡ 2 ⁢ X − 1

Proof

Step Hyp Ref Expression
1 pcoval.2 ⊢ φ → F ∈ II Cn J
2 pcoval.3 ⊢ φ → G ∈ II Cn J
3 1 2 pcoval ⊢ φ → F * 𝑝 ⁡ J G = x ∈ 0 1 ⟼ if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1
4 3 fveq1d ⊢ φ → F * 𝑝 ⁡ J G ⁡ X = x ∈ 0 1 ⟼ if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1 ⁡ X
5 breq1 ⊢ x = X → x ≤ 1 2 ↔ X ≤ 1 2
6 oveq2 ⊢ x = X → 2 ⁢ x = 2 ⁢ X
7 6 fveq2d ⊢ x = X → F ⁡ 2 ⁢ x = F ⁡ 2 ⁢ X
8 6 fvoveq1d ⊢ x = X → G ⁡ 2 ⁢ x − 1 = G ⁡ 2 ⁢ X − 1
9 5 7 8 ifbieq12d ⊢ x = X → if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1 = if X ≤ 1 2 F ⁡ 2 ⁢ X G ⁡ 2 ⁢ X − 1
10 eqid ⊢ x ∈ 0 1 ⟼ if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1 = x ∈ 0 1 ⟼ if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1
11 fvex ⊢ F ⁡ 2 ⁢ X ∈ V
12 fvex ⊢ G ⁡ 2 ⁢ X − 1 ∈ V
13 11 12 ifex ⊢ if X ≤ 1 2 F ⁡ 2 ⁢ X G ⁡ 2 ⁢ X − 1 ∈ V
14 9 10 13 fvmpt ⊢ X ∈ 0 1 → x ∈ 0 1 ⟼ if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1 ⁡ X = if X ≤ 1 2 F ⁡ 2 ⁢ X G ⁡ 2 ⁢ X − 1
15 4 14 sylan9eq ⊢ φ ∧ X ∈ 0 1 → F * 𝑝 ⁡ J G ⁡ X = if X ≤ 1 2 F ⁡ 2 ⁢ X G ⁡ 2 ⁢ X − 1