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 ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
reparpht.3 ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn II ) )
reparpht.4 ⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) = 0 )
reparpht.5 ⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) = 1 )
reparphti.6 ⊢ 𝐻 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( ( ( 1 − 𝑦 ) · ( 𝐺 ‘ 𝑥 ) ) + ( 𝑦 · 𝑥 ) ) ) )
Assertion reparphti ( 𝜑 → 𝐻 ∈ ( ( 𝐹 ∘ 𝐺 ) ( PHtpy ‘ 𝐽 ) 𝐹 ) )

Proof

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