Step | Hyp | Ref
| Expression |
1 | | pcoval.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) |
2 | | iiuni 22492 |
. . . . . . . . 9
⊢ (0[,]1) =
∪ II |
3 | | eqid 2610 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 |
4 | 2, 3 | cnf 20860 |
. . . . . . . 8
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐹:(0[,]1)⟶∪
𝐽) |
5 | 1, 4 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:(0[,]1)⟶∪
𝐽) |
6 | | elii1 22542 |
. . . . . . . 8
⊢ (𝑥 ∈ (0[,](1 / 2)) ↔
(𝑥 ∈ (0[,]1) ∧
𝑥 ≤ (1 /
2))) |
7 | | iihalf1 22538 |
. . . . . . . 8
⊢ (𝑥 ∈ (0[,](1 / 2)) → (2
· 𝑥) ∈
(0[,]1)) |
8 | 6, 7 | sylbir 224 |
. . . . . . 7
⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 2)) → (2
· 𝑥) ∈
(0[,]1)) |
9 | | fvco3 6185 |
. . . . . . 7
⊢ ((𝐹:(0[,]1)⟶∪ 𝐽
∧ (2 · 𝑥) ∈
(0[,]1)) → ((𝐻 ∘
𝐹)‘(2 · 𝑥)) = (𝐻‘(𝐹‘(2 · 𝑥)))) |
10 | 5, 8, 9 | syl2an 493 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 2))) → ((𝐻 ∘ 𝐹)‘(2 · 𝑥)) = (𝐻‘(𝐹‘(2 · 𝑥)))) |
11 | 10 | anassrs 678 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → ((𝐻 ∘ 𝐹)‘(2 · 𝑥)) = (𝐻‘(𝐹‘(2 · 𝑥)))) |
12 | 11 | ifeq1da 4066 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → if(𝑥 ≤ (1 / 2), ((𝐻 ∘ 𝐹)‘(2 · 𝑥)), ((𝐻 ∘ 𝐺)‘((2 · 𝑥) − 1))) = if(𝑥 ≤ (1 / 2), (𝐻‘(𝐹‘(2 · 𝑥))), ((𝐻 ∘ 𝐺)‘((2 · 𝑥) − 1)))) |
13 | | pcoval.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) |
14 | 2, 3 | cnf 20860 |
. . . . . . . 8
⊢ (𝐺 ∈ (II Cn 𝐽) → 𝐺:(0[,]1)⟶∪
𝐽) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺:(0[,]1)⟶∪
𝐽) |
16 | | elii2 22543 |
. . . . . . . 8
⊢ ((𝑥 ∈ (0[,]1) ∧ ¬
𝑥 ≤ (1 / 2)) →
𝑥 ∈ ((1 /
2)[,]1)) |
17 | | iihalf2 22540 |
. . . . . . . 8
⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((2
· 𝑥) − 1)
∈ (0[,]1)) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ ((𝑥 ∈ (0[,]1) ∧ ¬
𝑥 ≤ (1 / 2)) → ((2
· 𝑥) − 1)
∈ (0[,]1)) |
19 | | fvco3 6185 |
. . . . . . 7
⊢ ((𝐺:(0[,]1)⟶∪ 𝐽
∧ ((2 · 𝑥)
− 1) ∈ (0[,]1)) → ((𝐻 ∘ 𝐺)‘((2 · 𝑥) − 1)) = (𝐻‘(𝐺‘((2 · 𝑥) − 1)))) |
20 | 15, 18, 19 | syl2an 493 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2))) → ((𝐻 ∘ 𝐺)‘((2 · 𝑥) − 1)) = (𝐻‘(𝐺‘((2 · 𝑥) − 1)))) |
21 | 20 | anassrs 678 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐻 ∘ 𝐺)‘((2 · 𝑥) − 1)) = (𝐻‘(𝐺‘((2 · 𝑥) − 1)))) |
22 | 21 | ifeq2da 4067 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → if(𝑥 ≤ (1 / 2), (𝐻‘(𝐹‘(2 · 𝑥))), ((𝐻 ∘ 𝐺)‘((2 · 𝑥) − 1))) = if(𝑥 ≤ (1 / 2), (𝐻‘(𝐹‘(2 · 𝑥))), (𝐻‘(𝐺‘((2 · 𝑥) − 1))))) |
23 | 12, 22 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → if(𝑥 ≤ (1 / 2), ((𝐻 ∘ 𝐹)‘(2 · 𝑥)), ((𝐻 ∘ 𝐺)‘((2 · 𝑥) − 1))) = if(𝑥 ≤ (1 / 2), (𝐻‘(𝐹‘(2 · 𝑥))), (𝐻‘(𝐺‘((2 · 𝑥) − 1))))) |
24 | 23 | mpteq2dva 4672 |
. 2
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((𝐻 ∘ 𝐹)‘(2 · 𝑥)), ((𝐻 ∘ 𝐺)‘((2 · 𝑥) − 1)))) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝐻‘(𝐹‘(2 · 𝑥))), (𝐻‘(𝐺‘((2 · 𝑥) − 1)))))) |
25 | | copco.6 |
. . . 4
⊢ (𝜑 → 𝐻 ∈ (𝐽 Cn 𝐾)) |
26 | | cnco 20880 |
. . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝐻 ∈ (𝐽 Cn 𝐾)) → (𝐻 ∘ 𝐹) ∈ (II Cn 𝐾)) |
27 | 1, 25, 26 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ (II Cn 𝐾)) |
28 | | cnco 20880 |
. . . 4
⊢ ((𝐺 ∈ (II Cn 𝐽) ∧ 𝐻 ∈ (𝐽 Cn 𝐾)) → (𝐻 ∘ 𝐺) ∈ (II Cn 𝐾)) |
29 | 13, 25, 28 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝐻 ∘ 𝐺) ∈ (II Cn 𝐾)) |
30 | 27, 29 | pcoval 22619 |
. 2
⊢ (𝜑 → ((𝐻 ∘ 𝐹)(*𝑝‘𝐾)(𝐻 ∘ 𝐺)) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((𝐻 ∘ 𝐹)‘(2 · 𝑥)), ((𝐻 ∘ 𝐺)‘((2 · 𝑥) − 1))))) |
31 | 1, 13 | pcoval 22619 |
. . . . . 6
⊢ (𝜑 → (𝐹(*𝑝‘𝐽)𝐺) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1))))) |
32 | | pcoval2.4 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘1) = (𝐺‘0)) |
33 | 1, 13, 32 | pcocn 22625 |
. . . . . 6
⊢ (𝜑 → (𝐹(*𝑝‘𝐽)𝐺) ∈ (II Cn 𝐽)) |
34 | 31, 33 | eqeltrrd 2689 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1)))) ∈ (II Cn 𝐽)) |
35 | 2, 3 | cnf 20860 |
. . . . 5
⊢ ((𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1)))) ∈ (II Cn 𝐽) → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1)))):(0[,]1)⟶∪ 𝐽) |
36 | 34, 35 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1)))):(0[,]1)⟶∪ 𝐽) |
37 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1)))) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1)))) |
38 | 37 | fmpt 6289 |
. . . 4
⊢
(∀𝑥 ∈
(0[,]1)if(𝑥 ≤ (1 / 2),
(𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1))) ∈ ∪ 𝐽
↔ (𝑥 ∈ (0[,]1)
↦ if(𝑥 ≤ (1 / 2),
(𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1)))):(0[,]1)⟶∪ 𝐽) |
39 | 36, 38 | sylibr 223 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ (0[,]1)if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1))) ∈ ∪ 𝐽) |
40 | | eqid 2610 |
. . . . . 6
⊢ ∪ 𝐾 =
∪ 𝐾 |
41 | 3, 40 | cnf 20860 |
. . . . 5
⊢ (𝐻 ∈ (𝐽 Cn 𝐾) → 𝐻:∪ 𝐽⟶∪ 𝐾) |
42 | 25, 41 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐻:∪ 𝐽⟶∪ 𝐾) |
43 | 42 | feqmptd 6159 |
. . 3
⊢ (𝜑 → 𝐻 = (𝑦 ∈ ∪ 𝐽 ↦ (𝐻‘𝑦))) |
44 | | fveq2 6103 |
. . . 4
⊢ (𝑦 = if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1))) → (𝐻‘𝑦) = (𝐻‘if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1))))) |
45 | | fvif 6114 |
. . . 4
⊢ (𝐻‘if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1)))) = if(𝑥 ≤ (1 / 2), (𝐻‘(𝐹‘(2 · 𝑥))), (𝐻‘(𝐺‘((2 · 𝑥) − 1)))) |
46 | 44, 45 | syl6eq 2660 |
. . 3
⊢ (𝑦 = if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1))) → (𝐻‘𝑦) = if(𝑥 ≤ (1 / 2), (𝐻‘(𝐹‘(2 · 𝑥))), (𝐻‘(𝐺‘((2 · 𝑥) − 1))))) |
47 | 39, 31, 43, 46 | fmptcof 6304 |
. 2
⊢ (𝜑 → (𝐻 ∘ (𝐹(*𝑝‘𝐽)𝐺)) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝐻‘(𝐹‘(2 · 𝑥))), (𝐻‘(𝐺‘((2 · 𝑥) − 1)))))) |
48 | 24, 30, 47 | 3eqtr4rd 2655 |
1
⊢ (𝜑 → (𝐻 ∘ (𝐹(*𝑝‘𝐽)𝐺)) = ((𝐻 ∘ 𝐹)(*𝑝‘𝐾)(𝐻 ∘ 𝐺))) |