reparphti

Description: Lemma for reparpht . (Contributed by NM, 15-Jun-2010) (Revised by Mario Carneiro, 7-Jun-2014)

	Ref	Expression
Hypotheses	reparpht.2	$⊢ φ \to F \in (II Cn J)$
	reparpht.3	$⊢ φ \to G \in (II Cn II)$
	reparpht.4	$⊢ φ \to G (0) = 0$
	reparpht.5	$⊢ φ \to G (1) = 1$
	reparphti.6	$⊢ H = (x \in [0, 1], y \in [0, 1] ⟼ F ((1 - y) G (x) + y x))$
Assertion	reparphti	$⊢ φ \to H \in ((F \circ G) PHtpy (J) F)$

Proof

Step	Hyp	Ref	Expression
1		reparpht.2	$⊢ φ \to F \in (II Cn J)$
2		reparpht.3	$⊢ φ \to G \in (II Cn II)$
3		reparpht.4	$⊢ φ \to G (0) = 0$
4		reparpht.5	$⊢ φ \to G (1) = 1$
5		reparphti.6	$⊢ H = (x \in [0, 1], y \in [0, 1] ⟼ F ((1 - y) G (x) + y x))$
6		cnco	$⊢ (G \in (II Cn II) \land F \in (II Cn J)) \to F \circ G \in (II Cn J)$
7	2 1 6	syl2anc	$⊢ φ \to F \circ G \in (II Cn J)$
8		iitopon	$⊢ II \in TopOn ([0, 1])$
9	8	a1i	$⊢ φ \to II \in TopOn ([0, 1])$
10		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
11	10	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
12		cnrest2r	$⊢ TopOpen (ℂ_{fld}) \in Top \to (II \times_{t} II) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, 1]) \subseteq (II \times_{t} II) Cn TopOpen (ℂ_{fld})$
13	11 12	mp1i	$⊢ φ \to (II \times_{t} II) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, 1]) \subseteq (II \times_{t} II) Cn TopOpen (ℂ_{fld})$
14	9 9	cnmpt2nd	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ y) \in ((II \times_{t} II) Cn II)$
15		iirevcn	$⊢ (z \in [0, 1] ⟼ 1 - z) \in (II Cn II)$
16	15	a1i	$⊢ φ \to (z \in [0, 1] ⟼ 1 - z) \in (II Cn II)$
17		oveq2	$⊢ z = y \to 1 - z = 1 - y$
18	9 9 14 9 16 17	cnmpt21	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ 1 - y) \in ((II \times_{t} II) Cn II)$
19	10	dfii3	$⊢ II = TopOpen (ℂ_{fld}) ↾_{𝑡} [0, 1]$
20	19	oveq2i	$⊢ (II \times_{t} II) Cn II = (II \times_{t} II) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, 1])$
21	18 20	eleqtrdi	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ 1 - y) \in ((II \times_{t} II) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, 1]))$
22	13 21	sseldd	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ 1 - y) \in ((II \times_{t} II) Cn TopOpen (ℂ_{fld}))$
23	9 9	cnmpt1st	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ x) \in ((II \times_{t} II) Cn II)$
24	9 9 23 2	cnmpt21f	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ G (x)) \in ((II \times_{t} II) Cn II)$
25	24 20	eleqtrdi	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ G (x)) \in ((II \times_{t} II) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, 1]))$
26	13 25	sseldd	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ G (x)) \in ((II \times_{t} II) Cn TopOpen (ℂ_{fld}))$
27	10	mulcn	$⊢ \times \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
28	27	a1i	$⊢ φ \to \times \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
29	9 9 22 26 28	cnmpt22f	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ (1 - y) G (x)) \in ((II \times_{t} II) Cn TopOpen (ℂ_{fld}))$
30	14 20	eleqtrdi	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ y) \in ((II \times_{t} II) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, 1]))$
31	13 30	sseldd	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ y) \in ((II \times_{t} II) Cn TopOpen (ℂ_{fld}))$
32	23 20	eleqtrdi	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ x) \in ((II \times_{t} II) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, 1]))$
33	13 32	sseldd	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ x) \in ((II \times_{t} II) Cn TopOpen (ℂ_{fld}))$
34	9 9 31 33 28	cnmpt22f	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ y x) \in ((II \times_{t} II) Cn TopOpen (ℂ_{fld}))$
35	10	addcn	$⊢ + \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
36	35	a1i	$⊢ φ \to + \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
37	9 9 29 34 36	cnmpt22f	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ (1 - y) G (x) + y x) \in ((II \times_{t} II) Cn TopOpen (ℂ_{fld}))$
38	10	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
39	38	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
40		iiuni	$⊢ [0, 1] = ⋃ II$
41	40 40	cnf	$⊢ G \in (II Cn II) \to G : [0, 1] ⟶ [0, 1]$
42	2 41	syl	$⊢ φ \to G : [0, 1] ⟶ [0, 1]$
43	42	ffvelrnda	$⊢ (φ \land x \in [0, 1]) \to G (x) \in [0, 1]$
44	43	adantrr	$⊢ (φ \land (x \in [0, 1] \land y \in [0, 1])) \to G (x) \in [0, 1]$
45		simprl	$⊢ (φ \land (x \in [0, 1] \land y \in [0, 1])) \to x \in [0, 1]$
46		simprr	$⊢ (φ \land (x \in [0, 1] \land y \in [0, 1])) \to y \in [0, 1]$
47		0re	$⊢ 0 \in ℝ$
48		1re	$⊢ 1 \in ℝ$
49		icccvx	$⊢ (0 \in ℝ \land 1 \in ℝ) \to ((G (x) \in [0, 1] \land x \in [0, 1] \land y \in [0, 1]) \to (1 - y) G (x) + y x \in [0, 1])$
50	47 48 49	mp2an	$⊢ (G (x) \in [0, 1] \land x \in [0, 1] \land y \in [0, 1]) \to (1 - y) G (x) + y x \in [0, 1]$
51	44 45 46 50	syl3anc	$⊢ (φ \land (x \in [0, 1] \land y \in [0, 1])) \to (1 - y) G (x) + y x \in [0, 1]$
52	51	ralrimivva	$⊢ φ \to \forall x \in [0, 1] \forall y \in [0, 1] (1 - y) G (x) + y x \in [0, 1]$
53		eqid	$⊢ (x \in [0, 1], y \in [0, 1] ⟼ (1 - y) G (x) + y x) = (x \in [0, 1], y \in [0, 1] ⟼ (1 - y) G (x) + y x)$
54	53	fmpo	$⊢ \forall x \in [0, 1] \forall y \in [0, 1] (1 - y) G (x) + y x \in [0, 1] \leftrightarrow (x \in [0, 1], y \in [0, 1] ⟼ (1 - y) G (x) + y x) : [0, 1] \times [0, 1] ⟶ [0, 1]$
55	52 54	sylib	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ (1 - y) G (x) + y x) : [0, 1] \times [0, 1] ⟶ [0, 1]$
56	55	frnd	$⊢ φ \to ran (x \in [0, 1], y \in [0, 1] ⟼ (1 - y) G (x) + y x) \subseteq [0, 1]$
57		unitssre	$⊢ [0, 1] \subseteq ℝ$
58		ax-resscn	$⊢ ℝ \subseteq ℂ$
59	57 58	sstri	$⊢ [0, 1] \subseteq ℂ$
60	59	a1i	$⊢ φ \to [0, 1] \subseteq ℂ$
61		cnrest2	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land ran (x \in [0, 1], y \in [0, 1] ⟼ (1 - y) G (x) + y x) \subseteq [0, 1] \land [0, 1] \subseteq ℂ) \to ((x \in [0, 1], y \in [0, 1] ⟼ (1 - y) G (x) + y x) \in ((II \times_{t} II) Cn TopOpen (ℂ_{fld})) \leftrightarrow (x \in [0, 1], y \in [0, 1] ⟼ (1 - y) G (x) + y x) \in ((II \times_{t} II) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, 1])))$
62	39 56 60 61	syl3anc	$⊢ φ \to ((x \in [0, 1], y \in [0, 1] ⟼ (1 - y) G (x) + y x) \in ((II \times_{t} II) Cn TopOpen (ℂ_{fld})) \leftrightarrow (x \in [0, 1], y \in [0, 1] ⟼ (1 - y) G (x) + y x) \in ((II \times_{t} II) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, 1])))$
63	37 62	mpbid	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ (1 - y) G (x) + y x) \in ((II \times_{t} II) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, 1]))$
64	63 20	eleqtrrdi	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ (1 - y) G (x) + y x) \in ((II \times_{t} II) Cn II)$
65	9 9 64 1	cnmpt21f	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ F ((1 - y) G (x) + y x)) \in ((II \times_{t} II) Cn J)$
66	5 65	eqeltrid	$⊢ φ \to H \in ((II \times_{t} II) Cn J)$
67	42	ffvelrnda	$⊢ (φ \land s \in [0, 1]) \to G (s) \in [0, 1]$
68	59 67	sseldi	$⊢ (φ \land s \in [0, 1]) \to G (s) \in ℂ$
69	68	mulid2d	$⊢ (φ \land s \in [0, 1]) \to 1 G (s) = G (s)$
70	59	sseli	$⊢ s \in [0, 1] \to s \in ℂ$
71	70	adantl	$⊢ (φ \land s \in [0, 1]) \to s \in ℂ$
72	71	mul02d	$⊢ (φ \land s \in [0, 1]) \to 0 \cdot s = 0$
73	69 72	oveq12d	$⊢ (φ \land s \in [0, 1]) \to 1 G (s) + 0 \cdot s = G (s) + 0$
74	68	addid1d	$⊢ (φ \land s \in [0, 1]) \to G (s) + 0 = G (s)$
75	73 74	eqtrd	$⊢ (φ \land s \in [0, 1]) \to 1 G (s) + 0 \cdot s = G (s)$
76	75	fveq2d	$⊢ (φ \land s \in [0, 1]) \to F (1 G (s) + 0 \cdot s) = F (G (s))$
77		simpr	$⊢ (φ \land s \in [0, 1]) \to s \in [0, 1]$
78		0elunit	$⊢ 0 \in [0, 1]$
79		simpr	$⊢ (x = s \land y = 0) \to y = 0$
80	79	oveq2d	$⊢ (x = s \land y = 0) \to 1 - y = 1 - 0$
81		1m0e1	$⊢ 1 - 0 = 1$
82	80 81	eqtrdi	$⊢ (x = s \land y = 0) \to 1 - y = 1$
83		simpl	$⊢ (x = s \land y = 0) \to x = s$
84	83	fveq2d	$⊢ (x = s \land y = 0) \to G (x) = G (s)$
85	82 84	oveq12d	$⊢ (x = s \land y = 0) \to (1 - y) G (x) = 1 G (s)$
86	79 83	oveq12d	$⊢ (x = s \land y = 0) \to y x = 0 \cdot s$
87	85 86	oveq12d	$⊢ (x = s \land y = 0) \to (1 - y) G (x) + y x = 1 G (s) + 0 \cdot s$
88	87	fveq2d	$⊢ (x = s \land y = 0) \to F ((1 - y) G (x) + y x) = F (1 G (s) + 0 \cdot s)$
89		fvex	$⊢ F (1 G (s) + 0 \cdot s) \in V$
90	88 5 89	ovmpoa	$⊢ (s \in [0, 1] \land 0 \in [0, 1]) \to s H 0 = F (1 G (s) + 0 \cdot s)$
91	77 78 90	sylancl	$⊢ (φ \land s \in [0, 1]) \to s H 0 = F (1 G (s) + 0 \cdot s)$
92		fvco3	$⊢ (G : [0, 1] ⟶ [0, 1] \land s \in [0, 1]) \to (F \circ G) (s) = F (G (s))$
93	42 92	sylan	$⊢ (φ \land s \in [0, 1]) \to (F \circ G) (s) = F (G (s))$
94	76 91 93	3eqtr4d	$⊢ (φ \land s \in [0, 1]) \to s H 0 = (F \circ G) (s)$
95		1elunit	$⊢ 1 \in [0, 1]$
96		simpr	$⊢ (x = s \land y = 1) \to y = 1$
97	96	oveq2d	$⊢ (x = s \land y = 1) \to 1 - y = 1 - 1$
98		1m1e0	$⊢ 1 - 1 = 0$
99	97 98	eqtrdi	$⊢ (x = s \land y = 1) \to 1 - y = 0$
100		simpl	$⊢ (x = s \land y = 1) \to x = s$
101	100	fveq2d	$⊢ (x = s \land y = 1) \to G (x) = G (s)$
102	99 101	oveq12d	$⊢ (x = s \land y = 1) \to (1 - y) G (x) = 0 \cdot G (s)$
103	96 100	oveq12d	$⊢ (x = s \land y = 1) \to y x = 1 s$
104	102 103	oveq12d	$⊢ (x = s \land y = 1) \to (1 - y) G (x) + y x = 0 \cdot G (s) + 1 s$
105	104	fveq2d	$⊢ (x = s \land y = 1) \to F ((1 - y) G (x) + y x) = F (0 \cdot G (s) + 1 s)$
106		fvex	$⊢ F (0 \cdot G (s) + 1 s) \in V$
107	105 5 106	ovmpoa	$⊢ (s \in [0, 1] \land 1 \in [0, 1]) \to s H 1 = F (0 \cdot G (s) + 1 s)$
108	77 95 107	sylancl	$⊢ (φ \land s \in [0, 1]) \to s H 1 = F (0 \cdot G (s) + 1 s)$
109	68	mul02d	$⊢ (φ \land s \in [0, 1]) \to 0 \cdot G (s) = 0$
110	71	mulid2d	$⊢ (φ \land s \in [0, 1]) \to 1 s = s$
111	109 110	oveq12d	$⊢ (φ \land s \in [0, 1]) \to 0 \cdot G (s) + 1 s = 0 + s$
112	71	addid2d	$⊢ (φ \land s \in [0, 1]) \to 0 + s = s$
113	111 112	eqtrd	$⊢ (φ \land s \in [0, 1]) \to 0 \cdot G (s) + 1 s = s$
114	113	fveq2d	$⊢ (φ \land s \in [0, 1]) \to F (0 \cdot G (s) + 1 s) = F (s)$
115	108 114	eqtrd	$⊢ (φ \land s \in [0, 1]) \to s H 1 = F (s)$
116	3	adantr	$⊢ (φ \land s \in [0, 1]) \to G (0) = 0$
117	116	oveq2d	$⊢ (φ \land s \in [0, 1]) \to (1 - s) G (0) = (1 - s) \cdot 0$
118		ax-1cn	$⊢ 1 \in ℂ$
119		subcl	$⊢ (1 \in ℂ \land s \in ℂ) \to 1 - s \in ℂ$
120	118 71 119	sylancr	$⊢ (φ \land s \in [0, 1]) \to 1 - s \in ℂ$
121	120	mul01d	$⊢ (φ \land s \in [0, 1]) \to (1 - s) \cdot 0 = 0$
122	117 121	eqtrd	$⊢ (φ \land s \in [0, 1]) \to (1 - s) G (0) = 0$
123	71	mul01d	$⊢ (φ \land s \in [0, 1]) \to s \cdot 0 = 0$
124	122 123	oveq12d	$⊢ (φ \land s \in [0, 1]) \to (1 - s) G (0) + s \cdot 0 = 0 + 0$
125		00id	$⊢ 0 + 0 = 0$
126	124 125	eqtrdi	$⊢ (φ \land s \in [0, 1]) \to (1 - s) G (0) + s \cdot 0 = 0$
127	126	fveq2d	$⊢ (φ \land s \in [0, 1]) \to F ((1 - s) G (0) + s \cdot 0) = F (0)$
128		simpr	$⊢ (x = 0 \land y = s) \to y = s$
129	128	oveq2d	$⊢ (x = 0 \land y = s) \to 1 - y = 1 - s$
130		simpl	$⊢ (x = 0 \land y = s) \to x = 0$
131	130	fveq2d	$⊢ (x = 0 \land y = s) \to G (x) = G (0)$
132	129 131	oveq12d	$⊢ (x = 0 \land y = s) \to (1 - y) G (x) = (1 - s) G (0)$
133	128 130	oveq12d	$⊢ (x = 0 \land y = s) \to y x = s \cdot 0$
134	132 133	oveq12d	$⊢ (x = 0 \land y = s) \to (1 - y) G (x) + y x = (1 - s) G (0) + s \cdot 0$
135	134	fveq2d	$⊢ (x = 0 \land y = s) \to F ((1 - y) G (x) + y x) = F ((1 - s) G (0) + s \cdot 0)$
136		fvex	$⊢ F ((1 - s) G (0) + s \cdot 0) \in V$
137	135 5 136	ovmpoa	$⊢ (0 \in [0, 1] \land s \in [0, 1]) \to 0 H s = F ((1 - s) G (0) + s \cdot 0)$
138	78 77 137	sylancr	$⊢ (φ \land s \in [0, 1]) \to 0 H s = F ((1 - s) G (0) + s \cdot 0)$
139		fvco3	$⊢ (G : [0, 1] ⟶ [0, 1] \land 0 \in [0, 1]) \to (F \circ G) (0) = F (G (0))$
140	42 78 139	sylancl	$⊢ φ \to (F \circ G) (0) = F (G (0))$
141	3	fveq2d	$⊢ φ \to F (G (0)) = F (0)$
142	140 141	eqtrd	$⊢ φ \to (F \circ G) (0) = F (0)$
143	142	adantr	$⊢ (φ \land s \in [0, 1]) \to (F \circ G) (0) = F (0)$
144	127 138 143	3eqtr4d	$⊢ (φ \land s \in [0, 1]) \to 0 H s = (F \circ G) (0)$
145	4	adantr	$⊢ (φ \land s \in [0, 1]) \to G (1) = 1$
146	145	oveq2d	$⊢ (φ \land s \in [0, 1]) \to (1 - s) G (1) = (1 - s) \cdot 1$
147	120	mulid1d	$⊢ (φ \land s \in [0, 1]) \to (1 - s) \cdot 1 = 1 - s$
148	146 147	eqtrd	$⊢ (φ \land s \in [0, 1]) \to (1 - s) G (1) = 1 - s$
149	71	mulid1d	$⊢ (φ \land s \in [0, 1]) \to s \cdot 1 = s$
150	148 149	oveq12d	$⊢ (φ \land s \in [0, 1]) \to (1 - s) G (1) + s \cdot 1 = 1 - s + s$
151		npcan	$⊢ (1 \in ℂ \land s \in ℂ) \to 1 - s + s = 1$
152	118 71 151	sylancr	$⊢ (φ \land s \in [0, 1]) \to 1 - s + s = 1$
153	150 152	eqtrd	$⊢ (φ \land s \in [0, 1]) \to (1 - s) G (1) + s \cdot 1 = 1$
154	153	fveq2d	$⊢ (φ \land s \in [0, 1]) \to F ((1 - s) G (1) + s \cdot 1) = F (1)$
155		simpr	$⊢ (x = 1 \land y = s) \to y = s$
156	155	oveq2d	$⊢ (x = 1 \land y = s) \to 1 - y = 1 - s$
157		simpl	$⊢ (x = 1 \land y = s) \to x = 1$
158	157	fveq2d	$⊢ (x = 1 \land y = s) \to G (x) = G (1)$
159	156 158	oveq12d	$⊢ (x = 1 \land y = s) \to (1 - y) G (x) = (1 - s) G (1)$
160	155 157	oveq12d	$⊢ (x = 1 \land y = s) \to y x = s \cdot 1$
161	159 160	oveq12d	$⊢ (x = 1 \land y = s) \to (1 - y) G (x) + y x = (1 - s) G (1) + s \cdot 1$
162	161	fveq2d	$⊢ (x = 1 \land y = s) \to F ((1 - y) G (x) + y x) = F ((1 - s) G (1) + s \cdot 1)$
163		fvex	$⊢ F ((1 - s) G (1) + s \cdot 1) \in V$
164	162 5 163	ovmpoa	$⊢ (1 \in [0, 1] \land s \in [0, 1]) \to 1 H s = F ((1 - s) G (1) + s \cdot 1)$
165	95 77 164	sylancr	$⊢ (φ \land s \in [0, 1]) \to 1 H s = F ((1 - s) G (1) + s \cdot 1)$
166		fvco3	$⊢ (G : [0, 1] ⟶ [0, 1] \land 1 \in [0, 1]) \to (F \circ G) (1) = F (G (1))$
167	42 95 166	sylancl	$⊢ φ \to (F \circ G) (1) = F (G (1))$
168	4	fveq2d	$⊢ φ \to F (G (1)) = F (1)$
169	167 168	eqtrd	$⊢ φ \to (F \circ G) (1) = F (1)$
170	169	adantr	$⊢ (φ \land s \in [0, 1]) \to (F \circ G) (1) = F (1)$
171	154 165 170	3eqtr4d	$⊢ (φ \land s \in [0, 1]) \to 1 H s = (F \circ G) (1)$
172	7 1 66 94 115 144 171	isphtpy2d	$⊢ φ \to H \in ((F \circ G) PHtpy (J) F)$

Metamath Proof Explorer

Theorem reparphti

Proof