pcorevlem - Metamath Proof Explorer

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

Theorem pcorevlem 25260

Description: Lemma for pcorev 25261. Prove continuity of the homotopy function. (Contributed by Jeff Madsen, 11-Jun-2010.) (Proof shortened by Mario Carneiro, 8-Jun-2014.)

**Hypotheses**
Ref	Expression
pcorev.1	⊢ 𝐺 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥)))
pcorev.2	⊢ 𝑃 = ((0[,]1) × {(𝐹‘1)})
pcorevlem.3	⊢ 𝐻 = (𝑠 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ (𝐹‘if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1)))))))

**Assertion**
Ref	Expression
pcorevlem	⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐻 ∈ ((𝐺(_𝑝‘𝐽)𝐹)(PHtpy‘𝐽)𝑃) ∧ (𝐺(_𝑝‘𝐽)𝐹)( ≃_ph‘𝐽)𝑃))

Distinct variable groups: 𝑡,𝑠,𝑥,𝐹 𝐺,𝑠,𝑡 𝐽,𝑠,𝑡,𝑥 𝑃,𝑠,𝑡,𝑥 Allowed substitution hints: 𝐺(𝑥) 𝐻(𝑥, 𝑡, 𝑠)

Proof of Theorem pcorevlem Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pcorev.1	. . . . 5 ⊢ 𝐺 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥)))
2		iitopon 25113	. . . . . . 7 ⊢ II ∈ (TopOn‘(0[,]1))
3	2	a1i 11	. . . . . 6 ⊢ (𝐹 ∈ (II Cn 𝐽) → II ∈ (TopOn‘(0[,]1)))
4		iirevcn 25164	. . . . . . 7 ⊢ (𝑥 ∈ (0[,]1) ↦ (1 − 𝑥)) ∈ (II Cn II)
5	4	a1i 11	. . . . . 6 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑥 ∈ (0[,]1) ↦ (1 − 𝑥)) ∈ (II Cn II))
6		id 23	. . . . . 6 ⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐹 ∈ (II Cn 𝐽))
7	3, 5, 6	cnmpt11f 23896	. . . . 5 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥))) ∈ (II Cn 𝐽))
8	1, 7	eqeltrid 2866	. . . 4 ⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐺 ∈ (II Cn 𝐽))
9		1elunit 13527	. . . . 5 ⊢ 1 ∈ (0[,]1)
10		oveq2 7425	. . . . . . . 8 ⊢ (𝑥 = 1 → (1 − 𝑥) = (1 − 1))
11		1m1e0 12341	. . . . . . . 8 ⊢ (1 − 1) = 0
12	10, 11	eqtrdi 2813	. . . . . . 7 ⊢ (𝑥 = 1 → (1 − 𝑥) = 0)
13	12	fveq2d 6886	. . . . . 6 ⊢ (𝑥 = 1 → (𝐹‘(1 − 𝑥)) = (𝐹‘0))
14		fvex 6895	. . . . . 6 ⊢ (𝐹‘0) ∈ V
15	13, 1, 14	fvmpt 6990	. . . . 5 ⊢ (1 ∈ (0[,]1) → (𝐺‘1) = (𝐹‘0))
16	9, 15	mp1i 14	. . . 4 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐺‘1) = (𝐹‘0))
17	8, 6, 16	pcocn 25251	. . 3 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐺(*_𝑝‘𝐽)𝐹) ∈ (II Cn 𝐽))
18		cntop2 23472	. . . . . 6 ⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐽 ∈ Top)
19		toptopon2 23149	. . . . . 6 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))
20	18, 19	sylib 221	. . . . 5 ⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐽 ∈ (TopOn‘∪ 𝐽))
21		iiuni 25115	. . . . . . 7 ⊢ (0[,]1) = ∪ II
22		eqid 2762	. . . . . . 7 ⊢ ∪ 𝐽 = ∪ 𝐽
23	21, 22	cnf 23477	. . . . . 6 ⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐹:(0[,]1)⟶∪ 𝐽)
24		ffvelcdm 7078	. . . . . 6 ⊢ ((𝐹:(0[,]1)⟶∪ 𝐽 ∧ 1 ∈ (0[,]1)) → (𝐹‘1) ∈ ∪ 𝐽)
25	23, 9, 24	sylancl 598	. . . . 5 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐹‘1) ∈ ∪ 𝐽)
26		pcorev.2	. . . . . 6 ⊢ 𝑃 = ((0[,]1) × {(𝐹‘1)})
27	26	pcoptcl 25255	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ (𝐹‘1) ∈ ∪ 𝐽) → (𝑃 ∈ (II Cn 𝐽) ∧ (𝑃‘0) = (𝐹‘1) ∧ (𝑃‘1) = (𝐹‘1)))
28	20, 25, 27	syl2anc 596	. . . 4 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑃 ∈ (II Cn 𝐽) ∧ (𝑃‘0) = (𝐹‘1) ∧ (𝑃‘1) = (𝐹‘1)))
29	28	simp1d 1160	. . 3 ⊢ (𝐹 ∈ (II Cn 𝐽) → 𝑃 ∈ (II Cn 𝐽))
30		pcorevlem.3	. . . 4 ⊢ 𝐻 = (𝑠 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ (𝐹‘if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1)))))))
31		eqid 2762	. . . . . 6 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
32		eqid 2762	. . . . . 6 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 2))) = ((topGen‘ran (,)) ↾_t (0[,](1 / 2)))
33		eqid 2762	. . . . . 6 ⊢ ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) = ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1))
34		dfii2 25116	. . . . . 6 ⊢ II = ((topGen‘ran (,)) ↾_t (0[,]1))
35		0red 11239	. . . . . 6 ⊢ (𝐹 ∈ (II Cn 𝐽) → 0 ∈ ℝ)
36		1red 11237	. . . . . 6 ⊢ (𝐹 ∈ (II Cn 𝐽) → 1 ∈ ℝ)
37		halfre 12485	. . . . . . . 8 ⊢ (1 / 2) ∈ ℝ
38		halfge0 12488	. . . . . . . 8 ⊢ 0 ≤ (1 / 2)
39		1re 11236	. . . . . . . . 9 ⊢ 1 ∈ ℝ
40		halflt1 12489	. . . . . . . . 9 ⊢ (1 / 2) < 1
41	37, 39, 40	ltleii 11361	. . . . . . . 8 ⊢ (1 / 2) ≤ 1
42		elicc01 13523	. . . . . . . 8 ⊢ ((1 / 2) ∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 / 2) ≤ 1))
43	37, 38, 41, 42	mpbir3an 1360	. . . . . . 7 ⊢ (1 / 2) ∈ (0[,]1)
44	43	a1i 11	. . . . . 6 ⊢ (𝐹 ∈ (II Cn 𝐽) → (1 / 2) ∈ (0[,]1))
45		simprl 783	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → 𝑠 = (1 / 2))
46	45	oveq2d 7433	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → (2 · 𝑠) = (2 · (1 / 2)))
47		2thalfe1 12376	. . . . . . . . . 10 ⊢ (2 · (1 / 2)) = 1
48	46, 47	eqtrdi 2813	. . . . . . . . 9 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → (2 · 𝑠) = 1)
49	48	oveq1d 7432	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → ((2 · 𝑠) − 1) = (1 − 1))
50	49, 11	eqtrdi 2813	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → ((2 · 𝑠) − 1) = 0)
51	50	oveq2d 7433	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → (1 − ((2 · 𝑠) − 1)) = (1 − 0))
52		1m0e1 12388	. . . . . . . . . 10 ⊢ (1 − 0) = 1
53	51, 52	eqtrdi 2813	. . . . . . . . 9 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → (1 − ((2 · 𝑠) − 1)) = 1)
54	48, 53	eqtr4d 2800	. . . . . . . 8 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → (2 · 𝑠) = (1 − ((2 · 𝑠) − 1)))
55	54	oveq2d 7433	. . . . . . 7 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → ((1 − 𝑡) · (2 · 𝑠)) = ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))))
56	55	oveq2d 7433	. . . . . 6 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → (1 − ((1 − 𝑡) · (2 · 𝑠))) = (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1)))))
57		retopon 24995	. . . . . . . . 9 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
58		0re 11238	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
59		iccssre 13486	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆ ℝ)
60	58, 37, 59	mp2an 705	. . . . . . . . 9 ⊢ (0[,](1 / 2)) ⊆ ℝ
61		resttopon 23392	. . . . . . . . 9 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2))))
62	57, 60, 61	mp2an 705	. . . . . . . 8 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2)))
63	62	a1i 11	. . . . . . 7 ⊢ (𝐹 ∈ (II Cn 𝐽) → ((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2))))
64	63, 3	cnmpt2nd 23901	. . . . . . . . 9 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,](1 / 2)), 𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ×_t II) Cn II))
65		oveq2 7425	. . . . . . . . 9 ⊢ (𝑥 = 𝑡 → (1 − 𝑥) = (1 − 𝑡))
66	63, 3, 64, 3, 5, 65	cnmpt21 23903	. . . . . . . 8 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,](1 / 2)), 𝑡 ∈ (0[,]1) ↦ (1 − 𝑡)) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ×_t II) Cn II))
67	63, 3	cnmpt1st 23900	. . . . . . . . 9 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,](1 / 2)), 𝑡 ∈ (0[,]1) ↦ 𝑠) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ×_t II) Cn ((topGen‘ran (,)) ↾_t (0[,](1 / 2)))))
68	32	iihalf1cn 25166	. . . . . . . . . 10 ⊢ (𝑥 ∈ (0[,](1 / 2)) ↦ (2 · 𝑥)) ∈ (((topGen‘ran (,)) ↾_t (0[,](1 / 2))) Cn II)
69	68	a1i 11	. . . . . . . . 9 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑥 ∈ (0[,](1 / 2)) ↦ (2 · 𝑥)) ∈ (((topGen‘ran (,)) ↾_t (0[,](1 / 2))) Cn II))
70		oveq2 7425	. . . . . . . . 9 ⊢ (𝑥 = 𝑠 → (2 · 𝑥) = (2 · 𝑠))
71	63, 3, 67, 63, 69, 70	cnmpt21 23903	. . . . . . . 8 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,](1 / 2)), 𝑡 ∈ (0[,]1) ↦ (2 · 𝑠)) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ×_t II) Cn II))
72		iimulcn 25172	. . . . . . . . 9 ⊢ (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝑥 · 𝑦)) ∈ ((II ×_t II) Cn II)
73	72	a1i 11	. . . . . . . 8 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝑥 · 𝑦)) ∈ ((II ×_t II) Cn II))
74		oveq12 7426	. . . . . . . 8 ⊢ ((𝑥 = (1 − 𝑡) ∧ 𝑦 = (2 · 𝑠)) → (𝑥 · 𝑦) = ((1 − 𝑡) · (2 · 𝑠)))
75	63, 3, 66, 71, 3, 3, 73, 74	cnmpt22 23906	. . . . . . 7 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,](1 / 2)), 𝑡 ∈ (0[,]1) ↦ ((1 − 𝑡) · (2 · 𝑠))) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ×_t II) Cn II))
76		oveq2 7425	. . . . . . 7 ⊢ (𝑥 = ((1 − 𝑡) · (2 · 𝑠)) → (1 − 𝑥) = (1 − ((1 − 𝑡) · (2 · 𝑠))))
77	63, 3, 75, 3, 5, 76	cnmpt21 23903	. . . . . 6 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,](1 / 2)), 𝑡 ∈ (0[,]1) ↦ (1 − ((1 − 𝑡) · (2 · 𝑠)))) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ×_t II) Cn II))
78		iccssre 13486	. . . . . . . . . 10 ⊢ (((1 / 2) ∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆ ℝ)
79	37, 39, 78	mp2an 705	. . . . . . . . 9 ⊢ ((1 / 2)[,]1) ⊆ ℝ
80		resttopon 23392	. . . . . . . . 9 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 / 2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1)))
81	57, 79, 80	mp2an 705	. . . . . . . 8 ⊢ ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1))
82	81	a1i 11	. . . . . . 7 ⊢ (𝐹 ∈ (II Cn 𝐽) → ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1)))
83	82, 3	cnmpt2nd 23901	. . . . . . . . 9 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ×_t II) Cn II))
84	82, 3, 83, 3, 5, 65	cnmpt21 23903	. . . . . . . 8 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ (1 − 𝑡)) ∈ ((((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ×_t II) Cn II))
85	82, 3	cnmpt1st 23900	. . . . . . . . . 10 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ 𝑠) ∈ ((((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ×_t II) Cn ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1))))
86	33	iihalf2cn 25168	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((1 / 2)[,]1) ↦ ((2 · 𝑥) − 1)) ∈ (((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) Cn II)
87	86	a1i 11	. . . . . . . . . 10 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑥 ∈ ((1 / 2)[,]1) ↦ ((2 · 𝑥) − 1)) ∈ (((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) Cn II))
88	70	oveq1d 7432	. . . . . . . . . 10 ⊢ (𝑥 = 𝑠 → ((2 · 𝑥) − 1) = ((2 · 𝑠) − 1))
89	82, 3, 85, 82, 87, 88	cnmpt21 23903	. . . . . . . . 9 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ ((2 · 𝑠) − 1)) ∈ ((((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ×_t II) Cn II))
90		oveq2 7425	. . . . . . . . 9 ⊢ (𝑥 = ((2 · 𝑠) − 1) → (1 − 𝑥) = (1 − ((2 · 𝑠) − 1)))
91	82, 3, 89, 3, 5, 90	cnmpt21 23903	. . . . . . . 8 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ (1 − ((2 · 𝑠) − 1))) ∈ ((((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ×_t II) Cn II))
92		oveq12 7426	. . . . . . . 8 ⊢ ((𝑥 = (1 − 𝑡) ∧ 𝑦 = (1 − ((2 · 𝑠) − 1))) → (𝑥 · 𝑦) = ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))))
93	82, 3, 84, 91, 3, 3, 73, 92	cnmpt22 23906	. . . . . . 7 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1)))) ∈ ((((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ×_t II) Cn II))
94		oveq2 7425	. . . . . . 7 ⊢ (𝑥 = ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))) → (1 − 𝑥) = (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1)))))
95	82, 3, 93, 3, 5, 94	cnmpt21 23903	. . . . . 6 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))))) ∈ ((((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ×_t II) Cn II))
96	31, 32, 33, 34, 35, 36, 44, 3, 56, 77, 95	cnmpopc 25162	. . . . 5 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1)))))) ∈ ((II ×_t II) Cn II))
97	3, 3, 96, 6	cnmpt21f 23904	. . . 4 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ (𝐹‘if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))))))) ∈ ((II ×_t II) Cn 𝐽))
98	30, 97	eqeltrid 2866	. . 3 ⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐻 ∈ ((II ×_t II) Cn 𝐽))
99		simpr 490	. . . . 5 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → 𝑦 ∈ (0[,]1))
100		0elunit 13526	. . . . 5 ⊢ 0 ∈ (0[,]1)
101		simpl 488	. . . . . . . . 9 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → 𝑠 = 𝑦)
102	101	breq1d 5117	. . . . . . . 8 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (𝑠 ≤ (1 / 2) ↔ 𝑦 ≤ (1 / 2)))
103		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → 𝑡 = 0)
104	103	oveq2d 7433	. . . . . . . . . . 11 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (1 − 𝑡) = (1 − 0))
105	104, 52	eqtrdi 2813	. . . . . . . . . 10 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (1 − 𝑡) = 1)
106	101	oveq2d 7433	. . . . . . . . . 10 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (2 · 𝑠) = (2 · 𝑦))
107	105, 106	oveq12d 7435	. . . . . . . . 9 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → ((1 − 𝑡) · (2 · 𝑠)) = (1 · (2 · 𝑦)))
108	107	oveq2d 7433	. . . . . . . 8 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (1 − ((1 − 𝑡) · (2 · 𝑠))) = (1 − (1 · (2 · 𝑦))))
109	106	oveq1d 7432	. . . . . . . . . . 11 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → ((2 · 𝑠) − 1) = ((2 · 𝑦) − 1))
110	109	oveq2d 7433	. . . . . . . . . 10 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (1 − ((2 · 𝑠) − 1)) = (1 − ((2 · 𝑦) − 1)))
111	105, 110	oveq12d 7435	. . . . . . . . 9 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))) = (1 · (1 − ((2 · 𝑦) − 1))))
112	111	oveq2d 7433	. . . . . . . 8 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1)))) = (1 − (1 · (1 − ((2 · 𝑦) − 1)))))
113	102, 108, 112	ifbieq12d 4514	. . . . . . 7 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))))) = if(𝑦 ≤ (1 / 2), (1 − (1 · (2 · 𝑦))), (1 − (1 · (1 − ((2 · 𝑦) − 1))))))
114	113	fveq2d 6886	. . . . . 6 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (𝐹‘if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1)))))) = (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2 · 𝑦))), (1 − (1 · (1 − ((2 · 𝑦) − 1)))))))
115		fvex 6895	. . . . . 6 ⊢ (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2 · 𝑦))), (1 − (1 · (1 − ((2 · 𝑦) − 1)))))) ∈ V
116	114, 30, 115	ovmpoa 7572	. . . . 5 ⊢ ((𝑦 ∈ (0[,]1) ∧ 0 ∈ (0[,]1)) → (𝑦𝐻0) = (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2 · 𝑦))), (1 − (1 · (1 − ((2 · 𝑦) − 1)))))))
117	99, 100, 116	sylancl 598	. . . 4 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝑦𝐻0) = (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2 · 𝑦))), (1 − (1 · (1 − ((2 · 𝑦) − 1)))))))
118		iftrue 4491	. . . . . . . 8 ⊢ (𝑦 ≤ (1 / 2) → if(𝑦 ≤ (1 / 2), (1 − (1 · (2 · 𝑦))), (1 − (1 · (1 − ((2 · 𝑦) − 1))))) = (1 − (1 · (2 · 𝑦))))
119	118	adantl 487	. . . . . . 7 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ 𝑦 ≤ (1 / 2)) → if(𝑦 ≤ (1 / 2), (1 − (1 · (2 · 𝑦))), (1 − (1 · (1 − ((2 · 𝑦) − 1))))) = (1 − (1 · (2 · 𝑦))))
120	119	fveq2d 6886	. . . . . 6 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ 𝑦 ≤ (1 / 2)) → (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2 · 𝑦))), (1 − (1 · (1 − ((2 · 𝑦) − 1)))))) = (𝐹‘(1 − (1 · (2 · 𝑦)))))
121		elii1 25169	. . . . . . . 8 ⊢ (𝑦 ∈ (0[,](1 / 2)) ↔ (𝑦 ∈ (0[,]1) ∧ 𝑦 ≤ (1 / 2)))
122	8, 6	pcoval1 25247	. . . . . . . . 9 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,](1 / 2))) → ((𝐺(*_𝑝‘𝐽)𝐹)‘𝑦) = (𝐺‘(2 · 𝑦)))
123		iihalf1 25165	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (0[,](1 / 2)) → (2 · 𝑦) ∈ (0[,]1))
124	123	adantl 487	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,](1 / 2))) → (2 · 𝑦) ∈ (0[,]1))
125		oveq2 7425	. . . . . . . . . . . . 13 ⊢ (𝑥 = (2 · 𝑦) → (1 − 𝑥) = (1 − (2 · 𝑦)))
126	125	fveq2d 6886	. . . . . . . . . . . 12 ⊢ (𝑥 = (2 · 𝑦) → (𝐹‘(1 − 𝑥)) = (𝐹‘(1 − (2 · 𝑦))))
127		fvex 6895	. . . . . . . . . . . 12 ⊢ (𝐹‘(1 − (2 · 𝑦))) ∈ V
128	126, 1, 127	fvmpt 6990	. . . . . . . . . . 11 ⊢ ((2 · 𝑦) ∈ (0[,]1) → (𝐺‘(2 · 𝑦)) = (𝐹‘(1 − (2 · 𝑦))))
129		unitssre 13556	. . . . . . . . . . . . . . . 16 ⊢ (0[,]1) ⊆ ℝ
130	129	sseli 3930	. . . . . . . . . . . . . . 15 ⊢ ((2 · 𝑦) ∈ (0[,]1) → (2 · 𝑦) ∈ ℝ)
131	130	recnd 11265	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑦) ∈ (0[,]1) → (2 · 𝑦) ∈ ℂ)
132	131	mullidd 11255	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑦) ∈ (0[,]1) → (1 · (2 · 𝑦)) = (2 · 𝑦))
133	132	oveq2d 7433	. . . . . . . . . . . 12 ⊢ ((2 · 𝑦) ∈ (0[,]1) → (1 − (1 · (2 · 𝑦))) = (1 − (2 · 𝑦)))
134	133	fveq2d 6886	. . . . . . . . . . 11 ⊢ ((2 · 𝑦) ∈ (0[,]1) → (𝐹‘(1 − (1 · (2 · 𝑦)))) = (𝐹‘(1 − (2 · 𝑦))))
135	128, 134	eqtr4d 2800	. . . . . . . . . 10 ⊢ ((2 · 𝑦) ∈ (0[,]1) → (𝐺‘(2 · 𝑦)) = (𝐹‘(1 − (1 · (2 · 𝑦)))))
136	124, 135	syl 18	. . . . . . . . 9 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,](1 / 2))) → (𝐺‘(2 · 𝑦)) = (𝐹‘(1 − (1 · (2 · 𝑦)))))
137	122, 136	eqtrd 2797	. . . . . . . 8 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,](1 / 2))) → ((𝐺(*_𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘(1 − (1 · (2 · 𝑦)))))
138	121, 137	sylan2br 607	. . . . . . 7 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑦 ∈ (0[,]1) ∧ 𝑦 ≤ (1 / 2))) → ((𝐺(*_𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘(1 − (1 · (2 · 𝑦)))))
139	138	anassrs 473	. . . . . 6 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ 𝑦 ≤ (1 / 2)) → ((𝐺(*_𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘(1 − (1 · (2 · 𝑦)))))
140	120, 139	eqtr4d 2800	. . . . 5 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ 𝑦 ≤ (1 / 2)) → (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2 · 𝑦))), (1 − (1 · (1 − ((2 · 𝑦) − 1)))))) = ((𝐺(*_𝑝‘𝐽)𝐹)‘𝑦))
141		iffalse 4494	. . . . . . . 8 ⊢ (¬ 𝑦 ≤ (1 / 2) → if(𝑦 ≤ (1 / 2), (1 − (1 · (2 · 𝑦))), (1 − (1 · (1 − ((2 · 𝑦) − 1))))) = (1 − (1 · (1 − ((2 · 𝑦) − 1)))))
142	141	adantl 487	. . . . . . 7 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ ¬ 𝑦 ≤ (1 / 2)) → if(𝑦 ≤ (1 / 2), (1 − (1 · (2 · 𝑦))), (1 − (1 · (1 − ((2 · 𝑦) − 1))))) = (1 − (1 · (1 − ((2 · 𝑦) − 1)))))
143	142	fveq2d 6886	. . . . . 6 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ ¬ 𝑦 ≤ (1 / 2)) → (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2 · 𝑦))), (1 − (1 · (1 − ((2 · 𝑦) − 1)))))) = (𝐹‘(1 − (1 · (1 − ((2 · 𝑦) − 1))))))
144		elii2 25170	. . . . . . . 8 ⊢ ((𝑦 ∈ (0[,]1) ∧ ¬ 𝑦 ≤ (1 / 2)) → 𝑦 ∈ ((1 / 2)[,]1))
145	8, 6, 16	pcoval2 25250	. . . . . . . . 9 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ ((1 / 2)[,]1)) → ((𝐺(*_𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘((2 · 𝑦) − 1)))
146		iihalf2 25167	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ((1 / 2)[,]1) → ((2 · 𝑦) − 1) ∈ (0[,]1))
147	146	adantl 487	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ ((1 / 2)[,]1)) → ((2 · 𝑦) − 1) ∈ (0[,]1))
148		ax-1cn 11186	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
149	129	sseli 3930	. . . . . . . . . . . . . . . 16 ⊢ (((2 · 𝑦) − 1) ∈ (0[,]1) → ((2 · 𝑦) − 1) ∈ ℝ)
150	149	recnd 11265	. . . . . . . . . . . . . . 15 ⊢ (((2 · 𝑦) − 1) ∈ (0[,]1) → ((2 · 𝑦) − 1) ∈ ℂ)
151		subcl 11484	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ ((2 · 𝑦) − 1) ∈ ℂ) → (1 − ((2 · 𝑦) − 1)) ∈ ℂ)
152	148, 150, 151	sylancr 599	. . . . . . . . . . . . . 14 ⊢ (((2 · 𝑦) − 1) ∈ (0[,]1) → (1 − ((2 · 𝑦) − 1)) ∈ ℂ)
153	152	mullidd 11255	. . . . . . . . . . . . 13 ⊢ (((2 · 𝑦) − 1) ∈ (0[,]1) → (1 · (1 − ((2 · 𝑦) − 1))) = (1 − ((2 · 𝑦) − 1)))
154	153	oveq2d 7433	. . . . . . . . . . . 12 ⊢ (((2 · 𝑦) − 1) ∈ (0[,]1) → (1 − (1 · (1 − ((2 · 𝑦) − 1)))) = (1 − (1 − ((2 · 𝑦) − 1))))
155		nncan 11515	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ ((2 · 𝑦) − 1) ∈ ℂ) → (1 − (1 − ((2 · 𝑦) − 1))) = ((2 · 𝑦) − 1))
156	148, 150, 155	sylancr 599	. . . . . . . . . . . 12 ⊢ (((2 · 𝑦) − 1) ∈ (0[,]1) → (1 − (1 − ((2 · 𝑦) − 1))) = ((2 · 𝑦) − 1))
157	154, 156	eqtr2d 2798	. . . . . . . . . . 11 ⊢ (((2 · 𝑦) − 1) ∈ (0[,]1) → ((2 · 𝑦) − 1) = (1 − (1 · (1 − ((2 · 𝑦) − 1)))))
158	147, 157	syl 18	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ ((1 / 2)[,]1)) → ((2 · 𝑦) − 1) = (1 − (1 · (1 − ((2 · 𝑦) − 1)))))
159	158	fveq2d 6886	. . . . . . . . 9 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ ((1 / 2)[,]1)) → (𝐹‘((2 · 𝑦) − 1)) = (𝐹‘(1 − (1 · (1 − ((2 · 𝑦) − 1))))))
160	145, 159	eqtrd 2797	. . . . . . . 8 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ ((1 / 2)[,]1)) → ((𝐺(*_𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘(1 − (1 · (1 − ((2 · 𝑦) − 1))))))
161	144, 160	sylan2 605	. . . . . . 7 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑦 ∈ (0[,]1) ∧ ¬ 𝑦 ≤ (1 / 2))) → ((𝐺(*_𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘(1 − (1 · (1 − ((2 · 𝑦) − 1))))))
162	161	anassrs 473	. . . . . 6 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ ¬ 𝑦 ≤ (1 / 2)) → ((𝐺(*_𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘(1 − (1 · (1 − ((2 · 𝑦) − 1))))))
163	143, 162	eqtr4d 2800	. . . . 5 ⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ ¬ 𝑦 ≤ (1 / 2)) → (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2 · 𝑦))), (1 − (1 · (1 − ((2 · 𝑦) − 1)))))) = ((𝐺(*_𝑝‘𝐽)𝐹)‘𝑦))
164	140, 163	pm2.61dan 825	. . . 4 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2 · 𝑦))), (1 − (1 · (1 − ((2 · 𝑦) − 1)))))) = ((𝐺(*_𝑝‘𝐽)𝐹)‘𝑦))
165	117, 164	eqtrd 2797	. . 3 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝑦𝐻0) = ((𝐺(*_𝑝‘𝐽)𝐹)‘𝑦))
166		2cn 12344	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
167	129	sseli 3930	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (0[,]1) → 𝑦 ∈ ℝ)
168	167	recnd 11265	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (0[,]1) → 𝑦 ∈ ℂ)
169		mulcl 11212	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (2 · 𝑦) ∈ ℂ)
170	166, 168, 169	sylancr 599	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (0[,]1) → (2 · 𝑦) ∈ ℂ)
171	170	adantl 487	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (2 · 𝑦) ∈ ℂ)
172	171	mul02d 11436	. . . . . . . . 9 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (0 · (2 · 𝑦)) = 0)
173	172	oveq2d 7433	. . . . . . . 8 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (1 − (0 · (2 · 𝑦))) = (1 − 0))
174	173, 52	eqtrdi 2813	. . . . . . 7 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (1 − (0 · (2 · 𝑦))) = 1)
175		subcl 11484	. . . . . . . . . . . 12 ⊢ (((2 · 𝑦) ∈ ℂ ∧ 1 ∈ ℂ) → ((2 · 𝑦) − 1) ∈ ℂ)
176	171, 148, 175	sylancl 598	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → ((2 · 𝑦) − 1) ∈ ℂ)
177	148, 176, 151	sylancr 599	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (1 − ((2 · 𝑦) − 1)) ∈ ℂ)
178	177	mul02d 11436	. . . . . . . . 9 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (0 · (1 − ((2 · 𝑦) − 1))) = 0)
179	178	oveq2d 7433	. . . . . . . 8 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (1 − (0 · (1 − ((2 · 𝑦) − 1)))) = (1 − 0))
180	179, 52	eqtrdi 2813	. . . . . . 7 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (1 − (0 · (1 − ((2 · 𝑦) − 1)))) = 1)
181	174, 180	ifeq12d 4507	. . . . . 6 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → if(𝑦 ≤ (1 / 2), (1 − (0 · (2 · 𝑦))), (1 − (0 · (1 − ((2 · 𝑦) − 1))))) = if(𝑦 ≤ (1 / 2), 1, 1))
182		ifid 4526	. . . . . 6 ⊢ if(𝑦 ≤ (1 / 2), 1, 1) = 1
183	181, 182	eqtrdi 2813	. . . . 5 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → if(𝑦 ≤ (1 / 2), (1 − (0 · (2 · 𝑦))), (1 − (0 · (1 − ((2 · 𝑦) − 1))))) = 1)
184	183	fveq2d 6886	. . . 4 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (0 · (2 · 𝑦))), (1 − (0 · (1 − ((2 · 𝑦) − 1)))))) = (𝐹‘1))
185		simpl 488	. . . . . . . . 9 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → 𝑠 = 𝑦)
186	185	breq1d 5117	. . . . . . . 8 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (𝑠 ≤ (1 / 2) ↔ 𝑦 ≤ (1 / 2)))
187		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → 𝑡 = 1)
188	187	oveq2d 7433	. . . . . . . . . . 11 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (1 − 𝑡) = (1 − 1))
189	188, 11	eqtrdi 2813	. . . . . . . . . 10 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (1 − 𝑡) = 0)
190	185	oveq2d 7433	. . . . . . . . . 10 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (2 · 𝑠) = (2 · 𝑦))
191	189, 190	oveq12d 7435	. . . . . . . . 9 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → ((1 − 𝑡) · (2 · 𝑠)) = (0 · (2 · 𝑦)))
192	191	oveq2d 7433	. . . . . . . 8 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (1 − ((1 − 𝑡) · (2 · 𝑠))) = (1 − (0 · (2 · 𝑦))))
193	190	oveq1d 7432	. . . . . . . . . . 11 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → ((2 · 𝑠) − 1) = ((2 · 𝑦) − 1))
194	193	oveq2d 7433	. . . . . . . . . 10 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (1 − ((2 · 𝑠) − 1)) = (1 − ((2 · 𝑦) − 1)))
195	189, 194	oveq12d 7435	. . . . . . . . 9 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))) = (0 · (1 − ((2 · 𝑦) − 1))))
196	195	oveq2d 7433	. . . . . . . 8 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1)))) = (1 − (0 · (1 − ((2 · 𝑦) − 1)))))
197	186, 192, 196	ifbieq12d 4514	. . . . . . 7 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))))) = if(𝑦 ≤ (1 / 2), (1 − (0 · (2 · 𝑦))), (1 − (0 · (1 − ((2 · 𝑦) − 1))))))
198	197	fveq2d 6886	. . . . . 6 ⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (𝐹‘if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1)))))) = (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (0 · (2 · 𝑦))), (1 − (0 · (1 − ((2 · 𝑦) − 1)))))))
199		fvex 6895	. . . . . 6 ⊢ (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (0 · (2 · 𝑦))), (1 − (0 · (1 − ((2 · 𝑦) − 1)))))) ∈ V
200	198, 30, 199	ovmpoa 7572	. . . . 5 ⊢ ((𝑦 ∈ (0[,]1) ∧ 1 ∈ (0[,]1)) → (𝑦𝐻1) = (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (0 · (2 · 𝑦))), (1 − (0 · (1 − ((2 · 𝑦) − 1)))))))
201	99, 9, 200	sylancl 598	. . . 4 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝑦𝐻1) = (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (0 · (2 · 𝑦))), (1 − (0 · (1 − ((2 · 𝑦) − 1)))))))
202	26	fveq1i 6883	. . . . 5 ⊢ (𝑃‘𝑦) = (((0[,]1) × {(𝐹‘1)})‘𝑦)
203		fvex 6895	. . . . . . 7 ⊢ (𝐹‘1) ∈ V
204	203	fvconst2 7207	. . . . . 6 ⊢ (𝑦 ∈ (0[,]1) → (((0[,]1) × {(𝐹‘1)})‘𝑦) = (𝐹‘1))
205	204	adantl 487	. . . . 5 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (((0[,]1) × {(𝐹‘1)})‘𝑦) = (𝐹‘1))
206	202, 205	eqtrid 2809	. . . 4 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝑃‘𝑦) = (𝐹‘1))
207	184, 201, 206	3eqtr4d 2807	. . 3 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝑦𝐻1) = (𝑃‘𝑦))
208		simpl 488	. . . . . . . . . . 11 ⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → 𝑠 = 0)
209	208, 38	eqbrtrdi 5148	. . . . . . . . . 10 ⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → 𝑠 ≤ (1 / 2))
210	209	iftrued 4493	. . . . . . . . 9 ⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))))) = (1 − ((1 − 𝑡) · (2 · 𝑠))))
211		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → 𝑡 = 𝑦)
212	211	oveq2d 7433	. . . . . . . . . . 11 ⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → (1 − 𝑡) = (1 − 𝑦))
213	208	oveq2d 7433	. . . . . . . . . . . 12 ⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → (2 · 𝑠) = (2 · 0))
214		2t0e0 12439	. . . . . . . . . . . 12 ⊢ (2 · 0) = 0
215	213, 214	eqtrdi 2813	. . . . . . . . . . 11 ⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → (2 · 𝑠) = 0)
216	212, 215	oveq12d 7435	. . . . . . . . . 10 ⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → ((1 − 𝑡) · (2 · 𝑠)) = ((1 − 𝑦) · 0))
217	216	oveq2d 7433	. . . . . . . . 9 ⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → (1 − ((1 − 𝑡) · (2 · 𝑠))) = (1 − ((1 − 𝑦) · 0)))
218	210, 217	eqtrd 2797	. . . . . . . 8 ⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))))) = (1 − ((1 − 𝑦) · 0)))
219	218	fveq2d 6886	. . . . . . 7 ⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → (𝐹‘if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1)))))) = (𝐹‘(1 − ((1 − 𝑦) · 0))))
220		fvex 6895	. . . . . . 7 ⊢ (𝐹‘(1 − ((1 − 𝑦) · 0))) ∈ V
221	219, 30, 220	ovmpoa 7572	. . . . . 6 ⊢ ((0 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) → (0𝐻𝑦) = (𝐹‘(1 − ((1 − 𝑦) · 0))))
222	100, 221	mpan 703	. . . . 5 ⊢ (𝑦 ∈ (0[,]1) → (0𝐻𝑦) = (𝐹‘(1 − ((1 − 𝑦) · 0))))
223		subcl 11484	. . . . . . . . . 10 ⊢ ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (1 − 𝑦) ∈ ℂ)
224	148, 168, 223	sylancr 599	. . . . . . . . 9 ⊢ (𝑦 ∈ (0[,]1) → (1 − 𝑦) ∈ ℂ)
225	224	mul01d 11437	. . . . . . . 8 ⊢ (𝑦 ∈ (0[,]1) → ((1 − 𝑦) · 0) = 0)
226	225	oveq2d 7433	. . . . . . 7 ⊢ (𝑦 ∈ (0[,]1) → (1 − ((1 − 𝑦) · 0)) = (1 − 0))
227	226, 52	eqtrdi 2813	. . . . . 6 ⊢ (𝑦 ∈ (0[,]1) → (1 − ((1 − 𝑦) · 0)) = 1)
228	227	fveq2d 6886	. . . . 5 ⊢ (𝑦 ∈ (0[,]1) → (𝐹‘(1 − ((1 − 𝑦) · 0))) = (𝐹‘1))
229	222, 228	eqtrd 2797	. . . 4 ⊢ (𝑦 ∈ (0[,]1) → (0𝐻𝑦) = (𝐹‘1))
230	8, 6	pco0 25248	. . . . 5 ⊢ (𝐹 ∈ (II Cn 𝐽) → ((𝐺(*_𝑝‘𝐽)𝐹)‘0) = (𝐺‘0))
231		oveq2 7425	. . . . . . . . 9 ⊢ (𝑥 = 0 → (1 − 𝑥) = (1 − 0))
232	231, 52	eqtrdi 2813	. . . . . . . 8 ⊢ (𝑥 = 0 → (1 − 𝑥) = 1)
233	232	fveq2d 6886	. . . . . . 7 ⊢ (𝑥 = 0 → (𝐹‘(1 − 𝑥)) = (𝐹‘1))
234	233, 1, 203	fvmpt 6990	. . . . . 6 ⊢ (0 ∈ (0[,]1) → (𝐺‘0) = (𝐹‘1))
235	100, 234	ax-mp 5	. . . . 5 ⊢ (𝐺‘0) = (𝐹‘1)
236	230, 235	eqtr2di 2814	. . . 4 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐹‘1) = ((𝐺(*_𝑝‘𝐽)𝐹)‘0))
237	229, 236	sylan9eqr 2819	. . 3 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (0𝐻𝑦) = ((𝐺(*_𝑝‘𝐽)𝐹)‘0))
238	37, 39	ltnlei 11359	. . . . . . . . . . . 12 ⊢ ((1 / 2) < 1 ↔ ¬ 1 ≤ (1 / 2))
239	40, 238	mpbi 233	. . . . . . . . . . 11 ⊢ ¬ 1 ≤ (1 / 2)
240		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → 𝑠 = 1)
241	240	breq1d 5117	. . . . . . . . . . 11 ⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (𝑠 ≤ (1 / 2) ↔ 1 ≤ (1 / 2)))
242	239, 241	mtbiri 330	. . . . . . . . . 10 ⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → ¬ 𝑠 ≤ (1 / 2))
243	242	iffalsed 4496	. . . . . . . . 9 ⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))))) = (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1)))))
244		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → 𝑡 = 𝑦)
245	244	oveq2d 7433	. . . . . . . . . . 11 ⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (1 − 𝑡) = (1 − 𝑦))
246	240	oveq2d 7433	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (2 · 𝑠) = (2 · 1))
247		2t1e2 12431	. . . . . . . . . . . . . . . 16 ⊢ (2 · 1) = 2
248	246, 247	eqtrdi 2813	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (2 · 𝑠) = 2)
249	248	oveq1d 7432	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → ((2 · 𝑠) − 1) = (2 − 1))
250		2m1e1 12393	. . . . . . . . . . . . . 14 ⊢ (2 − 1) = 1
251	249, 250	eqtrdi 2813	. . . . . . . . . . . . 13 ⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → ((2 · 𝑠) − 1) = 1)
252	251	oveq2d 7433	. . . . . . . . . . . 12 ⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (1 − ((2 · 𝑠) − 1)) = (1 − 1))
253	252, 11	eqtrdi 2813	. . . . . . . . . . 11 ⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (1 − ((2 · 𝑠) − 1)) = 0)
254	245, 253	oveq12d 7435	. . . . . . . . . 10 ⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))) = ((1 − 𝑦) · 0))
255	254	oveq2d 7433	. . . . . . . . 9 ⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1)))) = (1 − ((1 − 𝑦) · 0)))
256	243, 255	eqtrd 2797	. . . . . . . 8 ⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))))) = (1 − ((1 − 𝑦) · 0)))
257	256	fveq2d 6886	. . . . . . 7 ⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (𝐹‘if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1)))))) = (𝐹‘(1 − ((1 − 𝑦) · 0))))
258	257, 30, 220	ovmpoa 7572	. . . . . 6 ⊢ ((1 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) → (1𝐻𝑦) = (𝐹‘(1 − ((1 − 𝑦) · 0))))
259	9, 258	mpan 703	. . . . 5 ⊢ (𝑦 ∈ (0[,]1) → (1𝐻𝑦) = (𝐹‘(1 − ((1 − 𝑦) · 0))))
260	259, 228	eqtrd 2797	. . . 4 ⊢ (𝑦 ∈ (0[,]1) → (1𝐻𝑦) = (𝐹‘1))
261	8, 6	pco1 25249	. . . . 5 ⊢ (𝐹 ∈ (II Cn 𝐽) → ((𝐺(*_𝑝‘𝐽)𝐹)‘1) = (𝐹‘1))
262	261	eqcomd 2768	. . . 4 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐹‘1) = ((𝐺(*_𝑝‘𝐽)𝐹)‘1))
263	260, 262	sylan9eqr 2819	. . 3 ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (1𝐻𝑦) = ((𝐺(*_𝑝‘𝐽)𝐹)‘1))
264	17, 29, 98, 165, 207, 237, 263	isphtpy2d 25221	. 2 ⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐻 ∈ ((𝐺(*_𝑝‘𝐽)𝐹)(PHtpy‘𝐽)𝑃))
265	264	ne0d 4291	. . 3 ⊢ (𝐹 ∈ (II Cn 𝐽) → ((𝐺(*_𝑝‘𝐽)𝐹)(PHtpy‘𝐽)𝑃) ≠ ∅)
266		isphtpc 25228	. . 3 ⊢ ((𝐺(_𝑝‘𝐽)𝐹)( ≃_ph‘𝐽)𝑃 ↔ ((𝐺(_𝑝‘𝐽)𝐹) ∈ (II Cn 𝐽) ∧ 𝑃 ∈ (II Cn 𝐽) ∧ ((𝐺(*_𝑝‘𝐽)𝐹)(PHtpy‘𝐽)𝑃) ≠ ∅))
267	17, 29, 265, 266	syl3anbrc 1362	. 2 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐺(*_𝑝‘𝐽)𝐹)( ≃_ph‘𝐽)𝑃)
268	264, 267	jca 521	1 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐻 ∈ ((𝐺(_𝑝‘𝐽)𝐹)(PHtpy‘𝐽)𝑃) ∧ (𝐺(_𝑝‘𝐽)𝐹)( ≃_ph‘𝐽)𝑃))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2957 ⊆ wss 3902 ∅c0 4282 ifcif 4485 {csn 4587 ∪ cuni 4870 class class class wbr 5107 ↦ cmpt 5190 × cxp 5657 ran crn 5660 ⟶wf 6533 ‘cfv 6537 (class class class)co 7417 ∈ cmpo 7419 ℂcc 11126 ℝcr 11127 0cc0 11128 1c1 11129 · cmul 11133 < clt 11271 ≤ cle 11272 − cmin 11469 / cdiv 11899 2c2 12323 (,)cioo 13402 [,]cicc 13405 ↾_t crest 17511 topGenctg 17528 Topctop 23124 TopOnctopon 23141 Cn ccn 23455 ×_t ctx 23792 IIcii 25109 PHtpycphtpy 25202 ≃_phcphtpc 25203 *_𝑝cpco 25234

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205 ax-pre-sup 11206

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-of 7682 df-om 7867 df-1st 7990 df-2nd 7991 df-supp 8163 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-er 8700 df-map 8832 df-ixp 8909 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-fsupp 9336 df-fi 9385 df-sup 9416 df-inf 9417 df-oi 9486 df-card 9948 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-div 11900 df-nn 12262 df-2 12331 df-3 12332 df-4 12333 df-5 12334 df-6 12335 df-7 12336 df-8 12337 df-9 12338 df-n0 12533 df-z 12620 df-dec 12741 df-uz 12892 df-q 13002 df-rp 13047 df-xneg 13167 df-xadd 13168 df-xmul 13169 df-ioo 13406 df-icc 13409 df-fz 13566 df-fzo 13714 df-seq 14070 df-exp 14130 df-hash 14399 df-cj 15190 df-re 15191 df-im 15192 df-sqrt 15326 df-abs 15327 df-struct 17245 df-sets 17262 df-slot 17280 df-ndx 17292 df-base 17308 df-ress 17329 df-plusg 17361 df-mulr 17362 df-starv 17363 df-sca 17364 df-vsca 17365 df-ip 17366 df-tset 17367 df-ple 17368 df-ds 17370 df-unif 17371 df-hom 17372 df-cco 17373 df-rest 17513 df-topn 17514 df-0g 17532 df-gsum 17533 df-topgen 17534 df-pt 17535 df-prds 17538 df-xrs 17594 df-qtop 17599 df-imas 17600 df-xps 17602 df-mre 17676 df-mrc 17677 df-acs 17679 df-mgm 18736 df-sgrp 18827 df-mnd 18843 df-submnd 18898 df-mulg 19197 df-cntz 19450 df-cmn 19915 df-psmet 21583 df-xmet 21584 df-met 21585 df-bl 21586 df-mopn 21587 df-cnfld 21592 df-top 23125 df-topon 23142 df-topsp 23164 df-bases 23177 df-cld 23250 df-cn 23458 df-cnp 23459 df-tx 23794 df-hmeo 23987 df-xms 24552 df-ms 24553 df-tms 24554 df-ii 25111 df-htpy 25204 df-phtpy 25205 df-phtpc 25226 df-pco 25239

This theorem is used by: pcorev 25261

W3C validator