| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pi1co.j | . . 3
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) | 
| 2 |  | pi1co.a | . . 3
⊢ (𝜑 → 𝐴 ∈ 𝑋) | 
| 3 |  | pi1co.p | . . . 4
⊢ 𝑃 = (𝐽 π1 𝐴) | 
| 4 | 3 | pi1grp 25083 | . . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → 𝑃 ∈ Grp) | 
| 5 | 1, 2, 4 | syl2anc 584 | . 2
⊢ (𝜑 → 𝑃 ∈ Grp) | 
| 6 |  | pi1co.f | . . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) | 
| 7 |  | cntop2 23249 | . . . . 5
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) | 
| 8 | 6, 7 | syl 17 | . . . 4
⊢ (𝜑 → 𝐾 ∈ Top) | 
| 9 |  | toptopon2 22924 | . . . 4
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) | 
| 10 | 8, 9 | sylib 218 | . . 3
⊢ (𝜑 → 𝐾 ∈ (TopOn‘∪ 𝐾)) | 
| 11 |  | pi1co.b | . . . 4
⊢ (𝜑 → (𝐹‘𝐴) = 𝐵) | 
| 12 |  | cnf2 23257 | . . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶∪ 𝐾) | 
| 13 | 1, 10, 6, 12 | syl3anc 1373 | . . . . 5
⊢ (𝜑 → 𝐹:𝑋⟶∪ 𝐾) | 
| 14 | 13, 2 | ffvelcdmd 7105 | . . . 4
⊢ (𝜑 → (𝐹‘𝐴) ∈ ∪ 𝐾) | 
| 15 | 11, 14 | eqeltrrd 2842 | . . 3
⊢ (𝜑 → 𝐵 ∈ ∪ 𝐾) | 
| 16 |  | pi1co.q | . . . 4
⊢ 𝑄 = (𝐾 π1 𝐵) | 
| 17 | 16 | pi1grp 25083 | . . 3
⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝐵 ∈ ∪ 𝐾)
→ 𝑄 ∈
Grp) | 
| 18 | 10, 15, 17 | syl2anc 584 | . 2
⊢ (𝜑 → 𝑄 ∈ Grp) | 
| 19 |  | pi1co.v | . . . 4
⊢ 𝑉 = (Base‘𝑃) | 
| 20 |  | pi1co.g | . . . 4
⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝑉 ↦ 〈[𝑔](
≃ph‘𝐽), [(𝐹 ∘ 𝑔)]( ≃ph‘𝐾)〉) | 
| 21 | 3, 16, 19, 20, 1, 6, 2, 11 | pi1cof 25092 | . . 3
⊢ (𝜑 → 𝐺:𝑉⟶(Base‘𝑄)) | 
| 22 | 19 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 𝑉 = (Base‘𝑃)) | 
| 23 | 3, 1, 2, 22 | pi1bas2 25074 | . . . . . . 7
⊢ (𝜑 → 𝑉 = (∪ 𝑉 / (
≃ph‘𝐽))) | 
| 24 | 23 | eleq2d 2827 | . . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝑉 ↔ 𝑦 ∈ (∪ 𝑉 / (
≃ph‘𝐽)))) | 
| 25 | 24 | biimpa 476 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → 𝑦 ∈ (∪ 𝑉 / (
≃ph‘𝐽))) | 
| 26 |  | eqid 2737 | . . . . . 6
⊢ (∪ 𝑉
/ ( ≃ph‘𝐽)) = (∪ 𝑉 / (
≃ph‘𝐽)) | 
| 27 |  | fvoveq1 7454 | . . . . . . . 8
⊢ ([𝑓](
≃ph‘𝐽) = 𝑦 → (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = (𝐺‘(𝑦(+g‘𝑃)𝑧))) | 
| 28 |  | fveq2 6906 | . . . . . . . . 9
⊢ ([𝑓](
≃ph‘𝐽) = 𝑦 → (𝐺‘[𝑓]( ≃ph‘𝐽)) = (𝐺‘𝑦)) | 
| 29 | 28 | oveq1d 7446 | . . . . . . . 8
⊢ ([𝑓](
≃ph‘𝐽) = 𝑦 → ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧))) | 
| 30 | 27, 29 | eqeq12d 2753 | . . . . . . 7
⊢ ([𝑓](
≃ph‘𝐽) = 𝑦 → ((𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧)) ↔ (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧)))) | 
| 31 | 30 | ralbidv 3178 | . . . . . 6
⊢ ([𝑓](
≃ph‘𝐽) = 𝑦 → (∀𝑧 ∈ 𝑉 (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧)) ↔ ∀𝑧 ∈ 𝑉 (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧)))) | 
| 32 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ ([ℎ](
≃ph‘𝐽) = 𝑧 → ([𝑓]( ≃ph‘𝐽)(+g‘𝑃)[ℎ]( ≃ph‘𝐽)) = ([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) | 
| 33 | 32 | fveq2d 6910 | . . . . . . . . . 10
⊢ ([ℎ](
≃ph‘𝐽) = 𝑧 → (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)[ℎ]( ≃ph‘𝐽))) = (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧))) | 
| 34 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ ([ℎ](
≃ph‘𝐽) = 𝑧 → (𝐺‘[ℎ]( ≃ph‘𝐽)) = (𝐺‘𝑧)) | 
| 35 | 34 | oveq2d 7447 | . . . . . . . . . 10
⊢ ([ℎ](
≃ph‘𝐽) = 𝑧 → ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘[ℎ]( ≃ph‘𝐽))) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧))) | 
| 36 | 33, 35 | eqeq12d 2753 | . . . . . . . . 9
⊢ ([ℎ](
≃ph‘𝐽) = 𝑧 → ((𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)[ℎ]( ≃ph‘𝐽))) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘[ℎ]( ≃ph‘𝐽))) ↔ (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧)))) | 
| 37 | 3, 1, 2, 22 | pi1eluni 25075 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑓 ∈ ∪ 𝑉 ↔ (𝑓 ∈ (II Cn 𝐽) ∧ (𝑓‘0) = 𝐴 ∧ (𝑓‘1) = 𝐴))) | 
| 38 | 37 | biimpa 476 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (𝑓 ∈ (II Cn 𝐽) ∧ (𝑓‘0) = 𝐴 ∧ (𝑓‘1) = 𝐴)) | 
| 39 | 38 | simp1d 1143 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → 𝑓 ∈ (II Cn 𝐽)) | 
| 40 | 39 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → 𝑓 ∈ (II Cn 𝐽)) | 
| 41 | 1 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → 𝐽 ∈ (TopOn‘𝑋)) | 
| 42 | 2 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → 𝐴 ∈ 𝑋) | 
| 43 | 19 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → 𝑉 = (Base‘𝑃)) | 
| 44 | 3, 41, 42, 43 | pi1eluni 25075 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (ℎ ∈ ∪ 𝑉 ↔ (ℎ ∈ (II Cn 𝐽) ∧ (ℎ‘0) = 𝐴 ∧ (ℎ‘1) = 𝐴))) | 
| 45 | 44 | biimpa 476 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (ℎ ∈ (II Cn 𝐽) ∧ (ℎ‘0) = 𝐴 ∧ (ℎ‘1) = 𝐴)) | 
| 46 | 45 | simp1d 1143 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ℎ ∈ (II Cn 𝐽)) | 
| 47 | 38 | simp3d 1145 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (𝑓‘1) = 𝐴) | 
| 48 | 47 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝑓‘1) = 𝐴) | 
| 49 | 45 | simp2d 1144 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (ℎ‘0) = 𝐴) | 
| 50 | 48, 49 | eqtr4d 2780 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝑓‘1) = (ℎ‘0)) | 
| 51 | 6 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → 𝐹 ∈ (𝐽 Cn 𝐾)) | 
| 52 | 40, 46, 50, 51 | copco 25051 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐹 ∘ (𝑓(*𝑝‘𝐽)ℎ)) = ((𝐹 ∘ 𝑓)(*𝑝‘𝐾)(𝐹 ∘ ℎ))) | 
| 53 | 52 | eceq1d 8785 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → [(𝐹 ∘ (𝑓(*𝑝‘𝐽)ℎ))]( ≃ph‘𝐾) = [((𝐹 ∘ 𝑓)(*𝑝‘𝐾)(𝐹 ∘ ℎ))]( ≃ph‘𝐾)) | 
| 54 | 40, 46, 50 | pcocn 25050 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝑓(*𝑝‘𝐽)ℎ) ∈ (II Cn 𝐽)) | 
| 55 | 40, 46 | pco0 25047 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝑓(*𝑝‘𝐽)ℎ)‘0) = (𝑓‘0)) | 
| 56 | 38 | simp2d 1144 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (𝑓‘0) = 𝐴) | 
| 57 | 56 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝑓‘0) = 𝐴) | 
| 58 | 55, 57 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝑓(*𝑝‘𝐽)ℎ)‘0) = 𝐴) | 
| 59 | 40, 46 | pco1 25048 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝑓(*𝑝‘𝐽)ℎ)‘1) = (ℎ‘1)) | 
| 60 | 45 | simp3d 1145 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (ℎ‘1) = 𝐴) | 
| 61 | 59, 60 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝑓(*𝑝‘𝐽)ℎ)‘1) = 𝐴) | 
| 62 | 1 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → 𝐽 ∈ (TopOn‘𝑋)) | 
| 63 | 2 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → 𝐴 ∈ 𝑋) | 
| 64 | 19 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → 𝑉 = (Base‘𝑃)) | 
| 65 | 3, 62, 63, 64 | pi1eluni 25075 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝑓(*𝑝‘𝐽)ℎ) ∈ ∪ 𝑉 ↔ ((𝑓(*𝑝‘𝐽)ℎ) ∈ (II Cn 𝐽) ∧ ((𝑓(*𝑝‘𝐽)ℎ)‘0) = 𝐴 ∧ ((𝑓(*𝑝‘𝐽)ℎ)‘1) = 𝐴))) | 
| 66 | 54, 58, 61, 65 | mpbir3and 1343 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝑓(*𝑝‘𝐽)ℎ) ∈ ∪ 𝑉) | 
| 67 | 3, 16, 19, 20, 1, 6, 2, 11 | pi1coval 25093 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓(*𝑝‘𝐽)ℎ) ∈ ∪ 𝑉) → (𝐺‘[(𝑓(*𝑝‘𝐽)ℎ)]( ≃ph‘𝐽)) = [(𝐹 ∘ (𝑓(*𝑝‘𝐽)ℎ))]( ≃ph‘𝐾)) | 
| 68 | 67 | adantlr 715 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ (𝑓(*𝑝‘𝐽)ℎ) ∈ ∪ 𝑉) → (𝐺‘[(𝑓(*𝑝‘𝐽)ℎ)]( ≃ph‘𝐽)) = [(𝐹 ∘ (𝑓(*𝑝‘𝐽)ℎ))]( ≃ph‘𝐾)) | 
| 69 | 66, 68 | syldan 591 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐺‘[(𝑓(*𝑝‘𝐽)ℎ)]( ≃ph‘𝐽)) = [(𝐹 ∘ (𝑓(*𝑝‘𝐽)ℎ))]( ≃ph‘𝐾)) | 
| 70 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(Base‘𝑄) =
(Base‘𝑄) | 
| 71 | 10 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → 𝐾 ∈ (TopOn‘∪ 𝐾)) | 
| 72 | 15 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → 𝐵 ∈ ∪ 𝐾) | 
| 73 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(+g‘𝑄) = (+g‘𝑄) | 
| 74 | 6 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → 𝐹 ∈ (𝐽 Cn 𝐾)) | 
| 75 |  | cnco 23274 | . . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ 𝑓) ∈ (II Cn 𝐾)) | 
| 76 | 39, 74, 75 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (𝐹 ∘ 𝑓) ∈ (II Cn 𝐾)) | 
| 77 |  | iitopon 24905 | . . . . . . . . . . . . . . . . 17
⊢ II ∈
(TopOn‘(0[,]1)) | 
| 78 |  | cnf2 23257 | . . . . . . . . . . . . . . . . 17
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐽 ∈ (TopOn‘𝑋) ∧ 𝑓 ∈ (II Cn 𝐽)) → 𝑓:(0[,]1)⟶𝑋) | 
| 79 | 77, 41, 39, 78 | mp3an2i 1468 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → 𝑓:(0[,]1)⟶𝑋) | 
| 80 |  | 0elunit 13509 | . . . . . . . . . . . . . . . 16
⊢ 0 ∈
(0[,]1) | 
| 81 |  | fvco3 7008 | . . . . . . . . . . . . . . . 16
⊢ ((𝑓:(0[,]1)⟶𝑋 ∧ 0 ∈ (0[,]1)) →
((𝐹 ∘ 𝑓)‘0) = (𝐹‘(𝑓‘0))) | 
| 82 | 79, 80, 81 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑓)‘0) = (𝐹‘(𝑓‘0))) | 
| 83 | 56 | fveq2d 6910 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (𝐹‘(𝑓‘0)) = (𝐹‘𝐴)) | 
| 84 | 11 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (𝐹‘𝐴) = 𝐵) | 
| 85 | 82, 83, 84 | 3eqtrd 2781 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑓)‘0) = 𝐵) | 
| 86 |  | 1elunit 13510 | . . . . . . . . . . . . . . . 16
⊢ 1 ∈
(0[,]1) | 
| 87 |  | fvco3 7008 | . . . . . . . . . . . . . . . 16
⊢ ((𝑓:(0[,]1)⟶𝑋 ∧ 1 ∈ (0[,]1)) →
((𝐹 ∘ 𝑓)‘1) = (𝐹‘(𝑓‘1))) | 
| 88 | 79, 86, 87 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑓)‘1) = (𝐹‘(𝑓‘1))) | 
| 89 | 47 | fveq2d 6910 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (𝐹‘(𝑓‘1)) = (𝐹‘𝐴)) | 
| 90 | 88, 89, 84 | 3eqtrd 2781 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑓)‘1) = 𝐵) | 
| 91 | 10 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → 𝐾 ∈ (TopOn‘∪ 𝐾)) | 
| 92 | 15 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → 𝐵 ∈ ∪ 𝐾) | 
| 93 |  | eqidd 2738 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (Base‘𝑄) = (Base‘𝑄)) | 
| 94 | 16, 91, 92, 93 | pi1eluni 25075 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑓) ∈ ∪
(Base‘𝑄) ↔
((𝐹 ∘ 𝑓) ∈ (II Cn 𝐾) ∧ ((𝐹 ∘ 𝑓)‘0) = 𝐵 ∧ ((𝐹 ∘ 𝑓)‘1) = 𝐵))) | 
| 95 | 76, 85, 90, 94 | mpbir3and 1343 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (𝐹 ∘ 𝑓) ∈ ∪
(Base‘𝑄)) | 
| 96 | 95 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐹 ∘ 𝑓) ∈ ∪
(Base‘𝑄)) | 
| 97 |  | cnco 23274 | . . . . . . . . . . . . . 14
⊢ ((ℎ ∈ (II Cn 𝐽) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ ℎ) ∈ (II Cn 𝐾)) | 
| 98 | 46, 51, 97 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐹 ∘ ℎ) ∈ (II Cn 𝐾)) | 
| 99 |  | cnf2 23257 | . . . . . . . . . . . . . . . 16
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐽 ∈ (TopOn‘𝑋) ∧ ℎ ∈ (II Cn 𝐽)) → ℎ:(0[,]1)⟶𝑋) | 
| 100 | 77, 62, 46, 99 | mp3an2i 1468 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ℎ:(0[,]1)⟶𝑋) | 
| 101 |  | fvco3 7008 | . . . . . . . . . . . . . . 15
⊢ ((ℎ:(0[,]1)⟶𝑋 ∧ 0 ∈ (0[,]1)) → ((𝐹 ∘ ℎ)‘0) = (𝐹‘(ℎ‘0))) | 
| 102 | 100, 80, 101 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝐹 ∘ ℎ)‘0) = (𝐹‘(ℎ‘0))) | 
| 103 | 49 | fveq2d 6910 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐹‘(ℎ‘0)) = (𝐹‘𝐴)) | 
| 104 | 11 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐹‘𝐴) = 𝐵) | 
| 105 | 102, 103,
104 | 3eqtrd 2781 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝐹 ∘ ℎ)‘0) = 𝐵) | 
| 106 |  | fvco3 7008 | . . . . . . . . . . . . . . 15
⊢ ((ℎ:(0[,]1)⟶𝑋 ∧ 1 ∈ (0[,]1)) → ((𝐹 ∘ ℎ)‘1) = (𝐹‘(ℎ‘1))) | 
| 107 | 100, 86, 106 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝐹 ∘ ℎ)‘1) = (𝐹‘(ℎ‘1))) | 
| 108 | 60 | fveq2d 6910 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐹‘(ℎ‘1)) = (𝐹‘𝐴)) | 
| 109 | 107, 108,
104 | 3eqtrd 2781 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝐹 ∘ ℎ)‘1) = 𝐵) | 
| 110 |  | eqidd 2738 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (Base‘𝑄) = (Base‘𝑄)) | 
| 111 | 16, 10, 15, 110 | pi1eluni 25075 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐹 ∘ ℎ) ∈ ∪
(Base‘𝑄) ↔
((𝐹 ∘ ℎ) ∈ (II Cn 𝐾) ∧ ((𝐹 ∘ ℎ)‘0) = 𝐵 ∧ ((𝐹 ∘ ℎ)‘1) = 𝐵))) | 
| 112 | 111 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝐹 ∘ ℎ) ∈ ∪
(Base‘𝑄) ↔
((𝐹 ∘ ℎ) ∈ (II Cn 𝐾) ∧ ((𝐹 ∘ ℎ)‘0) = 𝐵 ∧ ((𝐹 ∘ ℎ)‘1) = 𝐵))) | 
| 113 | 98, 105, 109, 112 | mpbir3and 1343 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐹 ∘ ℎ) ∈ ∪
(Base‘𝑄)) | 
| 114 | 16, 70, 71, 72, 73, 96, 113 | pi1addval 25081 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ([(𝐹 ∘ 𝑓)]( ≃ph‘𝐾)(+g‘𝑄)[(𝐹 ∘ ℎ)]( ≃ph‘𝐾)) = [((𝐹 ∘ 𝑓)(*𝑝‘𝐾)(𝐹 ∘ ℎ))]( ≃ph‘𝐾)) | 
| 115 | 53, 69, 114 | 3eqtr4d 2787 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐺‘[(𝑓(*𝑝‘𝐽)ℎ)]( ≃ph‘𝐽)) = ([(𝐹 ∘ 𝑓)]( ≃ph‘𝐾)(+g‘𝑄)[(𝐹 ∘ ℎ)]( ≃ph‘𝐾))) | 
| 116 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(+g‘𝑃) = (+g‘𝑃) | 
| 117 |  | simplr 769 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → 𝑓 ∈ ∪ 𝑉) | 
| 118 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ℎ ∈ ∪ 𝑉) | 
| 119 | 3, 19, 62, 63, 116, 117, 118 | pi1addval 25081 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ([𝑓]( ≃ph‘𝐽)(+g‘𝑃)[ℎ]( ≃ph‘𝐽)) = [(𝑓(*𝑝‘𝐽)ℎ)]( ≃ph‘𝐽)) | 
| 120 | 119 | fveq2d 6910 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)[ℎ]( ≃ph‘𝐽))) = (𝐺‘[(𝑓(*𝑝‘𝐽)ℎ)]( ≃ph‘𝐽))) | 
| 121 | 3, 16, 19, 20, 1, 6, 2, 11 | pi1coval 25093 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → (𝐺‘[𝑓]( ≃ph‘𝐽)) = [(𝐹 ∘ 𝑓)]( ≃ph‘𝐾)) | 
| 122 | 121 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐺‘[𝑓]( ≃ph‘𝐽)) = [(𝐹 ∘ 𝑓)]( ≃ph‘𝐾)) | 
| 123 | 3, 16, 19, 20, 1, 6, 2, 11 | pi1coval 25093 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ℎ ∈ ∪ 𝑉) → (𝐺‘[ℎ]( ≃ph‘𝐽)) = [(𝐹 ∘ ℎ)]( ≃ph‘𝐾)) | 
| 124 | 123 | adantlr 715 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐺‘[ℎ]( ≃ph‘𝐽)) = [(𝐹 ∘ ℎ)]( ≃ph‘𝐾)) | 
| 125 | 122, 124 | oveq12d 7449 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘[ℎ]( ≃ph‘𝐽))) = ([(𝐹 ∘ 𝑓)]( ≃ph‘𝐾)(+g‘𝑄)[(𝐹 ∘ ℎ)]( ≃ph‘𝐾))) | 
| 126 | 115, 120,
125 | 3eqtr4d 2787 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ ℎ ∈ ∪ 𝑉) → (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)[ℎ]( ≃ph‘𝐽))) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘[ℎ]( ≃ph‘𝐽)))) | 
| 127 | 26, 36, 126 | ectocld 8824 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) ∧ 𝑧 ∈ (∪ 𝑉 / (
≃ph‘𝐽))) → (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧))) | 
| 128 | 127 | ralrimiva 3146 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → ∀𝑧 ∈ (∪ 𝑉
/ ( ≃ph‘𝐽))(𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧))) | 
| 129 | 23 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → 𝑉 = (∪ 𝑉 / (
≃ph‘𝐽))) | 
| 130 | 128, 129 | raleqtrrdv 3330 | . . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝑉) → ∀𝑧 ∈ 𝑉 (𝐺‘([𝑓]( ≃ph‘𝐽)(+g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃ph‘𝐽))(+g‘𝑄)(𝐺‘𝑧))) | 
| 131 | 26, 31, 130 | ectocld 8824 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ 𝑉 / (
≃ph‘𝐽))) → ∀𝑧 ∈ 𝑉 (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧))) | 
| 132 | 25, 131 | syldan 591 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → ∀𝑧 ∈ 𝑉 (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧))) | 
| 133 | 132 | ralrimiva 3146 | . . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧))) | 
| 134 | 21, 133 | jca 511 | . 2
⊢ (𝜑 → (𝐺:𝑉⟶(Base‘𝑄) ∧ ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧)))) | 
| 135 | 19, 70, 116, 73 | isghm 19233 | . 2
⊢ (𝐺 ∈ (𝑃 GrpHom 𝑄) ↔ ((𝑃 ∈ Grp ∧ 𝑄 ∈ Grp) ∧ (𝐺:𝑉⟶(Base‘𝑄) ∧ ∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝐺‘(𝑦(+g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+g‘𝑄)(𝐺‘𝑧))))) | 
| 136 | 5, 18, 134, 135 | syl21anbrc 1345 | 1
⊢ (𝜑 → 𝐺 ∈ (𝑃 GrpHom 𝑄)) |