Metamath Proof Explorer

Theorem pi1xfr

Description: Given a path F and its inverse I between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015)

Ref Expression
Hypotheses pi1xfr.p ⊢ 𝑃 = ( 𝐽 π1 ( 𝐹 ‘ 0 ) )
pi1xfr.q ⊢ 𝑄 = ( 𝐽 π1 ( 𝐹 ‘ 1 ) )
pi1xfr.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
pi1xfr.g ⊢ 𝐺 = ran ( 𝑔 ∈ ∪ 𝐵 ↦ ⟨ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ )
pi1xfr.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
pi1xfr.f ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
pi1xfr.i ⊢ 𝐼 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 1 − 𝑥 ) ) )
Assertion pi1xfr ( 𝜑 → 𝐺 ∈ ( 𝑃 GrpHom 𝑄 ) )

Proof

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