Metamath Proof Explorer

Theorem pcorev2

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

Ref Expression
Hypotheses pcorev2.1 ⊢ G = x ∈ 0 1 ⟼ F ⁡ 1 − x
pcorev2.2 ⊢ P = 0 1 × F ⁡ 0
Assertion pcorev2 ⊢ F ∈ II Cn J → F * 𝑝 ⁡ J G ≃ ph ⁡ J P

Proof

Step Hyp Ref Expression
1 pcorev2.1 ⊢ G = x ∈ 0 1 ⟼ F ⁡ 1 − x
2 pcorev2.2 ⊢ P = 0 1 × F ⁡ 0
3 1 pcorevcl ⊢ F ∈ II Cn J → G ∈ II Cn J ∧ G ⁡ 0 = F ⁡ 1 ∧ G ⁡ 1 = F ⁡ 0
4 3 simp1d ⊢ F ∈ II Cn J → G ∈ II Cn J
5 eqid ⊢ y ∈ 0 1 ⟼ G ⁡ 1 − y = y ∈ 0 1 ⟼ G ⁡ 1 − y
6 eqid ⊢ 0 1 × G ⁡ 1 = 0 1 × G ⁡ 1
7 5 6 pcorev ⊢ G ∈ II Cn J → y ∈ 0 1 ⟼ G ⁡ 1 − y * 𝑝 ⁡ J G ≃ ph ⁡ J 0 1 × G ⁡ 1
8 4 7 syl ⊢ F ∈ II Cn J → y ∈ 0 1 ⟼ G ⁡ 1 − y * 𝑝 ⁡ J G ≃ ph ⁡ J 0 1 × G ⁡ 1
9 iirev ⊢ y ∈ 0 1 → 1 − y ∈ 0 1
10 oveq2 ⊢ x = 1 − y → 1 − x = 1 − 1 − y
11 10 fveq2d ⊢ x = 1 − y → F ⁡ 1 − x = F ⁡ 1 − 1 − y
12 fvex ⊢ F ⁡ 1 − 1 − y ∈ V
13 11 1 12 fvmpt ⊢ 1 − y ∈ 0 1 → G ⁡ 1 − y = F ⁡ 1 − 1 − y
14 9 13 syl ⊢ y ∈ 0 1 → G ⁡ 1 − y = F ⁡ 1 − 1 − y
15 ax-1cn ⊢ 1 ∈ ℂ
16 unitssre ⊢ 0 1 ⊆ ℝ
17 16 sseli ⊢ y ∈ 0 1 → y ∈ ℝ
18 17 recnd ⊢ y ∈ 0 1 → y ∈ ℂ
19 nncan ⊢ 1 ∈ ℂ ∧ y ∈ ℂ → 1 − 1 − y = y
20 15 18 19 sylancr ⊢ y ∈ 0 1 → 1 − 1 − y = y
21 20 fveq2d ⊢ y ∈ 0 1 → F ⁡ 1 − 1 − y = F ⁡ y
22 14 21 eqtrd ⊢ y ∈ 0 1 → G ⁡ 1 − y = F ⁡ y
23 22 mpteq2ia ⊢ y ∈ 0 1 ⟼ G ⁡ 1 − y = y ∈ 0 1 ⟼ F ⁡ y
24 iiuni ⊢ 0 1 = ⋃ II
25 eqid ⊢ ⋃ J = ⋃ J
26 24 25 cnf ⊢ F ∈ II Cn J → F : 0 1 ⟶ ⋃ J
27 26 feqmptd ⊢ F ∈ II Cn J → F = y ∈ 0 1 ⟼ F ⁡ y
28 23 27 eqtr4id ⊢ F ∈ II Cn J → y ∈ 0 1 ⟼ G ⁡ 1 − y = F
29 28 oveq1d ⊢ F ∈ II Cn J → y ∈ 0 1 ⟼ G ⁡ 1 − y * 𝑝 ⁡ J G = F * 𝑝 ⁡ J G
30 3 simp3d ⊢ F ∈ II Cn J → G ⁡ 1 = F ⁡ 0
31 30 sneqd ⊢ F ∈ II Cn J → G ⁡ 1 = F ⁡ 0
32 31 xpeq2d ⊢ F ∈ II Cn J → 0 1 × G ⁡ 1 = 0 1 × F ⁡ 0
33 32 2 eqtr4di ⊢ F ∈ II Cn J → 0 1 × G ⁡ 1 = P
34 8 29 33 3brtr3d ⊢ F ∈ II Cn J → F * 𝑝 ⁡ J G ≃ ph ⁡ J P