pcorev2

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

	Ref	Expression
Hypotheses	pcorev2.1	$⊢ G = (x \in [0, 1] ⟼ F (1 - x))$
	pcorev2.2	$⊢ P = [0, 1] \times \{F (0)\}$
Assertion	pcorev2	$⊢ F \in (II Cn J) \to (F *_{𝑝} (J) G) ≃_{ph} (J) P$

Proof

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

Metamath Proof Explorer

Theorem pcorev2

Proof