| Step | Hyp | Ref
| Expression |
| 1 | | pi1xfr.j |
. . 3
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
| 2 | | iitopon 24905 |
. . . . 5
⊢ II ∈
(TopOn‘(0[,]1)) |
| 3 | | pi1xfr.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) |
| 4 | | cnf2 23257 |
. . . . 5
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (II Cn 𝐽)) → 𝐹:(0[,]1)⟶𝑋) |
| 5 | 2, 1, 3, 4 | mp3an2i 1468 |
. . . 4
⊢ (𝜑 → 𝐹:(0[,]1)⟶𝑋) |
| 6 | | 0elunit 13509 |
. . . 4
⊢ 0 ∈
(0[,]1) |
| 7 | | ffvelcdm 7101 |
. . . 4
⊢ ((𝐹:(0[,]1)⟶𝑋 ∧ 0 ∈ (0[,]1)) →
(𝐹‘0) ∈ 𝑋) |
| 8 | 5, 6, 7 | sylancl 586 |
. . 3
⊢ (𝜑 → (𝐹‘0) ∈ 𝑋) |
| 9 | | pi1xfr.p |
. . . 4
⊢ 𝑃 = (𝐽 π1 (𝐹‘0)) |
| 10 | 9 | pi1grp 25083 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐹‘0) ∈ 𝑋) → 𝑃 ∈ Grp) |
| 11 | 1, 8, 10 | syl2anc 584 |
. 2
⊢ (𝜑 → 𝑃 ∈ Grp) |
| 12 | | 1elunit 13510 |
. . . 4
⊢ 1 ∈
(0[,]1) |
| 13 | | ffvelcdm 7101 |
. . . 4
⊢ ((𝐹:(0[,]1)⟶𝑋 ∧ 1 ∈ (0[,]1)) →
(𝐹‘1) ∈ 𝑋) |
| 14 | 5, 12, 13 | sylancl 586 |
. . 3
⊢ (𝜑 → (𝐹‘1) ∈ 𝑋) |
| 15 | | pi1xfr.q |
. . . 4
⊢ 𝑄 = (𝐽 π1 (𝐹‘1)) |
| 16 | 15 | pi1grp 25083 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐹‘1) ∈ 𝑋) → 𝑄 ∈ Grp) |
| 17 | 1, 14, 16 | syl2anc 584 |
. 2
⊢ (𝜑 → 𝑄 ∈ Grp) |
| 18 | | pi1xfr.b |
. . . 4
⊢ 𝐵 = (Base‘𝑃) |
| 19 | | pi1xfr.g |
. . . 4
⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝐵 ↦ 〈[𝑔](
≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)〉) |
| 20 | | pi1xfr.i |
. . . . . . 7
⊢ 𝐼 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥))) |
| 21 | 20 | pcorevcl 25058 |
. . . . . 6
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐼 ∈ (II Cn 𝐽) ∧ (𝐼‘0) = (𝐹‘1) ∧ (𝐼‘1) = (𝐹‘0))) |
| 22 | 3, 21 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐼 ∈ (II Cn 𝐽) ∧ (𝐼‘0) = (𝐹‘1) ∧ (𝐼‘1) = (𝐹‘0))) |
| 23 | 22 | simp1d 1143 |
. . . 4
⊢ (𝜑 → 𝐼 ∈ (II Cn 𝐽)) |
| 24 | 22 | simp2d 1144 |
. . . . 5
⊢ (𝜑 → (𝐼‘0) = (𝐹‘1)) |
| 25 | 24 | eqcomd 2743 |
. . . 4
⊢ (𝜑 → (𝐹‘1) = (𝐼‘0)) |
| 26 | 22 | simp3d 1145 |
. . . 4
⊢ (𝜑 → (𝐼‘1) = (𝐹‘0)) |
| 27 | 9, 15, 18, 19, 1, 3, 23, 25, 26 | pi1xfrf 25086 |
. . 3
⊢ (𝜑 → 𝐺:𝐵⟶(Base‘𝑄)) |
| 28 | 18 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = (Base‘𝑃)) |
| 29 | 9, 1, 8, 28 | pi1bas2 25074 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = (∪ 𝐵 / (
≃ph‘𝐽))) |
| 30 | 29 | eleq2d 2827 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (∪ 𝐵 / (
≃ph‘𝐽)))) |
| 31 | 30 | biimpa 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ (∪ 𝐵 / (
≃ph‘𝐽))) |
| 32 | | eqid 2737 |
. . . . . 6
⊢ (∪ 𝐵
/ ( ≃ph‘𝐽)) = (∪ 𝐵 / (
≃ph‘𝐽)) |
| 33 | | fvoveq1 7454 |
. . . . . . . 8
⊢ ([𝑓](
≃ph‘𝐽) = 𝑦 → (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = (𝐺‘(𝑦(+g‘𝑃)𝑧))) |
| 34 | | fveq2 6906 |
. . . . . . . . 9
⊢ ([𝑓](
≃ph‘𝐽) = 𝑦 → (𝐺‘[𝑓]( ≃ph‘𝐽)) = (𝐺‘𝑦)) |
| 35 | 34 | oveq1d 7446 |
. . . . . . . 8
⊢ ([𝑓](
≃ph‘𝐽) = 𝑦 → ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧))) |
| 36 | 33, 35 | eqeq12d 2753 |
. . . . . . 7
⊢ ([𝑓](
≃ph‘𝐽) = 𝑦 → ((𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧)) ↔ (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧)))) |
| 37 | 36 | ralbidv 3178 |
. . . . . 6
⊢ ([𝑓](
≃ph‘𝐽) = 𝑦 → (∀𝑧 ∈ 𝐵 (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧)) ↔ ∀𝑧 ∈ 𝐵 (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧)))) |
| 38 | 29 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ (∪ 𝐵 / (
≃ph‘𝐽)))) |
| 39 | 38 | biimpa 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ (∪ 𝐵 / (
≃ph‘𝐽))) |
| 40 | 39 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ (∪ 𝐵 / (
≃ph‘𝐽))) |
| 41 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ ([ℎ](
≃ph‘𝐽) = 𝑧 → ([𝑓]( ≃ph‘𝐽)(+g‘𝑃)[ℎ]( ≃ph‘𝐽)) = ([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) |
| 42 | 41 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ([ℎ](
≃ph‘𝐽) = 𝑧 → (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)[ℎ]( ≃ph‘𝐽))) = (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧))) |
| 43 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ ([ℎ](
≃ph‘𝐽) = 𝑧 → (𝐺‘[ℎ]( ≃ph‘𝐽)) = (𝐺‘𝑧)) |
| 44 | 43 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ([ℎ](
≃ph‘𝐽) = 𝑧 → ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘[ℎ]( ≃ph‘𝐽))) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧))) |
| 45 | 42, 44 | eqeq12d 2753 |
. . . . . . . . 9
⊢ ([ℎ](
≃ph‘𝐽) = 𝑧 → ((𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)[ℎ]( ≃ph‘𝐽))) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘[ℎ]( ≃ph‘𝐽))) ↔ (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧)))) |
| 46 | | phtpcer 25027 |
. . . . . . . . . . . . . 14
⊢ (
≃ph‘𝐽) Er (II Cn 𝐽) |
| 47 | 46 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (
≃ph‘𝐽) Er (II Cn 𝐽)) |
| 48 | 9, 1, 8, 28 | pi1eluni 25075 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑓 ∈ ∪ 𝐵 ↔ (𝑓 ∈ (II Cn 𝐽) ∧ (𝑓‘0) = (𝐹‘0) ∧ (𝑓‘1) = (𝐹‘0)))) |
| 49 | 48 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (𝑓 ∈ (II Cn 𝐽) ∧ (𝑓‘0) = (𝐹‘0) ∧ (𝑓‘1) = (𝐹‘0))) |
| 50 | 49 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → 𝑓 ∈ (II Cn 𝐽)) |
| 51 | 50 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → 𝑓 ∈ (II Cn 𝐽)) |
| 52 | 9, 1, 8, 28 | pi1eluni 25075 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (ℎ ∈ ∪ 𝐵 ↔ (ℎ ∈ (II Cn 𝐽) ∧ (ℎ‘0) = (𝐹‘0) ∧ (ℎ‘1) = (𝐹‘0)))) |
| 53 | 52 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (ℎ ∈ ∪ 𝐵 ↔ (ℎ ∈ (II Cn 𝐽) ∧ (ℎ‘0) = (𝐹‘0) ∧ (ℎ‘1) = (𝐹‘0)))) |
| 54 | 53 | biimp3a 1471 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (ℎ ∈ (II Cn 𝐽) ∧ (ℎ‘0) = (𝐹‘0) ∧ (ℎ‘1) = (𝐹‘0))) |
| 55 | 54 | simp1d 1143 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ℎ ∈ (II Cn 𝐽)) |
| 56 | 51, 55 | pco0 25047 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝑓(*𝑝‘𝐽)ℎ)‘0) = (𝑓‘0)) |
| 57 | 49 | simp2d 1144 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (𝑓‘0) = (𝐹‘0)) |
| 58 | 57 | 3adant3 1133 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝑓‘0) = (𝐹‘0)) |
| 59 | 56, 58 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝑓(*𝑝‘𝐽)ℎ)‘0) = (𝐹‘0)) |
| 60 | 49 | simp3d 1145 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (𝑓‘1) = (𝐹‘0)) |
| 61 | 60 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝑓‘1) = (𝐹‘0)) |
| 62 | 54 | simp2d 1144 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (ℎ‘0) = (𝐹‘0)) |
| 63 | 61, 62 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝑓‘1) = (ℎ‘0)) |
| 64 | 51, 55, 63 | pcocn 25050 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝑓(*𝑝‘𝐽)ℎ) ∈ (II Cn 𝐽)) |
| 65 | 3 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → 𝐹 ∈ (II Cn 𝐽)) |
| 66 | 64, 65 | pco0 25047 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (((𝑓(*𝑝‘𝐽)ℎ)(*𝑝‘𝐽)𝐹)‘0) = ((𝑓(*𝑝‘𝐽)ℎ)‘0)) |
| 67 | 26 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼‘1) = (𝐹‘0)) |
| 68 | 59, 66, 67 | 3eqtr4rd 2788 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼‘1) = (((𝑓(*𝑝‘𝐽)ℎ)(*𝑝‘𝐽)𝐹)‘0)) |
| 69 | 23 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → 𝐼 ∈ (II Cn 𝐽)) |
| 70 | 47, 69 | erref 8765 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → 𝐼( ≃ph‘𝐽)𝐼) |
| 71 | 54 | simp3d 1145 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (ℎ‘1) = (𝐹‘0)) |
| 72 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ (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)))) |
| 73 | 51, 55, 65, 63, 71, 72 | pcoass 25057 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝑓(*𝑝‘𝐽)ℎ)(*𝑝‘𝐽)𝐹)( ≃ph‘𝐽)(𝑓(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))) |
| 74 | 55, 65 | pco0 25047 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((ℎ(*𝑝‘𝐽)𝐹)‘0) = (ℎ‘0)) |
| 75 | 63, 74 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝑓‘1) = ((ℎ(*𝑝‘𝐽)𝐹)‘0)) |
| 76 | 47, 51 | erref 8765 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → 𝑓( ≃ph‘𝐽)𝑓) |
| 77 | 65, 69 | pco1 25048 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐹(*𝑝‘𝐽)𝐼)‘1) = (𝐼‘1)) |
| 78 | 62, 74, 67 | 3eqtr4rd 2788 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼‘1) = ((ℎ(*𝑝‘𝐽)𝐹)‘0)) |
| 79 | 77, 78 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐹(*𝑝‘𝐽)𝐼)‘1) = ((ℎ(*𝑝‘𝐽)𝐹)‘0)) |
| 80 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((0[,]1)
× {(𝐹‘0)}) =
((0[,]1) × {(𝐹‘0)}) |
| 81 | 20, 80 | pcorev2 25061 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐹(*𝑝‘𝐽)𝐼)( ≃ph‘𝐽)((0[,]1) × {(𝐹‘0)})) |
| 82 | 65, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐹(*𝑝‘𝐽)𝐼)( ≃ph‘𝐽)((0[,]1) × {(𝐹‘0)})) |
| 83 | 55, 65, 71 | pcocn 25050 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (ℎ(*𝑝‘𝐽)𝐹) ∈ (II Cn 𝐽)) |
| 84 | 47, 83 | erref 8765 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (ℎ(*𝑝‘𝐽)𝐹)( ≃ph‘𝐽)(ℎ(*𝑝‘𝐽)𝐹)) |
| 85 | 79, 82, 84 | pcohtpy 25053 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐹(*𝑝‘𝐽)𝐼)(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))( ≃ph‘𝐽)(((0[,]1) × {(𝐹‘0)})(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))) |
| 86 | 74, 62 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((ℎ(*𝑝‘𝐽)𝐹)‘0) = (𝐹‘0)) |
| 87 | 80 | pcopt 25055 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((ℎ(*𝑝‘𝐽)𝐹) ∈ (II Cn 𝐽) ∧ ((ℎ(*𝑝‘𝐽)𝐹)‘0) = (𝐹‘0)) → (((0[,]1) × {(𝐹‘0)})(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))( ≃ph‘𝐽)(ℎ(*𝑝‘𝐽)𝐹)) |
| 88 | 83, 86, 87 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (((0[,]1) ×
{(𝐹‘0)})(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))( ≃ph‘𝐽)(ℎ(*𝑝‘𝐽)𝐹)) |
| 89 | 47, 85, 88 | ertrd 8761 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐹(*𝑝‘𝐽)𝐼)(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))( ≃ph‘𝐽)(ℎ(*𝑝‘𝐽)𝐹)) |
| 90 | 24 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼‘0) = (𝐹‘1)) |
| 91 | 90 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐹‘1) = (𝐼‘0)) |
| 92 | 65, 69, 83, 91, 78, 72 | pcoass 25057 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐹(*𝑝‘𝐽)𝐼)(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))( ≃ph‘𝐽)(𝐹(*𝑝‘𝐽)(𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹)))) |
| 93 | 47, 89, 92 | ertr3d 8763 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (ℎ(*𝑝‘𝐽)𝐹)( ≃ph‘𝐽)(𝐹(*𝑝‘𝐽)(𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹)))) |
| 94 | 75, 76, 93 | pcohtpy 25053 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝑓(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))( ≃ph‘𝐽)(𝑓(*𝑝‘𝐽)(𝐹(*𝑝‘𝐽)(𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))))) |
| 95 | 69, 83, 78 | pcocn 25050 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹)) ∈ (II Cn 𝐽)) |
| 96 | 69, 83 | pco0 25047 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))‘0) = (𝐼‘0)) |
| 97 | 96, 90 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))‘0) = (𝐹‘1)) |
| 98 | 97 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐹‘1) = ((𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))‘0)) |
| 99 | 51, 65, 95, 61, 98, 72 | pcoass 25057 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝑓(*𝑝‘𝐽)𝐹)(*𝑝‘𝐽)(𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹)))( ≃ph‘𝐽)(𝑓(*𝑝‘𝐽)(𝐹(*𝑝‘𝐽)(𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))))) |
| 100 | 47, 94, 99 | ertr4d 8764 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝑓(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))( ≃ph‘𝐽)((𝑓(*𝑝‘𝐽)𝐹)(*𝑝‘𝐽)(𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹)))) |
| 101 | 47, 73, 100 | ertrd 8761 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝑓(*𝑝‘𝐽)ℎ)(*𝑝‘𝐽)𝐹)( ≃ph‘𝐽)((𝑓(*𝑝‘𝐽)𝐹)(*𝑝‘𝐽)(𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹)))) |
| 102 | 68, 70, 101 | pcohtpy 25053 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼(*𝑝‘𝐽)((𝑓(*𝑝‘𝐽)ℎ)(*𝑝‘𝐽)𝐹))( ≃ph‘𝐽)(𝐼(*𝑝‘𝐽)((𝑓(*𝑝‘𝐽)𝐹)(*𝑝‘𝐽)(𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))))) |
| 103 | 3 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → 𝐹 ∈ (II Cn 𝐽)) |
| 104 | 50, 103, 60 | pcocn 25050 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (𝑓(*𝑝‘𝐽)𝐹) ∈ (II Cn 𝐽)) |
| 105 | 104 | 3adant3 1133 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝑓(*𝑝‘𝐽)𝐹) ∈ (II Cn 𝐽)) |
| 106 | 50, 103 | pco0 25047 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → ((𝑓(*𝑝‘𝐽)𝐹)‘0) = (𝑓‘0)) |
| 107 | 26 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (𝐼‘1) = (𝐹‘0)) |
| 108 | 57, 106, 107 | 3eqtr4rd 2788 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (𝐼‘1) = ((𝑓(*𝑝‘𝐽)𝐹)‘0)) |
| 109 | 108 | 3adant3 1133 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼‘1) = ((𝑓(*𝑝‘𝐽)𝐹)‘0)) |
| 110 | 51, 65 | pco1 25048 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝑓(*𝑝‘𝐽)𝐹)‘1) = (𝐹‘1)) |
| 111 | 110, 97 | eqtr4d 2780 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝑓(*𝑝‘𝐽)𝐹)‘1) = ((𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))‘0)) |
| 112 | 69, 105, 95, 109, 111, 72 | pcoass 25057 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹))(*𝑝‘𝐽)(𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹)))( ≃ph‘𝐽)(𝐼(*𝑝‘𝐽)((𝑓(*𝑝‘𝐽)𝐹)(*𝑝‘𝐽)(𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))))) |
| 113 | 47, 102, 112 | ertr4d 8764 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼(*𝑝‘𝐽)((𝑓(*𝑝‘𝐽)ℎ)(*𝑝‘𝐽)𝐹))( ≃ph‘𝐽)((𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹))(*𝑝‘𝐽)(𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹)))) |
| 114 | 47, 113 | erthi 8798 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → [(𝐼(*𝑝‘𝐽)((𝑓(*𝑝‘𝐽)ℎ)(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽) = [((𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹))(*𝑝‘𝐽)(𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹)))](
≃ph‘𝐽)) |
| 115 | 1 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → 𝐽 ∈ (TopOn‘𝑋)) |
| 116 | 51, 55 | pco1 25048 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝑓(*𝑝‘𝐽)ℎ)‘1) = (ℎ‘1)) |
| 117 | 116, 71 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝑓(*𝑝‘𝐽)ℎ)‘1) = (𝐹‘0)) |
| 118 | 9, 1, 8, 28 | pi1eluni 25075 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑓(*𝑝‘𝐽)ℎ) ∈ ∪ 𝐵 ↔ ((𝑓(*𝑝‘𝐽)ℎ) ∈ (II Cn 𝐽) ∧ ((𝑓(*𝑝‘𝐽)ℎ)‘0) = (𝐹‘0) ∧ ((𝑓(*𝑝‘𝐽)ℎ)‘1) = (𝐹‘0)))) |
| 119 | 118 | 3ad2ant1 1134 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝑓(*𝑝‘𝐽)ℎ) ∈ ∪ 𝐵 ↔ ((𝑓(*𝑝‘𝐽)ℎ) ∈ (II Cn 𝐽) ∧ ((𝑓(*𝑝‘𝐽)ℎ)‘0) = (𝐹‘0) ∧ ((𝑓(*𝑝‘𝐽)ℎ)‘1) = (𝐹‘0)))) |
| 120 | 64, 59, 117, 119 | mpbir3and 1343 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝑓(*𝑝‘𝐽)ℎ) ∈ ∪ 𝐵) |
| 121 | 9, 15, 18, 19, 115, 65, 69, 91, 67, 120 | pi1xfrval 25087 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐺‘[(𝑓(*𝑝‘𝐽)ℎ)]( ≃ph‘𝐽)) = [(𝐼(*𝑝‘𝐽)((𝑓(*𝑝‘𝐽)ℎ)(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)) |
| 122 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑄) =
(Base‘𝑄) |
| 123 | 14 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐹‘1) ∈ 𝑋) |
| 124 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(+g‘𝑄) = (+g‘𝑄) |
| 125 | 23 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → 𝐼 ∈ (II Cn 𝐽)) |
| 126 | 125, 104,
108 | pcocn 25050 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹)) ∈ (II Cn 𝐽)) |
| 127 | 126 | 3adant3 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹)) ∈ (II Cn 𝐽)) |
| 128 | 125, 104 | pco0 25047 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → ((𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹))‘0) = (𝐼‘0)) |
| 129 | 24 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (𝐼‘0) = (𝐹‘1)) |
| 130 | 128, 129 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → ((𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹))‘0) = (𝐹‘1)) |
| 131 | 130 | 3adant3 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹))‘0) = (𝐹‘1)) |
| 132 | 125, 104 | pco1 25048 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → ((𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹))‘1) = ((𝑓(*𝑝‘𝐽)𝐹)‘1)) |
| 133 | 50, 103 | pco1 25048 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → ((𝑓(*𝑝‘𝐽)𝐹)‘1) = (𝐹‘1)) |
| 134 | 132, 133 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → ((𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹))‘1) = (𝐹‘1)) |
| 135 | 134 | 3adant3 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹))‘1) = (𝐹‘1)) |
| 136 | | eqidd 2738 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (Base‘𝑄) = (Base‘𝑄)) |
| 137 | 15, 115, 123, 136 | pi1eluni 25075 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹)) ∈ ∪
(Base‘𝑄) ↔
((𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹)) ∈ (II Cn 𝐽) ∧ ((𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹))‘0) = (𝐹‘1) ∧ ((𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹))‘1) = (𝐹‘1)))) |
| 138 | 127, 131,
135, 137 | mpbir3and 1343 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹)) ∈ ∪
(Base‘𝑄)) |
| 139 | 69, 83 | pco1 25048 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))‘1) = ((ℎ(*𝑝‘𝐽)𝐹)‘1)) |
| 140 | 55, 65 | pco1 25048 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((ℎ(*𝑝‘𝐽)𝐹)‘1) = (𝐹‘1)) |
| 141 | 139, 140 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))‘1) = (𝐹‘1)) |
| 142 | 15, 115, 123, 136 | pi1eluni 25075 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹)) ∈ ∪
(Base‘𝑄) ↔
((𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹)) ∈ (II Cn 𝐽) ∧ ((𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))‘0) = (𝐹‘1) ∧ ((𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))‘1) = (𝐹‘1)))) |
| 143 | 95, 97, 141, 142 | mpbir3and 1343 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹)) ∈ ∪
(Base‘𝑄)) |
| 144 | 15, 122, 115, 123, 124, 138, 143 | pi1addval 25081 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ([(𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)(+g‘𝑄)[(𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)) = [((𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹))(*𝑝‘𝐽)(𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹)))](
≃ph‘𝐽)) |
| 145 | 114, 121,
144 | 3eqtr4d 2787 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐺‘[(𝑓(*𝑝‘𝐽)ℎ)]( ≃ph‘𝐽)) = ([(𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)(+g‘𝑄)[(𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽))) |
| 146 | 8 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐹‘0) ∈ 𝑋) |
| 147 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(+g‘𝑃) = (+g‘𝑃) |
| 148 | | simp2 1138 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → 𝑓 ∈ ∪ 𝐵) |
| 149 | | simp3 1139 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ℎ ∈ ∪ 𝐵) |
| 150 | 9, 18, 115, 146, 147, 148, 149 | pi1addval 25081 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ([𝑓]( ≃ph‘𝐽)(+g‘𝑃)[ℎ]( ≃ph‘𝐽)) = [(𝑓(*𝑝‘𝐽)ℎ)]( ≃ph‘𝐽)) |
| 151 | 150 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)[ℎ]( ≃ph‘𝐽))) = (𝐺‘[(𝑓(*𝑝‘𝐽)ℎ)]( ≃ph‘𝐽))) |
| 152 | 1 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → 𝐽 ∈ (TopOn‘𝑋)) |
| 153 | 25 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (𝐹‘1) = (𝐼‘0)) |
| 154 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → 𝑓 ∈ ∪ 𝐵) |
| 155 | 9, 15, 18, 19, 152, 103, 125, 153, 107, 154 | pi1xfrval 25087 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (𝐺‘[𝑓]( ≃ph‘𝐽)) = [(𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)) |
| 156 | 155 | 3adant3 1133 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐺‘[𝑓]( ≃ph‘𝐽)) = [(𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)) |
| 157 | 9, 15, 18, 19, 115, 65, 69, 91, 67, 149 | pi1xfrval 25087 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐺‘[ℎ]( ≃ph‘𝐽)) = [(𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)) |
| 158 | 156, 157 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘[ℎ]( ≃ph‘𝐽))) = ([(𝐼(*𝑝‘𝐽)(𝑓(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)(+g‘𝑄)[(𝐼(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽))) |
| 159 | 145, 151,
158 | 3eqtr4d 2787 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)[ℎ]( ≃ph‘𝐽))) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘[ℎ]( ≃ph‘𝐽)))) |
| 160 | 159 | 3expa 1119 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) ∧ ℎ ∈ ∪ 𝐵) → (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)[ℎ]( ≃ph‘𝐽))) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘[ℎ]( ≃ph‘𝐽)))) |
| 161 | 32, 45, 160 | ectocld 8824 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) ∧ 𝑧 ∈ (∪ 𝐵 / (
≃ph‘𝐽))) → (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧))) |
| 162 | 40, 161 | syldan 591 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧))) |
| 163 | 162 | ralrimiva 3146 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → ∀𝑧 ∈ 𝐵 (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧))) |
| 164 | 32, 37, 163 | ectocld 8824 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ 𝐵 / (
≃ph‘𝐽))) → ∀𝑧 ∈ 𝐵 (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧))) |
| 165 | 31, 164 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐵 (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧))) |
| 166 | 165 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧))) |
| 167 | 27, 166 | jca 511 |
. 2
⊢ (𝜑 → (𝐺:𝐵⟶(Base‘𝑄) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧)))) |
| 168 | 18, 122, 147, 124 | isghm 19233 |
. 2
⊢ (𝐺 ∈ (𝑃 GrpHom 𝑄) ↔ ((𝑃 ∈ Grp ∧ 𝑄 ∈ Grp) ∧ (𝐺:𝐵⟶(Base‘𝑄) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧))))) |
| 169 | 11, 17, 167, 168 | syl21anbrc 1345 |
1
⊢ (𝜑 → 𝐺 ∈ (𝑃 GrpHom 𝑄)) |