pcopt - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > pcopt		Structured version Visualization version GIF version

Theorem pcopt 25040

Description: Concatenation with a point does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)

**Hypothesis**
Ref	Expression
pcopt.1	⊢ 𝑃 = ((0[,]1) × {𝑌})

**Assertion**
Ref	Expression
pcopt	⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑃(*_𝑝‘𝐽)𝐹)( ≃_ph‘𝐽)𝐹)

Proof of Theorem pcopt Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		pcopt.1	. . . . . . . . . 10 ⊢ 𝑃 = ((0[,]1) × {𝑌})
2	1	fveq1i 6902	. . . . . . . . 9 ⊢ (𝑃‘(2 · 𝑥)) = (((0[,]1) × {𝑌})‘(2 · 𝑥))
3		simpr 483	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝐹‘0) = 𝑌)
4		iiuni 24892	. . . . . . . . . . . . . 14 ⊢ (0[,]1) = ∪ II
5		eqid 2726	. . . . . . . . . . . . . 14 ⊢ ∪ 𝐽 = ∪ 𝐽
6	4, 5	cnf 23241	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐹:(0[,]1)⟶∪ 𝐽)
7	6	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → 𝐹:(0[,]1)⟶∪ 𝐽)
8		0elunit 13500	. . . . . . . . . . . 12 ⊢ 0 ∈ (0[,]1)
9		ffvelcdm 7095	. . . . . . . . . . . 12 ⊢ ((𝐹:(0[,]1)⟶∪ 𝐽 ∧ 0 ∈ (0[,]1)) → (𝐹‘0) ∈ ∪ 𝐽)
10	7, 8, 9	sylancl 584	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝐹‘0) ∈ ∪ 𝐽)
11	3, 10	eqeltrrd 2827	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → 𝑌 ∈ ∪ 𝐽)
12		elii1 24949	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (0[,](1 / 2)) ↔ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 2)))
13		iihalf1 24943	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (0[,](1 / 2)) → (2 · 𝑥) ∈ (0[,]1))
14	12, 13	sylbir 234	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 2)) → (2 · 𝑥) ∈ (0[,]1))
15		fvconst2g 7219	. . . . . . . . . 10 ⊢ ((𝑌 ∈ ∪ 𝐽 ∧ (2 · 𝑥) ∈ (0[,]1)) → (((0[,]1) × {𝑌})‘(2 · 𝑥)) = 𝑌)
16	11, 14, 15	syl2an 594	. . . . . . . . 9 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 2))) → (((0[,]1) × {𝑌})‘(2 · 𝑥)) = 𝑌)
17	2, 16	eqtrid 2778	. . . . . . . 8 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 2))) → (𝑃‘(2 · 𝑥)) = 𝑌)
18		simplr 767	. . . . . . . 8 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 2))) → (𝐹‘0) = 𝑌)
19	17, 18	eqtr4d 2769	. . . . . . 7 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 2))) → (𝑃‘(2 · 𝑥)) = (𝐹‘0))
20	19	ifeq1d 4552	. . . . . 6 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 2))) → if(𝑥 ≤ (1 / 2), (𝑃‘(2 · 𝑥)), (𝐹‘((2 · 𝑥) − 1))) = if(𝑥 ≤ (1 / 2), (𝐹‘0), (𝐹‘((2 · 𝑥) − 1))))
21	20	expr 455	. . . . 5 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ 𝑥 ∈ (0[,]1)) → (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), (𝑃‘(2 · 𝑥)), (𝐹‘((2 · 𝑥) − 1))) = if(𝑥 ≤ (1 / 2), (𝐹‘0), (𝐹‘((2 · 𝑥) − 1)))))
22		iffalse 4542	. . . . . 6 ⊢ (¬ 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), (𝑃‘(2 · 𝑥)), (𝐹‘((2 · 𝑥) − 1))) = (𝐹‘((2 · 𝑥) − 1)))
23		iffalse 4542	. . . . . 6 ⊢ (¬ 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), (𝐹‘0), (𝐹‘((2 · 𝑥) − 1))) = (𝐹‘((2 · 𝑥) − 1)))
24	22, 23	eqtr4d 2769	. . . . 5 ⊢ (¬ 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), (𝑃‘(2 · 𝑥)), (𝐹‘((2 · 𝑥) − 1))) = if(𝑥 ≤ (1 / 2), (𝐹‘0), (𝐹‘((2 · 𝑥) − 1))))
25	21, 24	pm2.61d1 180	. . . 4 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ 𝑥 ∈ (0[,]1)) → if(𝑥 ≤ (1 / 2), (𝑃‘(2 · 𝑥)), (𝐹‘((2 · 𝑥) − 1))) = if(𝑥 ≤ (1 / 2), (𝐹‘0), (𝐹‘((2 · 𝑥) − 1))))
26	25	mpteq2dva 5253	. . 3 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑃‘(2 · 𝑥)), (𝐹‘((2 · 𝑥) − 1)))) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝐹‘0), (𝐹‘((2 · 𝑥) − 1)))))
27		cntop2 23236	. . . . . . . 8 ⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐽 ∈ Top)
28	27	adantr 479	. . . . . . 7 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → 𝐽 ∈ Top)
29		toptopon2 22911	. . . . . . 7 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))
30	28, 29	sylib 217	. . . . . 6 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → 𝐽 ∈ (TopOn‘∪ 𝐽))
31	1	pcoptcl 25039	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ 𝑌 ∈ ∪ 𝐽) → (𝑃 ∈ (II Cn 𝐽) ∧ (𝑃‘0) = 𝑌 ∧ (𝑃‘1) = 𝑌))
32	30, 11, 31	syl2anc 582	. . . . 5 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑃 ∈ (II Cn 𝐽) ∧ (𝑃‘0) = 𝑌 ∧ (𝑃‘1) = 𝑌))
33	32	simp1d 1139	. . . 4 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → 𝑃 ∈ (II Cn 𝐽))
34		simpl 481	. . . 4 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → 𝐹 ∈ (II Cn 𝐽))
35	33, 34	pcoval 25029	. . 3 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑃(*_𝑝‘𝐽)𝐹) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑃‘(2 · 𝑥)), (𝐹‘((2 · 𝑥) − 1)))))
36		iffalse 4542	. . . . . . . . 9 ⊢ (¬ 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)) = ((2 · 𝑥) − 1))
37	36	adantl 480	. . . . . . . 8 ⊢ ((𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)) = ((2 · 𝑥) − 1))
38		elii2 24950	. . . . . . . . 9 ⊢ ((𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ((1 / 2)[,]1))
39		iihalf2 24946	. . . . . . . . 9 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((2 · 𝑥) − 1) ∈ (0[,]1))
40	38, 39	syl 17	. . . . . . . 8 ⊢ ((𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((2 · 𝑥) − 1) ∈ (0[,]1))
41	37, 40	eqeltrd 2826	. . . . . . 7 ⊢ ((𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)) ∈ (0[,]1))
42	41	ex 411	. . . . . 6 ⊢ (𝑥 ∈ (0[,]1) → (¬ 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)) ∈ (0[,]1)))
43		iftrue 4539	. . . . . . 7 ⊢ (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)) = 0)
44	43, 8	eqeltrdi 2834	. . . . . 6 ⊢ (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)) ∈ (0[,]1))
45	42, 44	pm2.61d2 181	. . . . 5 ⊢ (𝑥 ∈ (0[,]1) → if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)) ∈ (0[,]1))
46	45	adantl 480	. . . 4 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ 𝑥 ∈ (0[,]1)) → if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)) ∈ (0[,]1))
47		eqid 2726	. . . . 5 ⊢ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1))) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)))
48	47	a1i 11	. . . 4 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1))) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1))))
49	7	feqmptd 6971	. . . 4 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → 𝐹 = (𝑦 ∈ (0[,]1) ↦ (𝐹‘𝑦)))
50		fveq2 6901	. . . . 5 ⊢ (𝑦 = if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)) → (𝐹‘𝑦) = (𝐹‘if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1))))
51		fvif 6917	. . . . 5 ⊢ (𝐹‘if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1))) = if(𝑥 ≤ (1 / 2), (𝐹‘0), (𝐹‘((2 · 𝑥) − 1)))
52	50, 51	eqtrdi 2782	. . . 4 ⊢ (𝑦 = if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)) → (𝐹‘𝑦) = if(𝑥 ≤ (1 / 2), (𝐹‘0), (𝐹‘((2 · 𝑥) − 1))))
53	46, 48, 49, 52	fmptco 7143	. . 3 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝐹 ∘ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)))) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝐹‘0), (𝐹‘((2 · 𝑥) − 1)))))
54	26, 35, 53	3eqtr4d 2776	. 2 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑃(*_𝑝‘𝐽)𝐹) = (𝐹 ∘ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)))))
55		iitopon 24890	. . . . 5 ⊢ II ∈ (TopOn‘(0[,]1))
56	55	a1i 11	. . . 4 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → II ∈ (TopOn‘(0[,]1)))
57	56	cnmptid 23656	. . . 4 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn II))
58	8	a1i 11	. . . . 5 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → 0 ∈ (0[,]1))
59	56, 56, 58	cnmptc 23657	. . . 4 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑥 ∈ (0[,]1) ↦ 0) ∈ (II Cn II))
60		eqid 2726	. . . . 5 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
61		eqid 2726	. . . . 5 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 2))) = ((topGen‘ran (,)) ↾_t (0[,](1 / 2)))
62		eqid 2726	. . . . 5 ⊢ ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) = ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1))
63		dfii2 24893	. . . . 5 ⊢ II = ((topGen‘ran (,)) ↾_t (0[,]1))
64		0re 11266	. . . . . 6 ⊢ 0 ∈ ℝ
65	64	a1i 11	. . . . 5 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → 0 ∈ ℝ)
66		1re 11264	. . . . . 6 ⊢ 1 ∈ ℝ
67	66	a1i 11	. . . . 5 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → 1 ∈ ℝ)
68		halfre 12478	. . . . . . 7 ⊢ (1 / 2) ∈ ℝ
69		halfge0 12481	. . . . . . 7 ⊢ 0 ≤ (1 / 2)
70		halflt1 12482	. . . . . . . 8 ⊢ (1 / 2) < 1
71	68, 66, 70	ltleii 11387	. . . . . . 7 ⊢ (1 / 2) ≤ 1
72		elicc01 13497	. . . . . . 7 ⊢ ((1 / 2) ∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 / 2) ≤ 1))
73	68, 69, 71, 72	mpbir3an 1338	. . . . . 6 ⊢ (1 / 2) ∈ (0[,]1)
74	73	a1i 11	. . . . 5 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (1 / 2) ∈ (0[,]1))
75		simprl 769	. . . . . . . . 9 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 2))
76	75	oveq2d 7440	. . . . . . . 8 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (2 · (1 / 2)))
77		2cn 12339	. . . . . . . . 9 ⊢ 2 ∈ ℂ
78		2ne0 12368	. . . . . . . . 9 ⊢ 2 ≠ 0
79	77, 78	recidi 11996	. . . . . . . 8 ⊢ (2 · (1 / 2)) = 1
80	76, 79	eqtrdi 2782	. . . . . . 7 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = 1)
81	80	oveq1d 7439	. . . . . 6 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ((2 · 𝑦) − 1) = (1 − 1))
82		1m1e0 12336	. . . . . 6 ⊢ (1 − 1) = 0
83	81, 82	eqtr2di 2783	. . . . 5 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → 0 = ((2 · 𝑦) − 1))
84		retopon 24771	. . . . . . . 8 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
85		iccssre 13460	. . . . . . . . 9 ⊢ ((0 ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆ ℝ)
86	64, 68, 85	mp2an 690	. . . . . . . 8 ⊢ (0[,](1 / 2)) ⊆ ℝ
87		resttopon 23156	. . . . . . . 8 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2))))
88	84, 86, 87	mp2an 690	. . . . . . 7 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2)))
89	88	a1i 11	. . . . . 6 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → ((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2))))
90	89, 56, 56, 58	cnmpt2c 23665	. . . . 5 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑦 ∈ (0[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ 0) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ×_t II) Cn II))
91		iccssre 13460	. . . . . . . . 9 ⊢ (((1 / 2) ∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆ ℝ)
92	68, 66, 91	mp2an 690	. . . . . . . 8 ⊢ ((1 / 2)[,]1) ⊆ ℝ
93		resttopon 23156	. . . . . . . 8 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 / 2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1)))
94	84, 92, 93	mp2an 690	. . . . . . 7 ⊢ ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1))
95	94	a1i 11	. . . . . 6 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1)))
96	95, 56	cnmpt1st 23663	. . . . . 6 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑦 ∈ ((1 / 2)[,]1), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ×_t II) Cn ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1))))
97	62	iihalf2cn 24947	. . . . . . 7 ⊢ (𝑥 ∈ ((1 / 2)[,]1) ↦ ((2 · 𝑥) − 1)) ∈ (((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) Cn II)
98	97	a1i 11	. . . . . 6 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑥 ∈ ((1 / 2)[,]1) ↦ ((2 · 𝑥) − 1)) ∈ (((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) Cn II))
99		oveq2 7432	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
100	99	oveq1d 7439	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1))
101	95, 56, 96, 95, 98, 100	cnmpt21 23666	. . . . 5 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑦 ∈ ((1 / 2)[,]1), 𝑧 ∈ (0[,]1) ↦ ((2 · 𝑦) − 1)) ∈ ((((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ×_t II) Cn II))
102	60, 61, 62, 63, 65, 67, 74, 56, 83, 90, 101	cnmpopc 24940	. . . 4 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), 0, ((2 · 𝑦) − 1))) ∈ ((II ×_t II) Cn II))
103		breq1 5156	. . . . . 6 ⊢ (𝑦 = 𝑥 → (𝑦 ≤ (1 / 2) ↔ 𝑥 ≤ (1 / 2)))
104		oveq2 7432	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (2 · 𝑦) = (2 · 𝑥))
105	104	oveq1d 7439	. . . . . 6 ⊢ (𝑦 = 𝑥 → ((2 · 𝑦) − 1) = ((2 · 𝑥) − 1))
106	103, 105	ifbieq2d 4559	. . . . 5 ⊢ (𝑦 = 𝑥 → if(𝑦 ≤ (1 / 2), 0, ((2 · 𝑦) − 1)) = if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)))
107	106	adantr 479	. . . 4 ⊢ ((𝑦 = 𝑥 ∧ 𝑧 = 0) → if(𝑦 ≤ (1 / 2), 0, ((2 · 𝑦) − 1)) = if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)))
108	56, 57, 59, 56, 56, 102, 107	cnmpt12 23662	. . 3 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1))) ∈ (II Cn II))
109		id 22	. . . . . . 7 ⊢ (𝑥 = 0 → 𝑥 = 0)
110	109, 69	eqbrtrdi 5192	. . . . . 6 ⊢ (𝑥 = 0 → 𝑥 ≤ (1 / 2))
111	110, 43	syl 17	. . . . 5 ⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)) = 0)
112		c0ex 11258	. . . . 5 ⊢ 0 ∈ V
113	111, 47, 112	fvmpt 7009	. . . 4 ⊢ (0 ∈ (0[,]1) → ((𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)))‘0) = 0)
114	8, 113	mp1i 13	. . 3 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → ((𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)))‘0) = 0)
115		1elunit 13501	. . . 4 ⊢ 1 ∈ (0[,]1)
116	68, 66	ltnlei 11385	. . . . . . . . 9 ⊢ ((1 / 2) < 1 ↔ ¬ 1 ≤ (1 / 2))
117	70, 116	mpbi 229	. . . . . . . 8 ⊢ ¬ 1 ≤ (1 / 2)
118		breq1 5156	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑥 ≤ (1 / 2) ↔ 1 ≤ (1 / 2)))
119	117, 118	mtbiri 326	. . . . . . 7 ⊢ (𝑥 = 1 → ¬ 𝑥 ≤ (1 / 2))
120	119, 36	syl 17	. . . . . 6 ⊢ (𝑥 = 1 → if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)) = ((2 · 𝑥) − 1))
121		oveq2 7432	. . . . . . . . 9 ⊢ (𝑥 = 1 → (2 · 𝑥) = (2 · 1))
122		2t1e2 12427	. . . . . . . . 9 ⊢ (2 · 1) = 2
123	121, 122	eqtrdi 2782	. . . . . . . 8 ⊢ (𝑥 = 1 → (2 · 𝑥) = 2)
124	123	oveq1d 7439	. . . . . . 7 ⊢ (𝑥 = 1 → ((2 · 𝑥) − 1) = (2 − 1))
125		2m1e1 12390	. . . . . . 7 ⊢ (2 − 1) = 1
126	124, 125	eqtrdi 2782	. . . . . 6 ⊢ (𝑥 = 1 → ((2 · 𝑥) − 1) = 1)
127	120, 126	eqtrd 2766	. . . . 5 ⊢ (𝑥 = 1 → if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)) = 1)
128		1ex 11260	. . . . 5 ⊢ 1 ∈ V
129	127, 47, 128	fvmpt 7009	. . . 4 ⊢ (1 ∈ (0[,]1) → ((𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)))‘1) = 1)
130	115, 129	mp1i 13	. . 3 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → ((𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)))‘1) = 1)
131	34, 108, 114, 130	reparpht 25016	. 2 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝐹 ∘ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1))))( ≃_ph‘𝐽)𝐹)
132	54, 131	eqbrtrd 5175	1 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑃(*_𝑝‘𝐽)𝐹)( ≃_ph‘𝐽)𝐹)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 394 ∧ w3a 1084 = wceq 1534 ∈ wcel 2099 ⊆ wss 3947 ifcif 4533 {csn 4633 ∪ cuni 4913 class class class wbr 5153 ↦ cmpt 5236 × cxp 5680 ran crn 5683 ∘ ccom 5686 ⟶wf 6550 ‘cfv 6554 (class class class)co 7424 ℝcr 11157 0cc0 11158 1c1 11159 · cmul 11163 < clt 11298 ≤ cle 11299 − cmin 11494 / cdiv 11921 2c2 12319 (,)cioo 13378 [,]cicc 13381 ↾_t crest 17435 topGenctg 17452 Topctop 22886 TopOnctopon 22903 Cn ccn 23219 IIcii 24886 ≃_phcphtpc 24986 *_𝑝cpco 25018

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-rep 5290 ax-sep 5304 ax-nul 5311 ax-pow 5369 ax-pr 5433 ax-un 7746 ax-cnex 11214 ax-resscn 11215 ax-1cn 11216 ax-icn 11217 ax-addcl 11218 ax-addrcl 11219 ax-mulcl 11220 ax-mulrcl 11221 ax-mulcom 11222 ax-addass 11223 ax-mulass 11224 ax-distr 11225 ax-i2m1 11226 ax-1ne0 11227 ax-1rid 11228 ax-rnegex 11229 ax-rrecex 11230 ax-cnre 11231 ax-pre-lttri 11232 ax-pre-lttrn 11233 ax-pre-ltadd 11234 ax-pre-mulgt0 11235 ax-pre-sup 11236 ax-addf 11237

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3464 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3967 df-nul 4326 df-if 4534 df-pw 4609 df-sn 4634 df-pr 4636 df-tp 4638 df-op 4640 df-uni 4914 df-int 4955 df-iun 5003 df-iin 5004 df-br 5154 df-opab 5216 df-mpt 5237 df-tr 5271 df-id 5580 df-eprel 5586 df-po 5594 df-so 5595 df-fr 5637 df-se 5638 df-we 5639 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-pred 6312 df-ord 6379 df-on 6380 df-lim 6381 df-suc 6382 df-iota 6506 df-fun 6556 df-fn 6557 df-f 6558 df-f1 6559 df-fo 6560 df-f1o 6561 df-fv 6562 df-isom 6563 df-riota 7380 df-ov 7427 df-oprab 7428 df-mpo 7429 df-of 7690 df-om 7877 df-1st 8003 df-2nd 8004 df-supp 8175 df-frecs 8296 df-wrecs 8327 df-recs 8401 df-rdg 8440 df-1o 8496 df-2o 8497 df-er 8734 df-map 8857 df-ixp 8927 df-en 8975 df-dom 8976 df-sdom 8977 df-fin 8978 df-fsupp 9406 df-fi 9454 df-sup 9485 df-inf 9486 df-oi 9553 df-card 9982 df-pnf 11300 df-mnf 11301 df-xr 11302 df-ltxr 11303 df-le 11304 df-sub 11496 df-neg 11497 df-div 11922 df-nn 12265 df-2 12327 df-3 12328 df-4 12329 df-5 12330 df-6 12331 df-7 12332 df-8 12333 df-9 12334 df-n0 12525 df-z 12611 df-dec 12730 df-uz 12875 df-q 12985 df-rp 13029 df-xneg 13146 df-xadd 13147 df-xmul 13148 df-ioo 13382 df-icc 13385 df-fz 13539 df-fzo 13682 df-seq 14022 df-exp 14082 df-hash 14348 df-cj 15104 df-re 15105 df-im 15106 df-sqrt 15240 df-abs 15241 df-struct 17149 df-sets 17166 df-slot 17184 df-ndx 17196 df-base 17214 df-ress 17243 df-plusg 17279 df-mulr 17280 df-starv 17281 df-sca 17282 df-vsca 17283 df-ip 17284 df-tset 17285 df-ple 17286 df-ds 17288 df-unif 17289 df-hom 17290 df-cco 17291 df-rest 17437 df-topn 17438 df-0g 17456 df-gsum 17457 df-topgen 17458 df-pt 17459 df-prds 17462 df-xrs 17517 df-qtop 17522 df-imas 17523 df-xps 17525 df-mre 17599 df-mrc 17600 df-acs 17602 df-mgm 18633 df-sgrp 18712 df-mnd 18728 df-submnd 18774 df-mulg 19062 df-cntz 19311 df-cmn 19780 df-psmet 21335 df-xmet 21336 df-met 21337 df-bl 21338 df-mopn 21339 df-cnfld 21344 df-top 22887 df-topon 22904 df-topsp 22926 df-bases 22940 df-cld 23014 df-cn 23222 df-cnp 23223 df-tx 23557 df-hmeo 23750 df-xms 24317 df-ms 24318 df-tms 24319 df-ii 24888 df-htpy 24987 df-phtpy 24988 df-phtpc 25009 df-pco 25023

This theorem is referenced by: pcophtb 25047 pi1grplem 25067 pi1xfr 25073 pi1xfrcnvlem 25074

W3C validator