Step | Hyp | Ref
| Expression |
1 | | pi1co.j |
. . . 4
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
2 | | pi1co.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
3 | | pi1co.p |
. . . . 5
⊢ 𝑃 = (𝐽 π1 𝐴) |
4 | 3 | pi1grp 22658 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → 𝑃 ∈ Grp) |
5 | 1, 2, 4 | syl2anc 691 |
. . 3
⊢ (𝜑 → 𝑃 ∈ Grp) |
6 | | pi1co.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
7 | | cntop2 20855 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
8 | 6, 7 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ Top) |
9 | | eqid 2610 |
. . . . . 6
⊢ ∪ 𝐾 =
∪ 𝐾 |
10 | 9 | toptopon 20548 |
. . . . 5
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
11 | 8, 10 | sylib 207 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
12 | | pi1co.b |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐴) = 𝐵) |
13 | | cnf2 20863 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶∪ 𝐾) |
14 | 1, 11, 6, 13 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑋⟶∪ 𝐾) |
15 | 14, 2 | ffvelrnd 6268 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐴) ∈ ∪ 𝐾) |
16 | 12, 15 | eqeltrrd 2689 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ∪ 𝐾) |
17 | | pi1co.q |
. . . . 5
⊢ 𝑄 = (𝐾 π1 𝐵) |
18 | 17 | pi1grp 22658 |
. . . 4
⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝐵 ∈ ∪ 𝐾)
→ 𝑄 ∈
Grp) |
19 | 11, 16, 18 | syl2anc 691 |
. . 3
⊢ (𝜑 → 𝑄 ∈ Grp) |
20 | 5, 19 | jca 553 |
. 2
⊢ (𝜑 → (𝑃 ∈ Grp ∧ 𝑄 ∈ Grp)) |
21 | | pi1co.v |
. . . 4
⊢ 𝑉 = (Base‘𝑃) |
22 | | pi1co.g |
. . . 4
⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝑉 ↦ 〈[𝑔](
≃ph‘𝐽), [(𝐹 ∘ 𝑔)]( ≃ph‘𝐾)〉) |
23 | 3, 17, 21, 22, 1, 6, 2, 12 | pi1cof 22667 |
. . 3
⊢ (𝜑 → 𝐺:𝑉⟶(Base‘𝑄)) |
24 | 21 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝑉 = (Base‘𝑃)) |
25 | 3, 1, 2, 24 | pi1bas2 22649 |
. . . . . . 7
⊢ (𝜑 → 𝑉 = (∪ 𝑉 / (
≃ph‘𝐽))) |
26 | 25 | eleq2d 2673 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝑉 ↔ 𝑦 ∈ (∪ 𝑉 / (
≃ph‘𝐽)))) |
27 | 26 | biimpa 500 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → 𝑦 ∈ (∪ 𝑉 / (
≃ph‘𝐽))) |
28 | | eqid 2610 |
. . . . . 6
⊢ (∪ 𝑉
/ ( ≃ph‘𝐽)) = (∪ 𝑉 / (
≃ph‘𝐽)) |
29 | | oveq1 6556 |
. . . . . . . . 9
⊢ ([𝑓](
≃ph‘𝐽) = 𝑦 → ([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧) = (𝑦(+g‘𝑃)𝑧)) |
30 | 29 | fveq2d 6107 |
. . . . . . . 8
⊢ ([𝑓](
≃ph‘𝐽) = 𝑦 → (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = (𝐺‘(𝑦(+g‘𝑃)𝑧))) |
31 | | fveq2 6103 |
. . . . . . . . 9
⊢ ([𝑓](
≃ph‘𝐽) = 𝑦 → (𝐺‘[𝑓]( ≃ph‘𝐽)) = (𝐺‘𝑦)) |
32 | 31 | oveq1d 6564 |
. . . . . . . 8
⊢ ([𝑓](
≃ph‘𝐽) = 𝑦 → ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧))) |
33 | 30, 32 | eqeq12d 2625 |
. . . . . . 7
⊢ ([𝑓](
≃ph‘𝐽) = 𝑦 → ((𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧)) ↔ (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧)))) |
34 | 33 | ralbidv 2969 |
. . . . . 6
⊢ ([𝑓](
≃ph‘𝐽) = 𝑦 → (∀𝑧 ∈ 𝑉 (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧)) ↔ ∀𝑧 ∈ 𝑉 (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧)))) |
35 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ ([ℎ](
≃ph‘𝐽) = 𝑧 → ([𝑓]( ≃ph‘𝐽)(+g‘𝑃)[ℎ]( ≃ph‘𝐽)) = ([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) |
36 | 35 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ([ℎ](
≃ph‘𝐽) = 𝑧 → (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)[ℎ]( ≃ph‘𝐽))) = (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧))) |
37 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ ([ℎ](
≃ph‘𝐽) = 𝑧 → (𝐺‘[ℎ]( ≃ph‘𝐽)) = (𝐺‘𝑧)) |
38 | 37 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ([ℎ](
≃ph‘𝐽) = 𝑧 → ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘[ℎ]( ≃ph‘𝐽))) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧))) |
39 | 36, 38 | eqeq12d 2625 |
. . . . . . . . 9
⊢ ([ℎ](
≃ph‘𝐽) = 𝑧 → ((𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)[ℎ]( ≃ph‘𝐽))) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘[ℎ]( ≃ph‘𝐽))) ↔ (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧)))) |
40 | 3, 1, 2, 24 | pi1eluni 22650 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑓 ∈ ∪ 𝑉 ↔ (𝑓 ∈ (II Cn 𝐽) ∧ (𝑓‘0) = 𝐴 ∧ (𝑓‘1) = 𝐴))) |
41 | 40 | biimpa 500 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (𝑓 ∈ (II Cn 𝐽) ∧ (𝑓‘0) = 𝐴 ∧ (𝑓‘1) = 𝐴)) |
42 | 41 | simp1d 1066 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → 𝑓 ∈ (II Cn 𝐽)) |
43 | 42 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → 𝑓 ∈ (II Cn 𝐽)) |
44 | 1 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → 𝐽 ∈ (TopOn‘𝑋)) |
45 | 2 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → 𝐴 ∈ 𝑋) |
46 | 21 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → 𝑉 = (Base‘𝑃)) |
47 | 3, 44, 45, 46 | pi1eluni 22650 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (ℎ ∈ ∪ 𝑉 ↔ (ℎ ∈ (II Cn 𝐽) ∧ (ℎ‘0) = 𝐴 ∧ (ℎ‘1) = 𝐴))) |
48 | 47 | biimpa 500 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (ℎ ∈ (II Cn 𝐽) ∧ (ℎ‘0) = 𝐴 ∧ (ℎ‘1) = 𝐴)) |
49 | 48 | simp1d 1066 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ℎ ∈ (II Cn 𝐽)) |
50 | 41 | simp3d 1068 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (𝑓‘1) = 𝐴) |
51 | 50 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝑓‘1) = 𝐴) |
52 | 48 | simp2d 1067 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (ℎ‘0) = 𝐴) |
53 | 51, 52 | eqtr4d 2647 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝑓‘1) = (ℎ‘0)) |
54 | 6 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
55 | 43, 49, 53, 54 | copco 22626 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐹 ∘ (𝑓(*𝑝‘𝐽)ℎ)) = ((𝐹 ∘ 𝑓)(*𝑝‘𝐾)(𝐹 ∘ ℎ))) |
56 | 55 | eceq1d 7670 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → [(𝐹 ∘ (𝑓(*𝑝‘𝐽)ℎ))]( ≃ph‘𝐾) = [((𝐹 ∘ 𝑓)(*𝑝‘𝐾)(𝐹 ∘ ℎ))]( ≃ph‘𝐾)) |
57 | 43, 49, 53 | pcocn 22625 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝑓(*𝑝‘𝐽)ℎ) ∈ (II Cn 𝐽)) |
58 | 43, 49 | pco0 22622 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝑓(*𝑝‘𝐽)ℎ)‘0) = (𝑓‘0)) |
59 | 41 | simp2d 1067 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (𝑓‘0) = 𝐴) |
60 | 59 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝑓‘0) = 𝐴) |
61 | 58, 60 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝑓(*𝑝‘𝐽)ℎ)‘0) = 𝐴) |
62 | 43, 49 | pco1 22623 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝑓(*𝑝‘𝐽)ℎ)‘1) = (ℎ‘1)) |
63 | 48 | simp3d 1068 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (ℎ‘1) = 𝐴) |
64 | 62, 63 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝑓(*𝑝‘𝐽)ℎ)‘1) = 𝐴) |
65 | 1 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → 𝐽 ∈ (TopOn‘𝑋)) |
66 | 2 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → 𝐴 ∈ 𝑋) |
67 | 21 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → 𝑉 = (Base‘𝑃)) |
68 | 3, 65, 66, 67 | pi1eluni 22650 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝑓(*𝑝‘𝐽)ℎ) ∈ ∪ 𝑉 ↔ ((𝑓(*𝑝‘𝐽)ℎ) ∈ (II Cn 𝐽) ∧ ((𝑓(*𝑝‘𝐽)ℎ)‘0) = 𝐴 ∧ ((𝑓(*𝑝‘𝐽)ℎ)‘1) = 𝐴))) |
69 | 57, 61, 64, 68 | mpbir3and 1238 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝑓(*𝑝‘𝐽)ℎ) ∈ ∪ 𝑉) |
70 | 3, 17, 21, 22, 1, 6, 2, 12 | pi1coval 22668 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓(*𝑝‘𝐽)ℎ) ∈ ∪ 𝑉) → (𝐺‘[(𝑓(*𝑝‘𝐽)ℎ)]( ≃ph‘𝐽)) = [(𝐹 ∘ (𝑓(*𝑝‘𝐽)ℎ))]( ≃ph‘𝐾)) |
71 | 70 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ (𝑓(*𝑝‘𝐽)ℎ) ∈ ∪ 𝑉) → (𝐺‘[(𝑓(*𝑝‘𝐽)ℎ)]( ≃ph‘𝐽)) = [(𝐹 ∘ (𝑓(*𝑝‘𝐽)ℎ))]( ≃ph‘𝐾)) |
72 | 69, 71 | syldan 486 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐺‘[(𝑓(*𝑝‘𝐽)ℎ)]( ≃ph‘𝐽)) = [(𝐹 ∘ (𝑓(*𝑝‘𝐽)ℎ))]( ≃ph‘𝐾)) |
73 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Base‘𝑄) =
(Base‘𝑄) |
74 | 11 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
75 | 16 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → 𝐵 ∈ ∪ 𝐾) |
76 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(+g‘𝑄) = (+g‘𝑄) |
77 | 6 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
78 | | cnco 20880 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ 𝑓) ∈ (II Cn 𝐾)) |
79 | 42, 77, 78 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (𝐹 ∘ 𝑓) ∈ (II Cn 𝐾)) |
80 | | iitopon 22490 |
. . . . . . . . . . . . . . . . . 18
⊢ II ∈
(TopOn‘(0[,]1)) |
81 | 80 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → II ∈
(TopOn‘(0[,]1))) |
82 | | cnf2 20863 |
. . . . . . . . . . . . . . . . 17
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐽 ∈ (TopOn‘𝑋) ∧ 𝑓 ∈ (II Cn 𝐽)) → 𝑓:(0[,]1)⟶𝑋) |
83 | 81, 44, 42, 82 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → 𝑓:(0[,]1)⟶𝑋) |
84 | | 0elunit 12161 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
(0[,]1) |
85 | | fvco3 6185 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(0[,]1)⟶𝑋 ∧ 0 ∈ (0[,]1)) →
((𝐹 ∘ 𝑓)‘0) = (𝐹‘(𝑓‘0))) |
86 | 83, 84, 85 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑓)‘0) = (𝐹‘(𝑓‘0))) |
87 | 59 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (𝐹‘(𝑓‘0)) = (𝐹‘𝐴)) |
88 | 12 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (𝐹‘𝐴) = 𝐵) |
89 | 86, 87, 88 | 3eqtrd 2648 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑓)‘0) = 𝐵) |
90 | | 1elunit 12162 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
(0[,]1) |
91 | | fvco3 6185 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(0[,]1)⟶𝑋 ∧ 1 ∈ (0[,]1)) →
((𝐹 ∘ 𝑓)‘1) = (𝐹‘(𝑓‘1))) |
92 | 83, 90, 91 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑓)‘1) = (𝐹‘(𝑓‘1))) |
93 | 50 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (𝐹‘(𝑓‘1)) = (𝐹‘𝐴)) |
94 | 92, 93, 88 | 3eqtrd 2648 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑓)‘1) = 𝐵) |
95 | 11 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
96 | 16 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → 𝐵 ∈ ∪ 𝐾) |
97 | | eqidd 2611 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (Base‘𝑄) = (Base‘𝑄)) |
98 | 17, 95, 96, 97 | pi1eluni 22650 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑓) ∈ ∪
(Base‘𝑄) ↔
((𝐹 ∘ 𝑓) ∈ (II Cn 𝐾) ∧ ((𝐹 ∘ 𝑓)‘0) = 𝐵 ∧ ((𝐹 ∘ 𝑓)‘1) = 𝐵))) |
99 | 79, 89, 94, 98 | mpbir3and 1238 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (𝐹 ∘ 𝑓) ∈ ∪
(Base‘𝑄)) |
100 | 99 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐹 ∘ 𝑓) ∈ ∪
(Base‘𝑄)) |
101 | | cnco 20880 |
. . . . . . . . . . . . . 14
⊢ ((ℎ ∈ (II Cn 𝐽) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ ℎ) ∈ (II Cn 𝐾)) |
102 | 49, 54, 101 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐹 ∘ ℎ) ∈ (II Cn 𝐾)) |
103 | 80 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → II ∈
(TopOn‘(0[,]1))) |
104 | | cnf2 20863 |
. . . . . . . . . . . . . . . 16
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐽 ∈ (TopOn‘𝑋) ∧ ℎ ∈ (II Cn 𝐽)) → ℎ:(0[,]1)⟶𝑋) |
105 | 103, 65, 49, 104 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ℎ:(0[,]1)⟶𝑋) |
106 | | fvco3 6185 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ:(0[,]1)⟶𝑋 ∧ 0 ∈ (0[,]1)) → ((𝐹 ∘ ℎ)‘0) = (𝐹‘(ℎ‘0))) |
107 | 105, 84, 106 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝐹 ∘ ℎ)‘0) = (𝐹‘(ℎ‘0))) |
108 | 52 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐹‘(ℎ‘0)) = (𝐹‘𝐴)) |
109 | 12 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐹‘𝐴) = 𝐵) |
110 | 107, 108,
109 | 3eqtrd 2648 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝐹 ∘ ℎ)‘0) = 𝐵) |
111 | | fvco3 6185 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ:(0[,]1)⟶𝑋 ∧ 1 ∈ (0[,]1)) → ((𝐹 ∘ ℎ)‘1) = (𝐹‘(ℎ‘1))) |
112 | 105, 90, 111 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝐹 ∘ ℎ)‘1) = (𝐹‘(ℎ‘1))) |
113 | 63 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐹‘(ℎ‘1)) = (𝐹‘𝐴)) |
114 | 112, 113,
109 | 3eqtrd 2648 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝐹 ∘ ℎ)‘1) = 𝐵) |
115 | | eqidd 2611 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (Base‘𝑄) = (Base‘𝑄)) |
116 | 17, 11, 16, 115 | pi1eluni 22650 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐹 ∘ ℎ) ∈ ∪
(Base‘𝑄) ↔
((𝐹 ∘ ℎ) ∈ (II Cn 𝐾) ∧ ((𝐹 ∘ ℎ)‘0) = 𝐵 ∧ ((𝐹 ∘ ℎ)‘1) = 𝐵))) |
117 | 116 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝐹 ∘ ℎ) ∈ ∪
(Base‘𝑄) ↔
((𝐹 ∘ ℎ) ∈ (II Cn 𝐾) ∧ ((𝐹 ∘ ℎ)‘0) = 𝐵 ∧ ((𝐹 ∘ ℎ)‘1) = 𝐵))) |
118 | 102, 110,
114, 117 | mpbir3and 1238 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐹 ∘ ℎ) ∈ ∪
(Base‘𝑄)) |
119 | 17, 73, 74, 75, 76, 100, 118 | pi1addval 22656 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ([(𝐹 ∘ 𝑓)]( ≃ph‘𝐾)(+g‘𝑄)[(𝐹 ∘ ℎ)]( ≃ph‘𝐾)) = [((𝐹 ∘ 𝑓)(*𝑝‘𝐾)(𝐹 ∘ ℎ))]( ≃ph‘𝐾)) |
120 | 56, 72, 119 | 3eqtr4d 2654 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐺‘[(𝑓(*𝑝‘𝐽)ℎ)]( ≃ph‘𝐽)) = ([(𝐹 ∘ 𝑓)]( ≃ph‘𝐾)(+g‘𝑄)[(𝐹 ∘ ℎ)]( ≃ph‘𝐾))) |
121 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(+g‘𝑃) = (+g‘𝑃) |
122 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → 𝑓 ∈ ∪ 𝑉) |
123 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ℎ ∈ ∪ 𝑉) |
124 | 3, 21, 65, 66, 121, 122, 123 | pi1addval 22656 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ([𝑓]( ≃ph‘𝐽)(+g‘𝑃)[ℎ]( ≃ph‘𝐽)) = [(𝑓(*𝑝‘𝐽)ℎ)]( ≃ph‘𝐽)) |
125 | 124 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)[ℎ]( ≃ph‘𝐽))) = (𝐺‘[(𝑓(*𝑝‘𝐽)ℎ)]( ≃ph‘𝐽))) |
126 | 3, 17, 21, 22, 1, 6, 2, 12 | pi1coval 22668 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (𝐺‘[𝑓]( ≃ph‘𝐽)) = [(𝐹 ∘ 𝑓)]( ≃ph‘𝐾)) |
127 | 126 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐺‘[𝑓]( ≃ph‘𝐽)) = [(𝐹 ∘ 𝑓)]( ≃ph‘𝐾)) |
128 | 3, 17, 21, 22, 1, 6, 2, 12 | pi1coval 22668 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ℎ ∈ ∪ 𝑉) → (𝐺‘[ℎ]( ≃ph‘𝐽)) = [(𝐹 ∘ ℎ)]( ≃ph‘𝐾)) |
129 | 128 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐺‘[ℎ]( ≃ph‘𝐽)) = [(𝐹 ∘ ℎ)]( ≃ph‘𝐾)) |
130 | 127, 129 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘[ℎ]( ≃ph‘𝐽))) = ([(𝐹 ∘ 𝑓)]( ≃ph‘𝐾)(+g‘𝑄)[(𝐹 ∘ ℎ)]( ≃ph‘𝐾))) |
131 | 120, 125,
130 | 3eqtr4d 2654 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)[ℎ]( ≃ph‘𝐽))) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘[ℎ]( ≃ph‘𝐽)))) |
132 | 28, 39, 131 | ectocld 7701 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ 𝑧 ∈ (∪ 𝑉 / (
≃ph‘𝐽))) → (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧))) |
133 | 132 | ralrimiva 2949 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → ∀𝑧 ∈ (∪ 𝑉
/ ( ≃ph‘𝐽))(𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧))) |
134 | 25 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → 𝑉 = (∪ 𝑉 / (
≃ph‘𝐽))) |
135 | 134 | raleqdv 3121 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (∀𝑧 ∈ 𝑉 (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧)) ↔ ∀𝑧 ∈ (∪ 𝑉 / (
≃ph‘𝐽))(𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧)))) |
136 | 133, 135 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → ∀𝑧 ∈ 𝑉 (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧))) |
137 | 28, 34, 136 | ectocld 7701 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ 𝑉 / (
≃ph‘𝐽))) → ∀𝑧 ∈ 𝑉 (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧))) |
138 | 27, 137 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → ∀𝑧 ∈ 𝑉 (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧))) |
139 | 138 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧))) |
140 | 23, 139 | jca 553 |
. 2
⊢ (𝜑 → (𝐺:𝑉⟶(Base‘𝑄) ∧ ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧)))) |
141 | 21, 73, 121, 76 | isghm 17483 |
. 2
⊢ (𝐺 ∈ (𝑃 GrpHom 𝑄) ↔ ((𝑃 ∈ Grp ∧ 𝑄 ∈ Grp) ∧ (𝐺:𝑉⟶(Base‘𝑄) ∧ ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧))))) |
142 | 20, 140, 141 | sylanbrc 695 |
1
⊢ (𝜑 → 𝐺 ∈ (𝑃 GrpHom 𝑄)) |