| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | reparpht.2 | . . 3
⊢ (𝜑 → 𝐺 ∈ (II Cn II)) | 
| 2 |  | reparpht.1 | . . 3
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) | 
| 3 |  | cnco 23274 | . . 3
⊢ ((𝐺 ∈ (II Cn II) ∧ 𝐹 ∈ (II Cn 𝐽)) → (𝐹 ∘ 𝐺) ∈ (II Cn 𝐽)) | 
| 4 | 1, 2, 3 | syl2anc 584 | . 2
⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ (II Cn 𝐽)) | 
| 5 |  | reparphti.5 | . . 3
⊢ 𝐻 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝐹‘(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)))) | 
| 6 |  | iitopon 24905 | . . . . 5
⊢ II ∈
(TopOn‘(0[,]1)) | 
| 7 | 6 | a1i 11 | . . . 4
⊢ (𝜑 → II ∈
(TopOn‘(0[,]1))) | 
| 8 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 9 | 8 | cnfldtop 24804 | . . . . . . . . . 10
⊢
(TopOpen‘ℂfld) ∈ Top | 
| 10 |  | cnrest2r 23295 | . . . . . . . . . 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 23677 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ 𝑦) ∈ ((II ×t II) Cn
II)) | 
| 13 |  | iirevcn 24957 | . . . . . . . . . . . 12
⊢ (𝑧 ∈ (0[,]1) ↦ (1
− 𝑧)) ∈ (II Cn
II) | 
| 14 | 13 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑧 ∈ (0[,]1) ↦ (1 − 𝑧)) ∈ (II Cn
II)) | 
| 15 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑧 = 𝑦 → (1 − 𝑧) = (1 − 𝑦)) | 
| 16 | 7, 7, 12, 7, 14, 15 | cnmpt21 23679 | . . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (1 − 𝑦)) ∈ ((II
×t II) Cn II)) | 
| 17 | 8 | dfii3 24909 | . . . . . . . . . . 11
⊢ II =
((TopOpen‘ℂfld) ↾t
(0[,]1)) | 
| 18 | 17 | oveq2i 7442 | . . . . . . . . . 10
⊢ ((II
×t II) Cn II) = ((II ×t II) Cn
((TopOpen‘ℂfld) ↾t
(0[,]1))) | 
| 19 | 16, 18 | eleqtrdi 2851 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (1 − 𝑦)) ∈ ((II
×t II) Cn ((TopOpen‘ℂfld)
↾t (0[,]1)))) | 
| 20 | 11, 19 | sseldd 3984 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (1 − 𝑦)) ∈ ((II
×t II) Cn
(TopOpen‘ℂfld))) | 
| 21 | 7, 7 | cnmpt1st 23676 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ 𝑥) ∈ ((II ×t II) Cn
II)) | 
| 22 | 7, 7, 21, 1 | cnmpt21f 23680 | . . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝐺‘𝑥)) ∈ ((II ×t II) Cn
II)) | 
| 23 | 22, 18 | eleqtrdi 2851 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝐺‘𝑥)) ∈ ((II ×t II) Cn
((TopOpen‘ℂfld) ↾t
(0[,]1)))) | 
| 24 | 11, 23 | sseldd 3984 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝐺‘𝑥)) ∈ ((II ×t II) Cn
(TopOpen‘ℂfld))) | 
| 25 | 8 | cnfldtopon 24803 | . . . . . . . . 9
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) | 
| 26 | 25 | a1i 11 | . . . . . . . 8
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) | 
| 27 | 8 | mpomulcn 24891 | . . . . . . . . 9
⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) | 
| 28 | 27 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) | 
| 29 |  | oveq12 7440 | . . . . . . . 8
⊢ ((𝑢 = (1 − 𝑦) ∧ 𝑣 = (𝐺‘𝑥)) → (𝑢 · 𝑣) = ((1 − 𝑦) · (𝐺‘𝑥))) | 
| 30 | 7, 7, 20, 24, 26, 26, 28, 29 | cnmpt22 23682 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ ((1 − 𝑦) · (𝐺‘𝑥))) ∈ ((II ×t II) Cn
(TopOpen‘ℂfld))) | 
| 31 | 9, 10 | ax-mp 5 | . . . . . . . . . 10
⊢ ((II
×t II) Cn ((TopOpen‘ℂfld)
↾t (0[,]1))) ⊆ ((II ×t II) Cn
(TopOpen‘ℂfld)) | 
| 32 | 18, 31 | eqsstri 4030 | . . . . . . . . 9
⊢ ((II
×t II) Cn II) ⊆ ((II ×t II) Cn
(TopOpen‘ℂfld)) | 
| 33 | 32, 12 | sselid 3981 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ 𝑦) ∈ ((II ×t II) Cn
(TopOpen‘ℂfld))) | 
| 34 | 32, 21 | sselid 3981 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ 𝑥) ∈ ((II ×t II) Cn
(TopOpen‘ℂfld))) | 
| 35 |  | oveq12 7440 | . . . . . . . 8
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑥) → (𝑢 · 𝑣) = (𝑦 · 𝑥)) | 
| 36 | 7, 7, 33, 34, 26, 26, 28, 35 | cnmpt22 23682 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝑦 · 𝑥)) ∈ ((II ×t II) Cn
(TopOpen‘ℂfld))) | 
| 37 | 8 | addcn 24887 | . . . . . . . 8
⊢  + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) | 
| 38 | 37 | a1i 11 | . . . . . . 7
⊢ (𝜑 → + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) | 
| 39 | 7, 7, 30, 36, 38 | cnmpt22f 23683 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))) ∈ ((II ×t II) Cn
(TopOpen‘ℂfld))) | 
| 40 |  | iiuni 24907 | . . . . . . . . . . . . . . 15
⊢ (0[,]1) =
∪ II | 
| 41 | 40, 40 | cnf 23254 | . . . . . . . . . . . . . 14
⊢ (𝐺 ∈ (II Cn II) → 𝐺:(0[,]1)⟶(0[,]1)) | 
| 42 | 1, 41 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺:(0[,]1)⟶(0[,]1)) | 
| 43 | 42 | ffvelcdmda 7104 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → (𝐺‘𝑥) ∈ (0[,]1)) | 
| 44 | 43 | adantrr 717 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1))) → (𝐺‘𝑥) ∈ (0[,]1)) | 
| 45 |  | simprl 771 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1))) → 𝑥 ∈ (0[,]1)) | 
| 46 |  | simprr 773 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1))) → 𝑦 ∈ (0[,]1)) | 
| 47 |  | 0re 11263 | . . . . . . . . . . . 12
⊢ 0 ∈
ℝ | 
| 48 |  | 1re 11261 | . . . . . . . . . . . 12
⊢ 1 ∈
ℝ | 
| 49 |  | icccvx 24981 | . . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ) → (((𝐺‘𝑥) ∈ (0[,]1) ∧ 𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) → (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)) ∈ (0[,]1))) | 
| 50 | 47, 48, 49 | mp2an 692 | . . . . . . . . . . 11
⊢ (((𝐺‘𝑥) ∈ (0[,]1) ∧ 𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) → (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)) ∈ (0[,]1)) | 
| 51 | 44, 45, 46, 50 | syl3anc 1373 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1))) → (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)) ∈ (0[,]1)) | 
| 52 | 51 | ralrimivva 3202 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ (0[,]1)∀𝑦 ∈ (0[,]1)(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)) ∈ (0[,]1)) | 
| 53 |  | eqid 2737 | . . . . . . . . . 10
⊢ (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (((1
− 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))) = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))) | 
| 54 | 53 | fmpo 8093 | . . . . . . . . 9
⊢
(∀𝑥 ∈
(0[,]1)∀𝑦 ∈
(0[,]1)(((1 − 𝑦)
· (𝐺‘𝑥)) + (𝑦 · 𝑥)) ∈ (0[,]1) ↔ (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))):((0[,]1) ×
(0[,]1))⟶(0[,]1)) | 
| 55 | 52, 54 | sylib 218 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))):((0[,]1) ×
(0[,]1))⟶(0[,]1)) | 
| 56 | 55 | frnd 6744 | . . . . . . 7
⊢ (𝜑 → ran (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))) ⊆ (0[,]1)) | 
| 57 |  | unitsscn 13540 | . . . . . . . 8
⊢ (0[,]1)
⊆ ℂ | 
| 58 | 57 | a1i 11 | . . . . . . 7
⊢ (𝜑 → (0[,]1) ⊆
ℂ) | 
| 59 |  | cnrest2 23294 | . . . . . . 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))))) | 
| 60 | 26, 56, 58, 59 | syl3anc 1373 | . . . . . 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))))) | 
| 61 | 39, 60 | mpbid 232 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))) ∈ ((II ×t II) Cn
((TopOpen‘ℂfld) ↾t
(0[,]1)))) | 
| 62 | 61, 18 | eleqtrrdi 2852 | . . . 4
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))) ∈ ((II ×t II) Cn
II)) | 
| 63 | 7, 7, 62, 2 | cnmpt21f 23680 | . . 3
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝐹‘(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)))) ∈ ((II ×t II) Cn
𝐽)) | 
| 64 | 5, 63 | eqeltrid 2845 | . 2
⊢ (𝜑 → 𝐻 ∈ ((II ×t II) Cn
𝐽)) | 
| 65 | 42 | ffvelcdmda 7104 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝐺‘𝑠) ∈ (0[,]1)) | 
| 66 | 57, 65 | sselid 3981 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝐺‘𝑠) ∈ ℂ) | 
| 67 | 66 | mullidd 11279 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1 · (𝐺‘𝑠)) = (𝐺‘𝑠)) | 
| 68 |  | elunitcn 13508 | . . . . . . . 8
⊢ (𝑠 ∈ (0[,]1) → 𝑠 ∈
ℂ) | 
| 69 | 68 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → 𝑠 ∈ ℂ) | 
| 70 | 69 | mul02d 11459 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0 · 𝑠) = 0) | 
| 71 | 67, 70 | oveq12d 7449 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((1 · (𝐺‘𝑠)) + (0 · 𝑠)) = ((𝐺‘𝑠) + 0)) | 
| 72 | 66 | addridd 11461 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((𝐺‘𝑠) + 0) = (𝐺‘𝑠)) | 
| 73 | 71, 72 | eqtrd 2777 | . . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((1 · (𝐺‘𝑠)) + (0 · 𝑠)) = (𝐺‘𝑠)) | 
| 74 | 73 | fveq2d 6910 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝐹‘((1 · (𝐺‘𝑠)) + (0 · 𝑠))) = (𝐹‘(𝐺‘𝑠))) | 
| 75 |  | simpr 484 | . . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → 𝑠 ∈ (0[,]1)) | 
| 76 |  | 0elunit 13509 | . . . 4
⊢ 0 ∈
(0[,]1) | 
| 77 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → 𝑦 = 0) | 
| 78 | 77 | oveq2d 7447 | . . . . . . . . 9
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (1 − 𝑦) = (1 − 0)) | 
| 79 |  | 1m0e1 12387 | . . . . . . . . 9
⊢ (1
− 0) = 1 | 
| 80 | 78, 79 | eqtrdi 2793 | . . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (1 − 𝑦) = 1) | 
| 81 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → 𝑥 = 𝑠) | 
| 82 | 81 | fveq2d 6910 | . . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (𝐺‘𝑥) = (𝐺‘𝑠)) | 
| 83 | 80, 82 | oveq12d 7449 | . . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → ((1 − 𝑦) · (𝐺‘𝑥)) = (1 · (𝐺‘𝑠))) | 
| 84 | 77, 81 | oveq12d 7449 | . . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (𝑦 · 𝑥) = (0 · 𝑠)) | 
| 85 | 83, 84 | oveq12d 7449 | . . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)) = ((1 · (𝐺‘𝑠)) + (0 · 𝑠))) | 
| 86 | 85 | fveq2d 6910 | . . . . 5
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (𝐹‘(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))) = (𝐹‘((1 · (𝐺‘𝑠)) + (0 · 𝑠)))) | 
| 87 |  | fvex 6919 | . . . . 5
⊢ (𝐹‘((1 · (𝐺‘𝑠)) + (0 · 𝑠))) ∈ V | 
| 88 | 86, 5, 87 | ovmpoa 7588 | . . . 4
⊢ ((𝑠 ∈ (0[,]1) ∧ 0 ∈
(0[,]1)) → (𝑠𝐻0) = (𝐹‘((1 · (𝐺‘𝑠)) + (0 · 𝑠)))) | 
| 89 | 75, 76, 88 | sylancl 586 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠𝐻0) = (𝐹‘((1 · (𝐺‘𝑠)) + (0 · 𝑠)))) | 
| 90 |  | fvco3 7008 | . . . 4
⊢ ((𝐺:(0[,]1)⟶(0[,]1) ∧
𝑠 ∈ (0[,]1)) →
((𝐹 ∘ 𝐺)‘𝑠) = (𝐹‘(𝐺‘𝑠))) | 
| 91 | 42, 90 | sylan 580 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((𝐹 ∘ 𝐺)‘𝑠) = (𝐹‘(𝐺‘𝑠))) | 
| 92 | 74, 89, 91 | 3eqtr4d 2787 | . 2
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠𝐻0) = ((𝐹 ∘ 𝐺)‘𝑠)) | 
| 93 |  | 1elunit 13510 | . . . 4
⊢ 1 ∈
(0[,]1) | 
| 94 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → 𝑦 = 1) | 
| 95 | 94 | oveq2d 7447 | . . . . . . . . 9
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (1 − 𝑦) = (1 − 1)) | 
| 96 |  | 1m1e0 12338 | . . . . . . . . 9
⊢ (1
− 1) = 0 | 
| 97 | 95, 96 | eqtrdi 2793 | . . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (1 − 𝑦) = 0) | 
| 98 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → 𝑥 = 𝑠) | 
| 99 | 98 | fveq2d 6910 | . . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (𝐺‘𝑥) = (𝐺‘𝑠)) | 
| 100 | 97, 99 | oveq12d 7449 | . . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → ((1 − 𝑦) · (𝐺‘𝑥)) = (0 · (𝐺‘𝑠))) | 
| 101 | 94, 98 | oveq12d 7449 | . . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (𝑦 · 𝑥) = (1 · 𝑠)) | 
| 102 | 100, 101 | oveq12d 7449 | . . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)) = ((0 · (𝐺‘𝑠)) + (1 · 𝑠))) | 
| 103 | 102 | fveq2d 6910 | . . . . 5
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (𝐹‘(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))) = (𝐹‘((0 · (𝐺‘𝑠)) + (1 · 𝑠)))) | 
| 104 |  | fvex 6919 | . . . . 5
⊢ (𝐹‘((0 · (𝐺‘𝑠)) + (1 · 𝑠))) ∈ V | 
| 105 | 103, 5, 104 | ovmpoa 7588 | . . . 4
⊢ ((𝑠 ∈ (0[,]1) ∧ 1 ∈
(0[,]1)) → (𝑠𝐻1) = (𝐹‘((0 · (𝐺‘𝑠)) + (1 · 𝑠)))) | 
| 106 | 75, 93, 105 | sylancl 586 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠𝐻1) = (𝐹‘((0 · (𝐺‘𝑠)) + (1 · 𝑠)))) | 
| 107 | 66 | mul02d 11459 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0 · (𝐺‘𝑠)) = 0) | 
| 108 | 69 | mullidd 11279 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1 · 𝑠) = 𝑠) | 
| 109 | 107, 108 | oveq12d 7449 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((0 · (𝐺‘𝑠)) + (1 · 𝑠)) = (0 + 𝑠)) | 
| 110 | 69 | addlidd 11462 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0 + 𝑠) = 𝑠) | 
| 111 | 109, 110 | eqtrd 2777 | . . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((0 · (𝐺‘𝑠)) + (1 · 𝑠)) = 𝑠) | 
| 112 | 111 | fveq2d 6910 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝐹‘((0 · (𝐺‘𝑠)) + (1 · 𝑠))) = (𝐹‘𝑠)) | 
| 113 | 106, 112 | eqtrd 2777 | . 2
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠𝐻1) = (𝐹‘𝑠)) | 
| 114 |  | reparpht.3 | . . . . . . . . 9
⊢ (𝜑 → (𝐺‘0) = 0) | 
| 115 | 114 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝐺‘0) = 0) | 
| 116 | 115 | oveq2d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((1 − 𝑠) · (𝐺‘0)) = ((1 − 𝑠) · 0)) | 
| 117 |  | ax-1cn 11213 | . . . . . . . . 9
⊢ 1 ∈
ℂ | 
| 118 |  | subcl 11507 | . . . . . . . . 9
⊢ ((1
∈ ℂ ∧ 𝑠
∈ ℂ) → (1 − 𝑠) ∈ ℂ) | 
| 119 | 117, 69, 118 | sylancr 587 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1 − 𝑠) ∈
ℂ) | 
| 120 | 119 | mul01d 11460 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((1 − 𝑠) · 0) =
0) | 
| 121 | 116, 120 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((1 − 𝑠) · (𝐺‘0)) = 0) | 
| 122 | 69 | mul01d 11460 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠 · 0) = 0) | 
| 123 | 121, 122 | oveq12d 7449 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (((1 − 𝑠) · (𝐺‘0)) + (𝑠 · 0)) = (0 + 0)) | 
| 124 |  | 00id 11436 | . . . . 5
⊢ (0 + 0) =
0 | 
| 125 | 123, 124 | eqtrdi 2793 | . . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (((1 − 𝑠) · (𝐺‘0)) + (𝑠 · 0)) = 0) | 
| 126 | 125 | fveq2d 6910 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝐹‘(((1 − 𝑠) · (𝐺‘0)) + (𝑠 · 0))) = (𝐹‘0)) | 
| 127 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → 𝑦 = 𝑠) | 
| 128 | 127 | oveq2d 7447 | . . . . . . . 8
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → (1 − 𝑦) = (1 − 𝑠)) | 
| 129 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → 𝑥 = 0) | 
| 130 | 129 | fveq2d 6910 | . . . . . . . 8
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → (𝐺‘𝑥) = (𝐺‘0)) | 
| 131 | 128, 130 | oveq12d 7449 | . . . . . . 7
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → ((1 − 𝑦) · (𝐺‘𝑥)) = ((1 − 𝑠) · (𝐺‘0))) | 
| 132 | 127, 129 | oveq12d 7449 | . . . . . . 7
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → (𝑦 · 𝑥) = (𝑠 · 0)) | 
| 133 | 131, 132 | oveq12d 7449 | . . . . . 6
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)) = (((1 − 𝑠) · (𝐺‘0)) + (𝑠 · 0))) | 
| 134 | 133 | fveq2d 6910 | . . . . 5
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → (𝐹‘(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))) = (𝐹‘(((1 − 𝑠) · (𝐺‘0)) + (𝑠 · 0)))) | 
| 135 |  | fvex 6919 | . . . . 5
⊢ (𝐹‘(((1 − 𝑠) · (𝐺‘0)) + (𝑠 · 0))) ∈ V | 
| 136 | 134, 5, 135 | ovmpoa 7588 | . . . 4
⊢ ((0
∈ (0[,]1) ∧ 𝑠
∈ (0[,]1)) → (0𝐻𝑠) = (𝐹‘(((1 − 𝑠) · (𝐺‘0)) + (𝑠 · 0)))) | 
| 137 | 76, 75, 136 | sylancr 587 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0𝐻𝑠) = (𝐹‘(((1 − 𝑠) · (𝐺‘0)) + (𝑠 · 0)))) | 
| 138 |  | fvco3 7008 | . . . . . 6
⊢ ((𝐺:(0[,]1)⟶(0[,]1) ∧ 0
∈ (0[,]1)) → ((𝐹
∘ 𝐺)‘0) =
(𝐹‘(𝐺‘0))) | 
| 139 | 42, 76, 138 | sylancl 586 | . . . . 5
⊢ (𝜑 → ((𝐹 ∘ 𝐺)‘0) = (𝐹‘(𝐺‘0))) | 
| 140 | 114 | fveq2d 6910 | . . . . 5
⊢ (𝜑 → (𝐹‘(𝐺‘0)) = (𝐹‘0)) | 
| 141 | 139, 140 | eqtrd 2777 | . . . 4
⊢ (𝜑 → ((𝐹 ∘ 𝐺)‘0) = (𝐹‘0)) | 
| 142 | 141 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((𝐹 ∘ 𝐺)‘0) = (𝐹‘0)) | 
| 143 | 126, 137,
142 | 3eqtr4d 2787 | . 2
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0𝐻𝑠) = ((𝐹 ∘ 𝐺)‘0)) | 
| 144 |  | reparpht.4 | . . . . . . . . 9
⊢ (𝜑 → (𝐺‘1) = 1) | 
| 145 | 144 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝐺‘1) = 1) | 
| 146 | 145 | oveq2d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((1 − 𝑠) · (𝐺‘1)) = ((1 − 𝑠) · 1)) | 
| 147 | 119 | mulridd 11278 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((1 − 𝑠) · 1) = (1 − 𝑠)) | 
| 148 | 146, 147 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((1 − 𝑠) · (𝐺‘1)) = (1 − 𝑠)) | 
| 149 | 69 | mulridd 11278 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠 · 1) = 𝑠) | 
| 150 | 148, 149 | oveq12d 7449 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (((1 − 𝑠) · (𝐺‘1)) + (𝑠 · 1)) = ((1 − 𝑠) + 𝑠)) | 
| 151 |  | npcan 11517 | . . . . . 6
⊢ ((1
∈ ℂ ∧ 𝑠
∈ ℂ) → ((1 − 𝑠) + 𝑠) = 1) | 
| 152 | 117, 69, 151 | sylancr 587 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((1 − 𝑠) + 𝑠) = 1) | 
| 153 | 150, 152 | eqtrd 2777 | . . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (((1 − 𝑠) · (𝐺‘1)) + (𝑠 · 1)) = 1) | 
| 154 | 153 | fveq2d 6910 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝐹‘(((1 − 𝑠) · (𝐺‘1)) + (𝑠 · 1))) = (𝐹‘1)) | 
| 155 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → 𝑦 = 𝑠) | 
| 156 | 155 | oveq2d 7447 | . . . . . . . 8
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (1 − 𝑦) = (1 − 𝑠)) | 
| 157 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → 𝑥 = 1) | 
| 158 | 157 | fveq2d 6910 | . . . . . . . 8
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (𝐺‘𝑥) = (𝐺‘1)) | 
| 159 | 156, 158 | oveq12d 7449 | . . . . . . 7
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → ((1 − 𝑦) · (𝐺‘𝑥)) = ((1 − 𝑠) · (𝐺‘1))) | 
| 160 | 155, 157 | oveq12d 7449 | . . . . . . 7
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (𝑦 · 𝑥) = (𝑠 · 1)) | 
| 161 | 159, 160 | oveq12d 7449 | . . . . . 6
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)) = (((1 − 𝑠) · (𝐺‘1)) + (𝑠 · 1))) | 
| 162 | 161 | fveq2d 6910 | . . . . 5
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (𝐹‘(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))) = (𝐹‘(((1 − 𝑠) · (𝐺‘1)) + (𝑠 · 1)))) | 
| 163 |  | fvex 6919 | . . . . 5
⊢ (𝐹‘(((1 − 𝑠) · (𝐺‘1)) + (𝑠 · 1))) ∈ V | 
| 164 | 162, 5, 163 | ovmpoa 7588 | . . . 4
⊢ ((1
∈ (0[,]1) ∧ 𝑠
∈ (0[,]1)) → (1𝐻𝑠) = (𝐹‘(((1 − 𝑠) · (𝐺‘1)) + (𝑠 · 1)))) | 
| 165 | 93, 75, 164 | sylancr 587 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1𝐻𝑠) = (𝐹‘(((1 − 𝑠) · (𝐺‘1)) + (𝑠 · 1)))) | 
| 166 |  | fvco3 7008 | . . . . . 6
⊢ ((𝐺:(0[,]1)⟶(0[,]1) ∧ 1
∈ (0[,]1)) → ((𝐹
∘ 𝐺)‘1) =
(𝐹‘(𝐺‘1))) | 
| 167 | 42, 93, 166 | sylancl 586 | . . . . 5
⊢ (𝜑 → ((𝐹 ∘ 𝐺)‘1) = (𝐹‘(𝐺‘1))) | 
| 168 | 144 | fveq2d 6910 | . . . . 5
⊢ (𝜑 → (𝐹‘(𝐺‘1)) = (𝐹‘1)) | 
| 169 | 167, 168 | eqtrd 2777 | . . . 4
⊢ (𝜑 → ((𝐹 ∘ 𝐺)‘1) = (𝐹‘1)) | 
| 170 | 169 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((𝐹 ∘ 𝐺)‘1) = (𝐹‘1)) | 
| 171 | 154, 165,
170 | 3eqtr4d 2787 | . 2
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1𝐻𝑠) = ((𝐹 ∘ 𝐺)‘1)) | 
| 172 | 4, 2, 64, 92, 113, 143, 171 | isphtpy2d 25019 | 1
⊢ (𝜑 → 𝐻 ∈ ((𝐹 ∘ 𝐺)(PHtpy‘𝐽)𝐹)) |