Step | Hyp | Ref
| Expression |
1 | | reparpht.3 |
. . 3
⊢ (𝜑 → 𝐺 ∈ (II Cn II)) |
2 | | reparpht.2 |
. . 3
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) |
3 | | cnco 20880 |
. . 3
⊢ ((𝐺 ∈ (II Cn II) ∧ 𝐹 ∈ (II Cn 𝐽)) → (𝐹 ∘ 𝐺) ∈ (II Cn 𝐽)) |
4 | 1, 2, 3 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ (II Cn 𝐽)) |
5 | | reparphti.6 |
. . 3
⊢ 𝐻 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝐹‘(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)))) |
6 | | iitopon 22490 |
. . . . 5
⊢ II ∈
(TopOn‘(0[,]1)) |
7 | 6 | a1i 11 |
. . . 4
⊢ (𝜑 → II ∈
(TopOn‘(0[,]1))) |
8 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
9 | 8 | cnfldtop 22397 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) ∈ Top |
10 | | cnrest2r 20901 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ∈ Top → ((II
×t II) Cn ((TopOpen‘ℂfld)
↾t (0[,]1))) ⊆ ((II ×t II) Cn
(TopOpen‘ℂfld))) |
11 | 9, 10 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → ((II ×t
II) Cn ((TopOpen‘ℂfld) ↾t (0[,]1)))
⊆ ((II ×t II) Cn
(TopOpen‘ℂfld))) |
12 | 7, 7 | cnmpt2nd 21282 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ 𝑦) ∈ ((II ×t II) Cn
II)) |
13 | | iirevcn 22537 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (0[,]1) ↦ (1
− 𝑧)) ∈ (II Cn
II) |
14 | 13 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑧 ∈ (0[,]1) ↦ (1 − 𝑧)) ∈ (II Cn
II)) |
15 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑦 → (1 − 𝑧) = (1 − 𝑦)) |
16 | 7, 7, 12, 7, 14, 15 | cnmpt21 21284 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (1 − 𝑦)) ∈ ((II
×t II) Cn II)) |
17 | 8 | dfii3 22494 |
. . . . . . . . . . 11
⊢ II =
((TopOpen‘ℂfld) ↾t
(0[,]1)) |
18 | 17 | oveq2i 6560 |
. . . . . . . . . 10
⊢ ((II
×t II) Cn II) = ((II ×t II) Cn
((TopOpen‘ℂfld) ↾t
(0[,]1))) |
19 | 16, 18 | syl6eleq 2698 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (1 − 𝑦)) ∈ ((II
×t II) Cn ((TopOpen‘ℂfld)
↾t (0[,]1)))) |
20 | 11, 19 | sseldd 3569 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (1 − 𝑦)) ∈ ((II
×t II) Cn
(TopOpen‘ℂfld))) |
21 | 7, 7 | cnmpt1st 21281 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ 𝑥) ∈ ((II ×t II) Cn
II)) |
22 | 7, 7, 21, 1 | cnmpt21f 21285 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝐺‘𝑥)) ∈ ((II ×t II) Cn
II)) |
23 | 22, 18 | syl6eleq 2698 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝐺‘𝑥)) ∈ ((II ×t II) Cn
((TopOpen‘ℂfld) ↾t
(0[,]1)))) |
24 | 11, 23 | sseldd 3569 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝐺‘𝑥)) ∈ ((II ×t II) Cn
(TopOpen‘ℂfld))) |
25 | 8 | mulcn 22478 |
. . . . . . . . 9
⊢ ·
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
26 | 25 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → · ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
27 | 7, 7, 20, 24, 26 | cnmpt22f 21288 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ ((1 − 𝑦) · (𝐺‘𝑥))) ∈ ((II ×t II) Cn
(TopOpen‘ℂfld))) |
28 | 12, 18 | syl6eleq 2698 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ 𝑦) ∈ ((II ×t II) Cn
((TopOpen‘ℂfld) ↾t
(0[,]1)))) |
29 | 11, 28 | sseldd 3569 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ 𝑦) ∈ ((II ×t II) Cn
(TopOpen‘ℂfld))) |
30 | 21, 18 | syl6eleq 2698 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ 𝑥) ∈ ((II ×t II) Cn
((TopOpen‘ℂfld) ↾t
(0[,]1)))) |
31 | 11, 30 | sseldd 3569 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ 𝑥) ∈ ((II ×t II) Cn
(TopOpen‘ℂfld))) |
32 | 7, 7, 29, 31, 26 | cnmpt22f 21288 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝑦 · 𝑥)) ∈ ((II ×t II) Cn
(TopOpen‘ℂfld))) |
33 | 8 | addcn 22476 |
. . . . . . . 8
⊢ + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
34 | 33 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
35 | 7, 7, 27, 32, 34 | cnmpt22f 21288 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))) ∈ ((II ×t II) Cn
(TopOpen‘ℂfld))) |
36 | 8 | cnfldtopon 22396 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
37 | 36 | a1i 11 |
. . . . . . 7
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) |
38 | | iiuni 22492 |
. . . . . . . . . . . . . . 15
⊢ (0[,]1) =
∪ II |
39 | 38, 38 | cnf 20860 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ (II Cn II) → 𝐺:(0[,]1)⟶(0[,]1)) |
40 | 1, 39 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺:(0[,]1)⟶(0[,]1)) |
41 | 40 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → (𝐺‘𝑥) ∈ (0[,]1)) |
42 | 41 | adantrr 749 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1))) → (𝐺‘𝑥) ∈ (0[,]1)) |
43 | | simprl 790 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1))) → 𝑥 ∈ (0[,]1)) |
44 | | simprr 792 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1))) → 𝑦 ∈ (0[,]1)) |
45 | | 0re 9919 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ |
46 | | 1re 9918 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
47 | | icccvx 22557 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ) → (((𝐺‘𝑥) ∈ (0[,]1) ∧ 𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) → (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)) ∈ (0[,]1))) |
48 | 45, 46, 47 | mp2an 704 |
. . . . . . . . . . 11
⊢ (((𝐺‘𝑥) ∈ (0[,]1) ∧ 𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) → (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)) ∈ (0[,]1)) |
49 | 42, 43, 44, 48 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1))) → (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)) ∈ (0[,]1)) |
50 | 49 | ralrimivva 2954 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ (0[,]1)∀𝑦 ∈ (0[,]1)(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)) ∈ (0[,]1)) |
51 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (((1
− 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))) = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))) |
52 | 51 | fmpt2 7126 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
(0[,]1)∀𝑦 ∈
(0[,]1)(((1 − 𝑦)
· (𝐺‘𝑥)) + (𝑦 · 𝑥)) ∈ (0[,]1) ↔ (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))):((0[,]1) ×
(0[,]1))⟶(0[,]1)) |
53 | 50, 52 | sylib 207 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))):((0[,]1) ×
(0[,]1))⟶(0[,]1)) |
54 | | frn 5966 |
. . . . . . . 8
⊢ ((𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (((1
− 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))):((0[,]1) × (0[,]1))⟶(0[,]1)
→ ran (𝑥 ∈
(0[,]1), 𝑦 ∈ (0[,]1)
↦ (((1 − 𝑦)
· (𝐺‘𝑥)) + (𝑦 · 𝑥))) ⊆ (0[,]1)) |
55 | 53, 54 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))) ⊆ (0[,]1)) |
56 | | unitssre 12190 |
. . . . . . . . 9
⊢ (0[,]1)
⊆ ℝ |
57 | | ax-resscn 9872 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
58 | 56, 57 | sstri 3577 |
. . . . . . . 8
⊢ (0[,]1)
⊆ ℂ |
59 | 58 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (0[,]1) ⊆
ℂ) |
60 | | cnrest2 20900 |
. . . . . . 7
⊢
(((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))))) |
61 | 37, 55, 59, 60 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (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 | 35, 61 | mpbid 221 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))) ∈ ((II ×t II) Cn
((TopOpen‘ℂfld) ↾t
(0[,]1)))) |
63 | 62, 18 | syl6eleqr 2699 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))) ∈ ((II ×t II) Cn
II)) |
64 | 7, 7, 63, 2 | cnmpt21f 21285 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝐹‘(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)))) ∈ ((II ×t II) Cn
𝐽)) |
65 | 5, 64 | syl5eqel 2692 |
. 2
⊢ (𝜑 → 𝐻 ∈ ((II ×t II) Cn
𝐽)) |
66 | 40 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝐺‘𝑠) ∈ (0[,]1)) |
67 | 58, 66 | sseldi 3566 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝐺‘𝑠) ∈ ℂ) |
68 | 67 | mulid2d 9937 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1 · (𝐺‘𝑠)) = (𝐺‘𝑠)) |
69 | 58 | sseli 3564 |
. . . . . . . 8
⊢ (𝑠 ∈ (0[,]1) → 𝑠 ∈
ℂ) |
70 | 69 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → 𝑠 ∈ ℂ) |
71 | 70 | mul02d 10113 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0 · 𝑠) = 0) |
72 | 68, 71 | oveq12d 6567 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((1 · (𝐺‘𝑠)) + (0 · 𝑠)) = ((𝐺‘𝑠) + 0)) |
73 | 67 | addid1d 10115 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((𝐺‘𝑠) + 0) = (𝐺‘𝑠)) |
74 | 72, 73 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((1 · (𝐺‘𝑠)) + (0 · 𝑠)) = (𝐺‘𝑠)) |
75 | 74 | fveq2d 6107 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝐹‘((1 · (𝐺‘𝑠)) + (0 · 𝑠))) = (𝐹‘(𝐺‘𝑠))) |
76 | | simpr 476 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → 𝑠 ∈ (0[,]1)) |
77 | | 0elunit 12161 |
. . . 4
⊢ 0 ∈
(0[,]1) |
78 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → 𝑦 = 0) |
79 | 78 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (1 − 𝑦) = (1 − 0)) |
80 | | 1m0e1 11008 |
. . . . . . . . 9
⊢ (1
− 0) = 1 |
81 | 79, 80 | syl6eq 2660 |
. . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (1 − 𝑦) = 1) |
82 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → 𝑥 = 𝑠) |
83 | 82 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (𝐺‘𝑥) = (𝐺‘𝑠)) |
84 | 81, 83 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → ((1 − 𝑦) · (𝐺‘𝑥)) = (1 · (𝐺‘𝑠))) |
85 | 78, 82 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (𝑦 · 𝑥) = (0 · 𝑠)) |
86 | 84, 85 | oveq12d 6567 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)) = ((1 · (𝐺‘𝑠)) + (0 · 𝑠))) |
87 | 86 | fveq2d 6107 |
. . . . 5
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (𝐹‘(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))) = (𝐹‘((1 · (𝐺‘𝑠)) + (0 · 𝑠)))) |
88 | | fvex 6113 |
. . . . 5
⊢ (𝐹‘((1 · (𝐺‘𝑠)) + (0 · 𝑠))) ∈ V |
89 | 87, 5, 88 | ovmpt2a 6689 |
. . . 4
⊢ ((𝑠 ∈ (0[,]1) ∧ 0 ∈
(0[,]1)) → (𝑠𝐻0) = (𝐹‘((1 · (𝐺‘𝑠)) + (0 · 𝑠)))) |
90 | 76, 77, 89 | sylancl 693 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠𝐻0) = (𝐹‘((1 · (𝐺‘𝑠)) + (0 · 𝑠)))) |
91 | | fvco3 6185 |
. . . 4
⊢ ((𝐺:(0[,]1)⟶(0[,]1) ∧
𝑠 ∈ (0[,]1)) →
((𝐹 ∘ 𝐺)‘𝑠) = (𝐹‘(𝐺‘𝑠))) |
92 | 40, 91 | sylan 487 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((𝐹 ∘ 𝐺)‘𝑠) = (𝐹‘(𝐺‘𝑠))) |
93 | 75, 90, 92 | 3eqtr4d 2654 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠𝐻0) = ((𝐹 ∘ 𝐺)‘𝑠)) |
94 | | 1elunit 12162 |
. . . 4
⊢ 1 ∈
(0[,]1) |
95 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → 𝑦 = 1) |
96 | 95 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (1 − 𝑦) = (1 − 1)) |
97 | | 1m1e0 10966 |
. . . . . . . . 9
⊢ (1
− 1) = 0 |
98 | 96, 97 | syl6eq 2660 |
. . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (1 − 𝑦) = 0) |
99 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → 𝑥 = 𝑠) |
100 | 99 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (𝐺‘𝑥) = (𝐺‘𝑠)) |
101 | 98, 100 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → ((1 − 𝑦) · (𝐺‘𝑥)) = (0 · (𝐺‘𝑠))) |
102 | 95, 99 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (𝑦 · 𝑥) = (1 · 𝑠)) |
103 | 101, 102 | oveq12d 6567 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)) = ((0 · (𝐺‘𝑠)) + (1 · 𝑠))) |
104 | 103 | fveq2d 6107 |
. . . . 5
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (𝐹‘(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))) = (𝐹‘((0 · (𝐺‘𝑠)) + (1 · 𝑠)))) |
105 | | fvex 6113 |
. . . . 5
⊢ (𝐹‘((0 · (𝐺‘𝑠)) + (1 · 𝑠))) ∈ V |
106 | 104, 5, 105 | ovmpt2a 6689 |
. . . 4
⊢ ((𝑠 ∈ (0[,]1) ∧ 1 ∈
(0[,]1)) → (𝑠𝐻1) = (𝐹‘((0 · (𝐺‘𝑠)) + (1 · 𝑠)))) |
107 | 76, 94, 106 | sylancl 693 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠𝐻1) = (𝐹‘((0 · (𝐺‘𝑠)) + (1 · 𝑠)))) |
108 | 67 | mul02d 10113 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0 · (𝐺‘𝑠)) = 0) |
109 | 70 | mulid2d 9937 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1 · 𝑠) = 𝑠) |
110 | 108, 109 | oveq12d 6567 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((0 · (𝐺‘𝑠)) + (1 · 𝑠)) = (0 + 𝑠)) |
111 | 70 | addid2d 10116 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0 + 𝑠) = 𝑠) |
112 | 110, 111 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((0 · (𝐺‘𝑠)) + (1 · 𝑠)) = 𝑠) |
113 | 112 | fveq2d 6107 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝐹‘((0 · (𝐺‘𝑠)) + (1 · 𝑠))) = (𝐹‘𝑠)) |
114 | 107, 113 | eqtrd 2644 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠𝐻1) = (𝐹‘𝑠)) |
115 | | reparpht.4 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺‘0) = 0) |
116 | 115 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝐺‘0) = 0) |
117 | 116 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((1 − 𝑠) · (𝐺‘0)) = ((1 − 𝑠) · 0)) |
118 | | ax-1cn 9873 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
119 | | subcl 10159 |
. . . . . . . . 9
⊢ ((1
∈ ℂ ∧ 𝑠
∈ ℂ) → (1 − 𝑠) ∈ ℂ) |
120 | 118, 70, 119 | sylancr 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1 − 𝑠) ∈
ℂ) |
121 | 120 | mul01d 10114 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((1 − 𝑠) · 0) =
0) |
122 | 117, 121 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((1 − 𝑠) · (𝐺‘0)) = 0) |
123 | 70 | mul01d 10114 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠 · 0) = 0) |
124 | 122, 123 | oveq12d 6567 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (((1 − 𝑠) · (𝐺‘0)) + (𝑠 · 0)) = (0 + 0)) |
125 | | 00id 10090 |
. . . . 5
⊢ (0 + 0) =
0 |
126 | 124, 125 | syl6eq 2660 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (((1 − 𝑠) · (𝐺‘0)) + (𝑠 · 0)) = 0) |
127 | 126 | fveq2d 6107 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝐹‘(((1 − 𝑠) · (𝐺‘0)) + (𝑠 · 0))) = (𝐹‘0)) |
128 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → 𝑦 = 𝑠) |
129 | 128 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → (1 − 𝑦) = (1 − 𝑠)) |
130 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → 𝑥 = 0) |
131 | 130 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → (𝐺‘𝑥) = (𝐺‘0)) |
132 | 129, 131 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → ((1 − 𝑦) · (𝐺‘𝑥)) = ((1 − 𝑠) · (𝐺‘0))) |
133 | 128, 130 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → (𝑦 · 𝑥) = (𝑠 · 0)) |
134 | 132, 133 | oveq12d 6567 |
. . . . . 6
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)) = (((1 − 𝑠) · (𝐺‘0)) + (𝑠 · 0))) |
135 | 134 | fveq2d 6107 |
. . . . 5
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → (𝐹‘(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))) = (𝐹‘(((1 − 𝑠) · (𝐺‘0)) + (𝑠 · 0)))) |
136 | | fvex 6113 |
. . . . 5
⊢ (𝐹‘(((1 − 𝑠) · (𝐺‘0)) + (𝑠 · 0))) ∈ V |
137 | 135, 5, 136 | ovmpt2a 6689 |
. . . 4
⊢ ((0
∈ (0[,]1) ∧ 𝑠
∈ (0[,]1)) → (0𝐻𝑠) = (𝐹‘(((1 − 𝑠) · (𝐺‘0)) + (𝑠 · 0)))) |
138 | 77, 76, 137 | sylancr 694 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0𝐻𝑠) = (𝐹‘(((1 − 𝑠) · (𝐺‘0)) + (𝑠 · 0)))) |
139 | | fvco3 6185 |
. . . . . 6
⊢ ((𝐺:(0[,]1)⟶(0[,]1) ∧ 0
∈ (0[,]1)) → ((𝐹
∘ 𝐺)‘0) =
(𝐹‘(𝐺‘0))) |
140 | 40, 77, 139 | sylancl 693 |
. . . . 5
⊢ (𝜑 → ((𝐹 ∘ 𝐺)‘0) = (𝐹‘(𝐺‘0))) |
141 | 115 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 → (𝐹‘(𝐺‘0)) = (𝐹‘0)) |
142 | 140, 141 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → ((𝐹 ∘ 𝐺)‘0) = (𝐹‘0)) |
143 | 142 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((𝐹 ∘ 𝐺)‘0) = (𝐹‘0)) |
144 | 127, 138,
143 | 3eqtr4d 2654 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0𝐻𝑠) = ((𝐹 ∘ 𝐺)‘0)) |
145 | | reparpht.5 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺‘1) = 1) |
146 | 145 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝐺‘1) = 1) |
147 | 146 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((1 − 𝑠) · (𝐺‘1)) = ((1 − 𝑠) · 1)) |
148 | 120 | mulid1d 9936 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((1 − 𝑠) · 1) = (1 − 𝑠)) |
149 | 147, 148 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((1 − 𝑠) · (𝐺‘1)) = (1 − 𝑠)) |
150 | 70 | mulid1d 9936 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠 · 1) = 𝑠) |
151 | 149, 150 | oveq12d 6567 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (((1 − 𝑠) · (𝐺‘1)) + (𝑠 · 1)) = ((1 − 𝑠) + 𝑠)) |
152 | | npcan 10169 |
. . . . . 6
⊢ ((1
∈ ℂ ∧ 𝑠
∈ ℂ) → ((1 − 𝑠) + 𝑠) = 1) |
153 | 118, 70, 152 | sylancr 694 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((1 − 𝑠) + 𝑠) = 1) |
154 | 151, 153 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (((1 − 𝑠) · (𝐺‘1)) + (𝑠 · 1)) = 1) |
155 | 154 | fveq2d 6107 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝐹‘(((1 − 𝑠) · (𝐺‘1)) + (𝑠 · 1))) = (𝐹‘1)) |
156 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → 𝑦 = 𝑠) |
157 | 156 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (1 − 𝑦) = (1 − 𝑠)) |
158 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → 𝑥 = 1) |
159 | 158 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (𝐺‘𝑥) = (𝐺‘1)) |
160 | 157, 159 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → ((1 − 𝑦) · (𝐺‘𝑥)) = ((1 − 𝑠) · (𝐺‘1))) |
161 | 156, 158 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (𝑦 · 𝑥) = (𝑠 · 1)) |
162 | 160, 161 | oveq12d 6567 |
. . . . . 6
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)) = (((1 − 𝑠) · (𝐺‘1)) + (𝑠 · 1))) |
163 | 162 | fveq2d 6107 |
. . . . 5
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (𝐹‘(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))) = (𝐹‘(((1 − 𝑠) · (𝐺‘1)) + (𝑠 · 1)))) |
164 | | fvex 6113 |
. . . . 5
⊢ (𝐹‘(((1 − 𝑠) · (𝐺‘1)) + (𝑠 · 1))) ∈ V |
165 | 163, 5, 164 | ovmpt2a 6689 |
. . . 4
⊢ ((1
∈ (0[,]1) ∧ 𝑠
∈ (0[,]1)) → (1𝐻𝑠) = (𝐹‘(((1 − 𝑠) · (𝐺‘1)) + (𝑠 · 1)))) |
166 | 94, 76, 165 | sylancr 694 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1𝐻𝑠) = (𝐹‘(((1 − 𝑠) · (𝐺‘1)) + (𝑠 · 1)))) |
167 | | fvco3 6185 |
. . . . . 6
⊢ ((𝐺:(0[,]1)⟶(0[,]1) ∧ 1
∈ (0[,]1)) → ((𝐹
∘ 𝐺)‘1) =
(𝐹‘(𝐺‘1))) |
168 | 40, 94, 167 | sylancl 693 |
. . . . 5
⊢ (𝜑 → ((𝐹 ∘ 𝐺)‘1) = (𝐹‘(𝐺‘1))) |
169 | 145 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 → (𝐹‘(𝐺‘1)) = (𝐹‘1)) |
170 | 168, 169 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → ((𝐹 ∘ 𝐺)‘1) = (𝐹‘1)) |
171 | 170 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((𝐹 ∘ 𝐺)‘1) = (𝐹‘1)) |
172 | 155, 166,
171 | 3eqtr4d 2654 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1𝐻𝑠) = ((𝐹 ∘ 𝐺)‘1)) |
173 | 4, 2, 65, 93, 114, 144, 172 | isphtpy2d 22594 |
1
⊢ (𝜑 → 𝐻 ∈ ((𝐹 ∘ 𝐺)(PHtpy‘𝐽)𝐹)) |