Metamath Proof Explorer

Theorem pi1coghm

Description: The mapping G between fundamental groups is a group homomorphism. (Contributed by Mario Carneiro, 10-Aug-2015) (Revised by Mario Carneiro, 23-Dec-2016)

Ref Expression
Hypotheses pi1co.p ⊢ 𝑃 = ( 𝐽 π1 𝐴 )
pi1co.q ⊢ 𝑄 = ( 𝐾 π1 𝐵 )
pi1co.v ⊢ 𝑉 = ( Base ‘ 𝑃 )
pi1co.g ⊢ 𝐺 = ran ( 𝑔 ∈ ∪ 𝑉 ↦ ⟨ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ∘ 𝑔 ) ] ( ≃ph ‘ 𝐾 ) ⟩ )
pi1co.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
pi1co.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
pi1co.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
pi1co.b ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 𝐵 )
Assertion pi1coghm ( 𝜑 → 𝐺 ∈ ( 𝑃 GrpHom 𝑄 ) )

Proof

Step Hyp Ref Expression
1 pi1co.p ⊢ 𝑃 = ( 𝐽 π1 𝐴 )
2 pi1co.q ⊢ 𝑄 = ( 𝐾 π1 𝐵 )
3 pi1co.v ⊢ 𝑉 = ( Base ‘ 𝑃 )
4 pi1co.g ⊢ 𝐺 = ran ( 𝑔 ∈ ∪ 𝑉 ↦ ⟨ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ∘ 𝑔 ) ] ( ≃ph ‘ 𝐾 ) ⟩ )
5 pi1co.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
6 pi1co.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
7 pi1co.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
8 pi1co.b ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 𝐵 )
9 1 pi1grp ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝑃 ∈ Grp )
10 5 7 9 syl2anc ⊢ ( 𝜑 → 𝑃 ∈ Grp )
11 cntop2 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
12 6 11 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
13 toptopon2 ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
14 12 13 sylib ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
15 cnf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 : 𝑋 ⟶ ∪ 𝐾 )
16 5 14 6 15 syl3anc ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ∪ 𝐾 )
17 16 7 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ∪ 𝐾 )
18 8 17 eqeltrrd ⊢ ( 𝜑 → 𝐵 ∈ ∪ 𝐾 )
19 2 pi1grp ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ 𝐵 ∈ ∪ 𝐾 ) → 𝑄 ∈ Grp )
20 14 18 19 syl2anc ⊢ ( 𝜑 → 𝑄 ∈ Grp )
21 1 2 3 4 5 6 7 8 pi1cof ⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ ( Base ‘ 𝑄 ) )
22 3 a1i ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑃 ) )
23 1 5 7 22 pi1bas2 ⊢ ( 𝜑 → 𝑉 = ( ∪ 𝑉 / ( ≃ph ‘ 𝐽 ) ) )
24 23 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑉 ↔ 𝑦 ∈ ( ∪ 𝑉 / ( ≃ph ‘ 𝐽 ) ) ) )
25 24 biimpa ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → 𝑦 ∈ ( ∪ 𝑉 / ( ≃ph ‘ 𝐽 ) ) )
26 eqid ⊢ ( ∪ 𝑉 / ( ≃ph ‘ 𝐽 ) ) = ( ∪ 𝑉 / ( ≃ph ‘ 𝐽 ) )
27 fvoveq1 ⊢ ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) = 𝑦 → ( 𝐺 ‘ ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ( +g ‘ 𝑃 ) 𝑧 ) ) = ( 𝐺 ‘ ( 𝑦 ( +g ‘ 𝑃 ) 𝑧 ) ) )
28 fveq2 ⊢ ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) = 𝑦 → ( 𝐺 ‘ [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) = ( 𝐺 ‘ 𝑦 ) )
29 28 oveq1d ⊢ ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) = 𝑦 → ( ( 𝐺 ‘ [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ 𝑧 ) ) = ( ( 𝐺 ‘ 𝑦 ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ 𝑧 ) ) )
30 27 29 eqeq12d ⊢ ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) = 𝑦 → ( ( 𝐺 ‘ ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ( +g ‘ 𝑃 ) 𝑧 ) ) = ( ( 𝐺 ‘ [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ 𝑧 ) ) ↔ ( 𝐺 ‘ ( 𝑦 ( +g ‘ 𝑃 ) 𝑧 ) ) = ( ( 𝐺 ‘ 𝑦 ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ 𝑧 ) ) ) )
31 30 ralbidv ⊢ ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) = 𝑦 → ( ∀ 𝑧 ∈ 𝑉 ( 𝐺 ‘ ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ( +g ‘ 𝑃 ) 𝑧 ) ) = ( ( 𝐺 ‘ [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝑉 ( 𝐺 ‘ ( 𝑦 ( +g ‘ 𝑃 ) 𝑧 ) ) = ( ( 𝐺 ‘ 𝑦 ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ 𝑧 ) ) ) )
32 oveq2 ⊢ ( [ ℎ ] ( ≃ph ‘ 𝐽 ) = 𝑧 → ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ( +g ‘ 𝑃 ) [ ℎ ] ( ≃ph ‘ 𝐽 ) ) = ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ( +g ‘ 𝑃 ) 𝑧 ) )
33 32 fveq2d ⊢ ( [ ℎ ] ( ≃ph ‘ 𝐽 ) = 𝑧 → ( 𝐺 ‘ ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ( +g ‘ 𝑃 ) [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) = ( 𝐺 ‘ ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ( +g ‘ 𝑃 ) 𝑧 ) ) )
34 fveq2 ⊢ ( [ ℎ ] ( ≃ph ‘ 𝐽 ) = 𝑧 → ( 𝐺 ‘ [ ℎ ] ( ≃ph ‘ 𝐽 ) ) = ( 𝐺 ‘ 𝑧 ) )
35 34 oveq2d ⊢ ( [ ℎ ] ( ≃ph ‘ 𝐽 ) = 𝑧 → ( ( 𝐺 ‘ [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) = ( ( 𝐺 ‘ [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ 𝑧 ) ) )
36 33 35 eqeq12d ⊢ ( [ ℎ ] ( ≃ph ‘ 𝐽 ) = 𝑧 → ( ( 𝐺 ‘ ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ( +g ‘ 𝑃 ) [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) = ( ( 𝐺 ‘ [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) ↔ ( 𝐺 ‘ ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ( +g ‘ 𝑃 ) 𝑧 ) ) = ( ( 𝐺 ‘ [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ 𝑧 ) ) ) )
37 1 5 7 22 pi1eluni ⊢ ( 𝜑 → ( 𝑓 ∈ ∪ 𝑉 ↔ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐴 ) ) )
38 37 biimpa ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐴 ) )
39 38 simp1d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → 𝑓 ∈ ( II Cn 𝐽 ) )
40 39 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → 𝑓 ∈ ( II Cn 𝐽 ) )
41 5 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
42 7 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → 𝐴 ∈ 𝑋 )
43 3 a1i ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → 𝑉 = ( Base ‘ 𝑃 ) )
44 1 41 42 43 pi1eluni ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → ( ℎ ∈ ∪ 𝑉 ↔ ( ℎ ∈ ( II Cn 𝐽 ) ∧ ( ℎ ‘ 0 ) = 𝐴 ∧ ( ℎ ‘ 1 ) = 𝐴 ) ) )
45 44 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( ℎ ∈ ( II Cn 𝐽 ) ∧ ( ℎ ‘ 0 ) = 𝐴 ∧ ( ℎ ‘ 1 ) = 𝐴 ) )
46 45 simp1d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ℎ ∈ ( II Cn 𝐽 ) )
47 38 simp3d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → ( 𝑓 ‘ 1 ) = 𝐴 )
48 47 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( 𝑓 ‘ 1 ) = 𝐴 )
49 45 simp2d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( ℎ ‘ 0 ) = 𝐴 )
50 48 49 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( 𝑓 ‘ 1 ) = ( ℎ ‘ 0 ) )
51 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
52 40 46 50 51 copco ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( 𝐹 ∘ ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ) = ( ( 𝐹 ∘ 𝑓 ) ( *𝑝 ‘ 𝐾 ) ( 𝐹 ∘ ℎ ) ) )
53 52 eceq1d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → [ ( 𝐹 ∘ ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ) ] ( ≃ph ‘ 𝐾 ) = [ ( ( 𝐹 ∘ 𝑓 ) ( *𝑝 ‘ 𝐾 ) ( 𝐹 ∘ ℎ ) ) ] ( ≃ph ‘ 𝐾 ) )
54 40 46 50 pcocn ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ∈ ( II Cn 𝐽 ) )
55 40 46 pco0 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ‘ 0 ) = ( 𝑓 ‘ 0 ) )
56 38 simp2d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → ( 𝑓 ‘ 0 ) = 𝐴 )
57 56 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( 𝑓 ‘ 0 ) = 𝐴 )
58 55 57 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ‘ 0 ) = 𝐴 )
59 40 46 pco1 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ‘ 1 ) = ( ℎ ‘ 1 ) )
60 45 simp3d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( ℎ ‘ 1 ) = 𝐴 )
61 59 60 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ‘ 1 ) = 𝐴 )
62 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
63 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → 𝐴 ∈ 𝑋 )
64 3 a1i ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → 𝑉 = ( Base ‘ 𝑃 ) )
65 1 62 63 64 pi1eluni ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ∈ ∪ 𝑉 ↔ ( ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ‘ 0 ) = 𝐴 ∧ ( ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ‘ 1 ) = 𝐴 ) ) )
66 54 58 61 65 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ∈ ∪ 𝑉 )
67 1 2 3 4 5 6 7 8 pi1coval ⊢ ( ( 𝜑 ∧ ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ∈ ∪ 𝑉 ) → ( 𝐺 ‘ [ ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ] ( ≃ph ‘ 𝐽 ) ) = [ ( 𝐹 ∘ ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ) ] ( ≃ph ‘ 𝐾 ) )
68 67 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ∈ ∪ 𝑉 ) → ( 𝐺 ‘ [ ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ] ( ≃ph ‘ 𝐽 ) ) = [ ( 𝐹 ∘ ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ) ] ( ≃ph ‘ 𝐾 ) )
69 66 68 syldan ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( 𝐺 ‘ [ ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ] ( ≃ph ‘ 𝐽 ) ) = [ ( 𝐹 ∘ ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ) ] ( ≃ph ‘ 𝐾 ) )
70 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
71 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
72 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → 𝐵 ∈ ∪ 𝐾 )
73 eqid ⊢ ( +g ‘ 𝑄 ) = ( +g ‘ 𝑄 )
74 6 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
75 cnco ⊢ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 ∘ 𝑓 ) ∈ ( II Cn 𝐾 ) )
76 39 74 75 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → ( 𝐹 ∘ 𝑓 ) ∈ ( II Cn 𝐾 ) )
77 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
78 cnf2 ⊢ ( ( II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑓 ∈ ( II Cn 𝐽 ) ) → 𝑓 : ( 0 [,] 1 ) ⟶ 𝑋 )
79 77 41 39 78 mp3an2i ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → 𝑓 : ( 0 [,] 1 ) ⟶ 𝑋 )
80 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
81 fvco3 ⊢ ( ( 𝑓 : ( 0 [,] 1 ) ⟶ 𝑋 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 0 ) = ( 𝐹 ‘ ( 𝑓 ‘ 0 ) ) )
82 79 80 81 sylancl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 0 ) = ( 𝐹 ‘ ( 𝑓 ‘ 0 ) ) )
83 56 fveq2d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → ( 𝐹 ‘ ( 𝑓 ‘ 0 ) ) = ( 𝐹 ‘ 𝐴 ) )
84 8 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → ( 𝐹 ‘ 𝐴 ) = 𝐵 )
85 82 83 84 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 0 ) = 𝐵 )
86 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
87 fvco3 ⊢ ( ( 𝑓 : ( 0 [,] 1 ) ⟶ 𝑋 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 1 ) = ( 𝐹 ‘ ( 𝑓 ‘ 1 ) ) )
88 79 86 87 sylancl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 1 ) = ( 𝐹 ‘ ( 𝑓 ‘ 1 ) ) )
89 47 fveq2d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → ( 𝐹 ‘ ( 𝑓 ‘ 1 ) ) = ( 𝐹 ‘ 𝐴 ) )
90 88 89 84 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 1 ) = 𝐵 )
91 14 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
92 18 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → 𝐵 ∈ ∪ 𝐾 )
93 eqidd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 ) )
94 2 91 92 93 pi1eluni ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → ( ( 𝐹 ∘ 𝑓 ) ∈ ∪ ( Base ‘ 𝑄 ) ↔ ( ( 𝐹 ∘ 𝑓 ) ∈ ( II Cn 𝐾 ) ∧ ( ( 𝐹 ∘ 𝑓 ) ‘ 0 ) = 𝐵 ∧ ( ( 𝐹 ∘ 𝑓 ) ‘ 1 ) = 𝐵 ) ) )
95 76 85 90 94 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → ( 𝐹 ∘ 𝑓 ) ∈ ∪ ( Base ‘ 𝑄 ) )
96 95 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( 𝐹 ∘ 𝑓 ) ∈ ∪ ( Base ‘ 𝑄 ) )
97 cnco ⊢ ( ( ℎ ∈ ( II Cn 𝐽 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 ∘ ℎ ) ∈ ( II Cn 𝐾 ) )
98 46 51 97 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( 𝐹 ∘ ℎ ) ∈ ( II Cn 𝐾 ) )
99 cnf2 ⊢ ( ( II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ℎ ∈ ( II Cn 𝐽 ) ) → ℎ : ( 0 [,] 1 ) ⟶ 𝑋 )
100 77 62 46 99 mp3an2i ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ℎ : ( 0 [,] 1 ) ⟶ 𝑋 )
101 fvco3 ⊢ ( ( ℎ : ( 0 [,] 1 ) ⟶ 𝑋 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ ℎ ) ‘ 0 ) = ( 𝐹 ‘ ( ℎ ‘ 0 ) ) )
102 100 80 101 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( ( 𝐹 ∘ ℎ ) ‘ 0 ) = ( 𝐹 ‘ ( ℎ ‘ 0 ) ) )
103 49 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( 𝐹 ‘ ( ℎ ‘ 0 ) ) = ( 𝐹 ‘ 𝐴 ) )
104 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( 𝐹 ‘ 𝐴 ) = 𝐵 )
105 102 103 104 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( ( 𝐹 ∘ ℎ ) ‘ 0 ) = 𝐵 )
106 fvco3 ⊢ ( ( ℎ : ( 0 [,] 1 ) ⟶ 𝑋 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ ℎ ) ‘ 1 ) = ( 𝐹 ‘ ( ℎ ‘ 1 ) ) )
107 100 86 106 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( ( 𝐹 ∘ ℎ ) ‘ 1 ) = ( 𝐹 ‘ ( ℎ ‘ 1 ) ) )
108 60 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( 𝐹 ‘ ( ℎ ‘ 1 ) ) = ( 𝐹 ‘ 𝐴 ) )
109 107 108 104 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( ( 𝐹 ∘ ℎ ) ‘ 1 ) = 𝐵 )
110 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 ) )
111 2 14 18 110 pi1eluni ⊢ ( 𝜑 → ( ( 𝐹 ∘ ℎ ) ∈ ∪ ( Base ‘ 𝑄 ) ↔ ( ( 𝐹 ∘ ℎ ) ∈ ( II Cn 𝐾 ) ∧ ( ( 𝐹 ∘ ℎ ) ‘ 0 ) = 𝐵 ∧ ( ( 𝐹 ∘ ℎ ) ‘ 1 ) = 𝐵 ) ) )
112 111 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( ( 𝐹 ∘ ℎ ) ∈ ∪ ( Base ‘ 𝑄 ) ↔ ( ( 𝐹 ∘ ℎ ) ∈ ( II Cn 𝐾 ) ∧ ( ( 𝐹 ∘ ℎ ) ‘ 0 ) = 𝐵 ∧ ( ( 𝐹 ∘ ℎ ) ‘ 1 ) = 𝐵 ) ) )
113 98 105 109 112 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( 𝐹 ∘ ℎ ) ∈ ∪ ( Base ‘ 𝑄 ) )
114 2 70 71 72 73 96 113 pi1addval ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( [ ( 𝐹 ∘ 𝑓 ) ] ( ≃ph ‘ 𝐾 ) ( +g ‘ 𝑄 ) [ ( 𝐹 ∘ ℎ ) ] ( ≃ph ‘ 𝐾 ) ) = [ ( ( 𝐹 ∘ 𝑓 ) ( *𝑝 ‘ 𝐾 ) ( 𝐹 ∘ ℎ ) ) ] ( ≃ph ‘ 𝐾 ) )
115 53 69 114 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( 𝐺 ‘ [ ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ] ( ≃ph ‘ 𝐽 ) ) = ( [ ( 𝐹 ∘ 𝑓 ) ] ( ≃ph ‘ 𝐾 ) ( +g ‘ 𝑄 ) [ ( 𝐹 ∘ ℎ ) ] ( ≃ph ‘ 𝐾 ) ) )
116 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
117 simplr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → 𝑓 ∈ ∪ 𝑉 )
118 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ℎ ∈ ∪ 𝑉 )
119 1 3 62 63 116 117 118 pi1addval ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ( +g ‘ 𝑃 ) [ ℎ ] ( ≃ph ‘ 𝐽 ) ) = [ ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ] ( ≃ph ‘ 𝐽 ) )
120 119 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( 𝐺 ‘ ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ( +g ‘ 𝑃 ) [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) = ( 𝐺 ‘ [ ( 𝑓 ( *𝑝 ‘ 𝐽 ) ℎ ) ] ( ≃ph ‘ 𝐽 ) ) )
121 1 2 3 4 5 6 7 8 pi1coval ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → ( 𝐺 ‘ [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) = [ ( 𝐹 ∘ 𝑓 ) ] ( ≃ph ‘ 𝐾 ) )
122 121 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( 𝐺 ‘ [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) = [ ( 𝐹 ∘ 𝑓 ) ] ( ≃ph ‘ 𝐾 ) )
123 1 2 3 4 5 6 7 8 pi1coval ⊢ ( ( 𝜑 ∧ ℎ ∈ ∪ 𝑉 ) → ( 𝐺 ‘ [ ℎ ] ( ≃ph ‘ 𝐽 ) ) = [ ( 𝐹 ∘ ℎ ) ] ( ≃ph ‘ 𝐾 ) )
124 123 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( 𝐺 ‘ [ ℎ ] ( ≃ph ‘ 𝐽 ) ) = [ ( 𝐹 ∘ ℎ ) ] ( ≃ph ‘ 𝐾 ) )
125 122 124 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( ( 𝐺 ‘ [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) = ( [ ( 𝐹 ∘ 𝑓 ) ] ( ≃ph ‘ 𝐾 ) ( +g ‘ 𝑄 ) [ ( 𝐹 ∘ ℎ ) ] ( ≃ph ‘ 𝐾 ) ) )
126 115 120 125 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ ℎ ∈ ∪ 𝑉 ) → ( 𝐺 ‘ ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ( +g ‘ 𝑃 ) [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) = ( ( 𝐺 ‘ [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ [ ℎ ] ( ≃ph ‘ 𝐽 ) ) ) )
127 26 36 126 ectocld ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) ∧ 𝑧 ∈ ( ∪ 𝑉 / ( ≃ph ‘ 𝐽 ) ) ) → ( 𝐺 ‘ ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ( +g ‘ 𝑃 ) 𝑧 ) ) = ( ( 𝐺 ‘ [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ 𝑧 ) ) )
128 127 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → ∀ 𝑧 ∈ ( ∪ 𝑉 / ( ≃ph ‘ 𝐽 ) ) ( 𝐺 ‘ ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ( +g ‘ 𝑃 ) 𝑧 ) ) = ( ( 𝐺 ‘ [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ 𝑧 ) ) )
129 23 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → 𝑉 = ( ∪ 𝑉 / ( ≃ph ‘ 𝐽 ) ) )
130 129 raleqdv ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → ( ∀ 𝑧 ∈ 𝑉 ( 𝐺 ‘ ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ( +g ‘ 𝑃 ) 𝑧 ) ) = ( ( 𝐺 ‘ [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ ( ∪ 𝑉 / ( ≃ph ‘ 𝐽 ) ) ( 𝐺 ‘ ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ( +g ‘ 𝑃 ) 𝑧 ) ) = ( ( 𝐺 ‘ [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ 𝑧 ) ) ) )
131 128 130 mpbird ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∪ 𝑉 ) → ∀ 𝑧 ∈ 𝑉 ( 𝐺 ‘ ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ( +g ‘ 𝑃 ) 𝑧 ) ) = ( ( 𝐺 ‘ [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ 𝑧 ) ) )
132 26 31 131 ectocld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ∪ 𝑉 / ( ≃ph ‘ 𝐽 ) ) ) → ∀ 𝑧 ∈ 𝑉 ( 𝐺 ‘ ( 𝑦 ( +g ‘ 𝑃 ) 𝑧 ) ) = ( ( 𝐺 ‘ 𝑦 ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ 𝑧 ) ) )
133 25 132 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ∀ 𝑧 ∈ 𝑉 ( 𝐺 ‘ ( 𝑦 ( +g ‘ 𝑃 ) 𝑧 ) ) = ( ( 𝐺 ‘ 𝑦 ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ 𝑧 ) ) )
134 133 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑉 ∀ 𝑧 ∈ 𝑉 ( 𝐺 ‘ ( 𝑦 ( +g ‘ 𝑃 ) 𝑧 ) ) = ( ( 𝐺 ‘ 𝑦 ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ 𝑧 ) ) )
135 21 134 jca ⊢ ( 𝜑 → ( 𝐺 : 𝑉 ⟶ ( Base ‘ 𝑄 ) ∧ ∀ 𝑦 ∈ 𝑉 ∀ 𝑧 ∈ 𝑉 ( 𝐺 ‘ ( 𝑦 ( +g ‘ 𝑃 ) 𝑧 ) ) = ( ( 𝐺 ‘ 𝑦 ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ 𝑧 ) ) ) )
136 3 70 116 73 isghm ⊢ ( 𝐺 ∈ ( 𝑃 GrpHom 𝑄 ) ↔ ( ( 𝑃 ∈ Grp ∧ 𝑄 ∈ Grp ) ∧ ( 𝐺 : 𝑉 ⟶ ( Base ‘ 𝑄 ) ∧ ∀ 𝑦 ∈ 𝑉 ∀ 𝑧 ∈ 𝑉 ( 𝐺 ‘ ( 𝑦 ( +g ‘ 𝑃 ) 𝑧 ) ) = ( ( 𝐺 ‘ 𝑦 ) ( +g ‘ 𝑄 ) ( 𝐺 ‘ 𝑧 ) ) ) ) )
137 10 20 135 136 syl21anbrc ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑃 GrpHom 𝑄 ) )