Metamath Proof Explorer

Theorem reparphti

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

Ref Expression
Hypotheses reparpht.2 ⊢φ→F∈IICnJ
reparpht.3 ⊢φ→G∈IICnII
reparpht.4 ⊢φ→G⁡0=0
reparpht.5 ⊢φ→G⁡1=1
reparphti.6 ⊢H=x∈01,y∈01⟼F⁡1−y⁢G⁡x+y⁢x
Assertion reparphti ⊢φ→H∈F∘GPHtpy⁡JF

Proof

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