| Step | Hyp | Ref
| Expression |
| 1 | | phtpcer 25027 |
. . . 4
⊢ (
≃ph‘𝐽) Er (II Cn 𝐽) |
| 2 | 1 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → (
≃ph‘𝐽) Er (II Cn 𝐽)) |
| 3 | | pcophtb.1 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘1) = (𝐺‘1)) |
| 4 | | pcophtb.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) |
| 5 | | pcophtb.h |
. . . . . . . . . . 11
⊢ 𝐻 = (𝑥 ∈ (0[,]1) ↦ (𝐺‘(1 − 𝑥))) |
| 6 | 5 | pcorevcl 25058 |
. . . . . . . . . 10
⊢ (𝐺 ∈ (II Cn 𝐽) → (𝐻 ∈ (II Cn 𝐽) ∧ (𝐻‘0) = (𝐺‘1) ∧ (𝐻‘1) = (𝐺‘0))) |
| 7 | 4, 6 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐻 ∈ (II Cn 𝐽) ∧ (𝐻‘0) = (𝐺‘1) ∧ (𝐻‘1) = (𝐺‘0))) |
| 8 | 7 | simp2d 1144 |
. . . . . . . 8
⊢ (𝜑 → (𝐻‘0) = (𝐺‘1)) |
| 9 | 3, 8 | eqtr4d 2780 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘1) = (𝐻‘0)) |
| 10 | 7 | simp1d 1143 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ∈ (II Cn 𝐽)) |
| 11 | 10, 4 | pco0 25047 |
. . . . . . 7
⊢ (𝜑 → ((𝐻(*𝑝‘𝐽)𝐺)‘0) = (𝐻‘0)) |
| 12 | 9, 11 | eqtr4d 2780 |
. . . . . 6
⊢ (𝜑 → (𝐹‘1) = ((𝐻(*𝑝‘𝐽)𝐺)‘0)) |
| 13 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → (𝐹‘1) = ((𝐻(*𝑝‘𝐽)𝐺)‘0)) |
| 14 | | pcophtb.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) |
| 15 | 14 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → 𝐹 ∈ (II Cn 𝐽)) |
| 16 | 2, 15 | erref 8765 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → 𝐹( ≃ph‘𝐽)𝐹) |
| 17 | | eqid 2737 |
. . . . . . . 8
⊢ ((0[,]1)
× {(𝐺‘1)}) =
((0[,]1) × {(𝐺‘1)}) |
| 18 | 5, 17 | pcorev 25060 |
. . . . . . 7
⊢ (𝐺 ∈ (II Cn 𝐽) → (𝐻(*𝑝‘𝐽)𝐺)( ≃ph‘𝐽)((0[,]1) × {(𝐺‘1)})) |
| 19 | 4, 18 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐻(*𝑝‘𝐽)𝐺)( ≃ph‘𝐽)((0[,]1) × {(𝐺‘1)})) |
| 20 | 19 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → (𝐻(*𝑝‘𝐽)𝐺)( ≃ph‘𝐽)((0[,]1) × {(𝐺‘1)})) |
| 21 | 13, 16, 20 | pcohtpy 25053 |
. . . 4
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → (𝐹(*𝑝‘𝐽)(𝐻(*𝑝‘𝐽)𝐺))( ≃ph‘𝐽)(𝐹(*𝑝‘𝐽)((0[,]1) × {(𝐺‘1)}))) |
| 22 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → (𝐹‘1) = (𝐺‘1)) |
| 23 | 17 | pcopt2 25056 |
. . . . 5
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘1) = (𝐺‘1)) → (𝐹(*𝑝‘𝐽)((0[,]1) × {(𝐺‘1)}))(
≃ph‘𝐽)𝐹) |
| 24 | 15, 22, 23 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → (𝐹(*𝑝‘𝐽)((0[,]1) × {(𝐺‘1)}))(
≃ph‘𝐽)𝐹) |
| 25 | 2, 21, 24 | ertrd 8761 |
. . 3
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → (𝐹(*𝑝‘𝐽)(𝐻(*𝑝‘𝐽)𝐺))( ≃ph‘𝐽)𝐹) |
| 26 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → 𝐻 ∈ (II Cn 𝐽)) |
| 27 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → 𝐺 ∈ (II Cn 𝐽)) |
| 28 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → (𝐹‘1) = (𝐻‘0)) |
| 29 | 7 | simp3d 1145 |
. . . . . . 7
⊢ (𝜑 → (𝐻‘1) = (𝐺‘0)) |
| 30 | 29 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → (𝐻‘1) = (𝐺‘0)) |
| 31 | | eqid 2737 |
. . . . . 6
⊢ (𝑦 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2)))) = (𝑦 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2)))) |
| 32 | 15, 26, 27, 28, 30, 31 | pcoass 25057 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → ((𝐹(*𝑝‘𝐽)𝐻)(*𝑝‘𝐽)𝐺)( ≃ph‘𝐽)(𝐹(*𝑝‘𝐽)(𝐻(*𝑝‘𝐽)𝐺))) |
| 33 | 14, 10 | pco1 25048 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐻)‘1) = (𝐻‘1)) |
| 34 | 33, 29 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐻)‘1) = (𝐺‘0)) |
| 35 | 34 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → ((𝐹(*𝑝‘𝐽)𝐻)‘1) = (𝐺‘0)) |
| 36 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) |
| 37 | 2, 27 | erref 8765 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → 𝐺( ≃ph‘𝐽)𝐺) |
| 38 | 35, 36, 37 | pcohtpy 25053 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → ((𝐹(*𝑝‘𝐽)𝐻)(*𝑝‘𝐽)𝐺)( ≃ph‘𝐽)(𝑃(*𝑝‘𝐽)𝐺)) |
| 39 | 2, 32, 38 | ertr3d 8763 |
. . . 4
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → (𝐹(*𝑝‘𝐽)(𝐻(*𝑝‘𝐽)𝐺))( ≃ph‘𝐽)(𝑃(*𝑝‘𝐽)𝐺)) |
| 40 | | pcophtb.0 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘0) = (𝐺‘0)) |
| 41 | 40 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → (𝐹‘0) = (𝐺‘0)) |
| 42 | 41 | eqcomd 2743 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → (𝐺‘0) = (𝐹‘0)) |
| 43 | | pcophtb.p |
. . . . . 6
⊢ 𝑃 = ((0[,]1) × {(𝐹‘0)}) |
| 44 | 43 | pcopt 25055 |
. . . . 5
⊢ ((𝐺 ∈ (II Cn 𝐽) ∧ (𝐺‘0) = (𝐹‘0)) → (𝑃(*𝑝‘𝐽)𝐺)( ≃ph‘𝐽)𝐺) |
| 45 | 27, 42, 44 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → (𝑃(*𝑝‘𝐽)𝐺)( ≃ph‘𝐽)𝐺) |
| 46 | 2, 39, 45 | ertrd 8761 |
. . 3
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → (𝐹(*𝑝‘𝐽)(𝐻(*𝑝‘𝐽)𝐺))( ≃ph‘𝐽)𝐺) |
| 47 | 2, 25, 46 | ertr3d 8763 |
. 2
⊢ ((𝜑 ∧ (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) → 𝐹( ≃ph‘𝐽)𝐺) |
| 48 | 1 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝐹( ≃ph‘𝐽)𝐺) → (
≃ph‘𝐽) Er (II Cn 𝐽)) |
| 49 | 9 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐹( ≃ph‘𝐽)𝐺) → (𝐹‘1) = (𝐻‘0)) |
| 50 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐹( ≃ph‘𝐽)𝐺) → 𝐹( ≃ph‘𝐽)𝐺) |
| 51 | 10 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹( ≃ph‘𝐽)𝐺) → 𝐻 ∈ (II Cn 𝐽)) |
| 52 | 48, 51 | erref 8765 |
. . . 4
⊢ ((𝜑 ∧ 𝐹( ≃ph‘𝐽)𝐺) → 𝐻( ≃ph‘𝐽)𝐻) |
| 53 | 49, 50, 52 | pcohtpy 25053 |
. . 3
⊢ ((𝜑 ∧ 𝐹( ≃ph‘𝐽)𝐺) → (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)(𝐺(*𝑝‘𝐽)𝐻)) |
| 54 | | eqid 2737 |
. . . . . . 7
⊢ ((0[,]1)
× {(𝐺‘0)}) =
((0[,]1) × {(𝐺‘0)}) |
| 55 | 5, 54 | pcorev2 25061 |
. . . . . 6
⊢ (𝐺 ∈ (II Cn 𝐽) → (𝐺(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)((0[,]1) × {(𝐺‘0)})) |
| 56 | 4, 55 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐺(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)((0[,]1) × {(𝐺‘0)})) |
| 57 | 40 | sneqd 4638 |
. . . . . . 7
⊢ (𝜑 → {(𝐹‘0)} = {(𝐺‘0)}) |
| 58 | 57 | xpeq2d 5715 |
. . . . . 6
⊢ (𝜑 → ((0[,]1) × {(𝐹‘0)}) = ((0[,]1) ×
{(𝐺‘0)})) |
| 59 | 43, 58 | eqtrid 2789 |
. . . . 5
⊢ (𝜑 → 𝑃 = ((0[,]1) × {(𝐺‘0)})) |
| 60 | 56, 59 | breqtrrd 5171 |
. . . 4
⊢ (𝜑 → (𝐺(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) |
| 61 | 60 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐹( ≃ph‘𝐽)𝐺) → (𝐺(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) |
| 62 | 48, 53, 61 | ertrd 8761 |
. 2
⊢ ((𝜑 ∧ 𝐹( ≃ph‘𝐽)𝐺) → (𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃) |
| 63 | 47, 62 | impbida 801 |
1
⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃 ↔ 𝐹( ≃ph‘𝐽)𝐺)) |