Metamath Proof Explorer

Theorem pi1xfrcnvlem

Description: Given a path F between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015) (Proof shortened by Mario Carneiro, 23-Dec-2016)

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 − 𝑥 ) ) )
pi1xfrcnv.h ⊢ 𝐻 = ran ( ℎ ∈ ∪ ( Base ‘ 𝑄 ) ↦ ⟨ [ ℎ ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ )
Assertion pi1xfrcnvlem ( 𝜑 → ◡ 𝐺 ⊆ 𝐻 )

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 pi1xfrcnv.h ⊢ 𝐻 = ran ( ℎ ∈ ∪ ( Base ‘ 𝑄 ) ↦ ⟨ [ ℎ ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ )
9 fvex ⊢ ( ≃ph ‘ 𝐽 ) ∈ V
10 ecexg ⊢ ( ( ≃ph ‘ 𝐽 ) ∈ V → [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ∈ V )
11 9 10 mp1i ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ∈ V )
12 ecexg ⊢ ( ( ≃ph ‘ 𝐽 ) ∈ V → [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) ∈ V )
13 9 12 mp1i ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) ∈ V )
14 4 11 13 fliftcnv ⊢ ( 𝜑 → ◡ 𝐺 = ran ( 𝑔 ∈ ∪ 𝐵 ↦ ⟨ [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) , [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ⟩ ) )
15 7 pcorevcl ⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → ( 𝐼 ∈ ( II Cn 𝐽 ) ∧ ( 𝐼 ‘ 0 ) = ( 𝐹 ‘ 1 ) ∧ ( 𝐼 ‘ 1 ) = ( 𝐹 ‘ 0 ) ) )
16 6 15 syl ⊢ ( 𝜑 → ( 𝐼 ∈ ( II Cn 𝐽 ) ∧ ( 𝐼 ‘ 0 ) = ( 𝐹 ‘ 1 ) ∧ ( 𝐼 ‘ 1 ) = ( 𝐹 ‘ 0 ) ) )
17 16 simp1d ⊢ ( 𝜑 → 𝐼 ∈ ( II Cn 𝐽 ) )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → 𝐼 ∈ ( II Cn 𝐽 ) )
19 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
20 cnf2 ⊢ ( ( II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( II Cn 𝐽 ) ) → 𝐹 : ( 0 [,] 1 ) ⟶ 𝑋 )
21 19 5 6 20 mp3an2i ⊢ ( 𝜑 → 𝐹 : ( 0 [,] 1 ) ⟶ 𝑋 )
22 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
23 ffvelcdm ⊢ ( ( 𝐹 : ( 0 [,] 1 ) ⟶ 𝑋 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ 0 ) ∈ 𝑋 )
24 21 22 23 sylancl ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) ∈ 𝑋 )
25 3 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑃 ) )
26 1 5 24 25 pi1eluni ⊢ ( 𝜑 → ( 𝑔 ∈ ∪ 𝐵 ↔ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( 𝑔 ‘ 0 ) = ( 𝐹 ‘ 0 ) ∧ ( 𝑔 ‘ 1 ) = ( 𝐹 ‘ 0 ) ) ) )
27 26 biimpa ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( 𝑔 ‘ 0 ) = ( 𝐹 ‘ 0 ) ∧ ( 𝑔 ‘ 1 ) = ( 𝐹 ‘ 0 ) ) )
28 27 simp1d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → 𝑔 ∈ ( II Cn 𝐽 ) )
29 6 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → 𝐹 ∈ ( II Cn 𝐽 ) )
30 27 simp3d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝑔 ‘ 1 ) = ( 𝐹 ‘ 0 ) )
31 28 29 30 pcocn ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ∈ ( II Cn 𝐽 ) )
32 16 simp3d ⊢ ( 𝜑 → ( 𝐼 ‘ 1 ) = ( 𝐹 ‘ 0 ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝐼 ‘ 1 ) = ( 𝐹 ‘ 0 ) )
34 27 simp2d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝑔 ‘ 0 ) = ( 𝐹 ‘ 0 ) )
35 33 34 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝐼 ‘ 1 ) = ( 𝑔 ‘ 0 ) )
36 28 29 pco0 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ‘ 0 ) = ( 𝑔 ‘ 0 ) )
37 35 36 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝐼 ‘ 1 ) = ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ‘ 0 ) )
38 18 31 37 pcocn ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ∈ ( II Cn 𝐽 ) )
39 18 31 pco0 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ‘ 0 ) = ( 𝐼 ‘ 0 ) )
40 16 simp2d ⊢ ( 𝜑 → ( 𝐼 ‘ 0 ) = ( 𝐹 ‘ 1 ) )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝐼 ‘ 0 ) = ( 𝐹 ‘ 1 ) )
42 39 41 eqtrd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ‘ 0 ) = ( 𝐹 ‘ 1 ) )
43 18 31 pco1 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ‘ 1 ) = ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ‘ 1 ) )
44 28 29 pco1 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ‘ 1 ) = ( 𝐹 ‘ 1 ) )
45 43 44 eqtrd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ‘ 1 ) = ( 𝐹 ‘ 1 ) )
46 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
47 ffvelcdm ⊢ ( ( 𝐹 : ( 0 [,] 1 ) ⟶ 𝑋 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ 1 ) ∈ 𝑋 )
48 21 46 47 sylancl ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) ∈ 𝑋 )
49 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 ) )
50 2 5 48 49 pi1eluni ⊢ ( 𝜑 → ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ∈ ∪ ( Base ‘ 𝑄 ) ↔ ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ∈ ( II Cn 𝐽 ) ∧ ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ‘ 0 ) = ( 𝐹 ‘ 1 ) ∧ ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ‘ 1 ) = ( 𝐹 ‘ 1 ) ) ) )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ∈ ∪ ( Base ‘ 𝑄 ) ↔ ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ∈ ( II Cn 𝐽 ) ∧ ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ‘ 0 ) = ( 𝐹 ‘ 1 ) ∧ ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ‘ 1 ) = ( 𝐹 ‘ 1 ) ) ) )
52 38 42 45 51 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ∈ ∪ ( Base ‘ 𝑄 ) )
53 eqidd ⊢ ( 𝜑 → ( 𝑔 ∈ ∪ 𝐵 ↦ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ) = ( 𝑔 ∈ ∪ 𝐵 ↦ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ) )
54 eqidd ⊢ ( 𝜑 → ( ℎ ∈ ∪ ( Base ‘ 𝑄 ) ↦ ⟨ [ ℎ ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ ) = ( ℎ ∈ ∪ ( Base ‘ 𝑄 ) ↦ ⟨ [ ℎ ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ ) )
55 eceq1 ⊢ ( ℎ = ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) → [ ℎ ] ( ≃ph ‘ 𝐽 ) = [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) )
56 oveq1 ⊢ ( ℎ = ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) → ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐼 ) = ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ( *𝑝 ‘ 𝐽 ) 𝐼 ) )
57 56 oveq2d ⊢ ( ℎ = ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) → ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) = ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) )
58 57 eceq1d ⊢ ( ℎ = ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) → [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) = [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) )
59 55 58 opeq12d ⊢ ( ℎ = ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) → ⟨ [ ℎ ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ = ⟨ [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ )
60 52 53 54 59 fmptco ⊢ ( 𝜑 → ( ( ℎ ∈ ∪ ( Base ‘ 𝑄 ) ↦ ⟨ [ ℎ ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ ) ∘ ( 𝑔 ∈ ∪ 𝐵 ↦ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ) ) = ( 𝑔 ∈ ∪ 𝐵 ↦ ⟨ [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ ) )
61 phtpcer ⊢ ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 )
62 61 a1i ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 ) )
63 18 28 pco0 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) 𝑔 ) ‘ 0 ) = ( 𝐼 ‘ 0 ) )
64 63 41 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝐹 ‘ 1 ) = ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) 𝑔 ) ‘ 0 ) )
65 62 29 erref ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → 𝐹 ( ≃ph ‘ 𝐽 ) 𝐹 )
66 62 18 erref ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → 𝐼 ( ≃ph ‘ 𝐽 ) 𝐼 )
67 eqid ⊢ ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) = ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } )
68 67 pcopt2 ⊢ ( ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( 𝑔 ‘ 1 ) = ( 𝐹 ‘ 0 ) ) → ( 𝑔 ( *𝑝 ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ) ( ≃ph ‘ 𝐽 ) 𝑔 )
69 28 30 68 syl2anc ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝑔 ( *𝑝 ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ) ( ≃ph ‘ 𝐽 ) 𝑔 )
70 41 eqcomd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝐹 ‘ 1 ) = ( 𝐼 ‘ 0 ) )
71 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 ) ) ) )
72 28 29 18 30 70 71 pcoass ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ( *𝑝 ‘ 𝐽 ) 𝐼 ) ( ≃ph ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) )
73 29 18 pco0 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐼 ) ‘ 0 ) = ( 𝐹 ‘ 0 ) )
74 30 73 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝑔 ‘ 1 ) = ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐼 ) ‘ 0 ) )
75 62 28 erref ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → 𝑔 ( ≃ph ‘ 𝐽 ) 𝑔 )
76 7 67 pcorev2 ⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐼 ) ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) )
77 29 76 syl ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐼 ) ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) )
78 74 75 77 pcohtpy ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝑔 ( *𝑝 ‘ 𝐽 ) ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ( ≃ph ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ) )
79 62 72 78 ertr2d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝑔 ( *𝑝 ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ) ( ≃ph ‘ 𝐽 ) ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ( *𝑝 ‘ 𝐽 ) 𝐼 ) )
80 62 69 79 ertr3d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → 𝑔 ( ≃ph ‘ 𝐽 ) ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ( *𝑝 ‘ 𝐽 ) 𝐼 ) )
81 35 66 80 pcohtpy ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝐼 ( *𝑝 ‘ 𝐽 ) 𝑔 ) ( ≃ph ‘ 𝐽 ) ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) )
82 44 41 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ‘ 1 ) = ( 𝐼 ‘ 0 ) )
83 18 31 18 37 82 71 pcoass ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ( *𝑝 ‘ 𝐽 ) 𝐼 ) ( ≃ph ‘ 𝐽 ) ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) )
84 62 81 83 ertr4d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝐼 ( *𝑝 ‘ 𝐽 ) 𝑔 ) ( ≃ph ‘ 𝐽 ) ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ( *𝑝 ‘ 𝐽 ) 𝐼 ) )
85 64 65 84 pcohtpy ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝐼 ( *𝑝 ‘ 𝐽 ) 𝑔 ) ) ( ≃ph ‘ 𝐽 ) ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) )
86 29 18 28 70 35 71 pcoass ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐼 ) ( *𝑝 ‘ 𝐽 ) 𝑔 ) ( ≃ph ‘ 𝐽 ) ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝐼 ( *𝑝 ‘ 𝐽 ) 𝑔 ) ) )
87 29 18 pco1 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐼 ) ‘ 1 ) = ( 𝐼 ‘ 1 ) )
88 87 35 eqtrd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐼 ) ‘ 1 ) = ( 𝑔 ‘ 0 ) )
89 88 77 75 pcohtpy ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐼 ) ( *𝑝 ‘ 𝐽 ) 𝑔 ) ( ≃ph ‘ 𝐽 ) ( ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ( *𝑝 ‘ 𝐽 ) 𝑔 ) )
90 67 pcopt ⊢ ( ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( 𝑔 ‘ 0 ) = ( 𝐹 ‘ 0 ) ) → ( ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ( *𝑝 ‘ 𝐽 ) 𝑔 ) ( ≃ph ‘ 𝐽 ) 𝑔 )
91 28 34 90 syl2anc ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ( *𝑝 ‘ 𝐽 ) 𝑔 ) ( ≃ph ‘ 𝐽 ) 𝑔 )
92 62 89 91 ertrd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐼 ) ( *𝑝 ‘ 𝐽 ) 𝑔 ) ( ≃ph ‘ 𝐽 ) 𝑔 )
93 62 86 92 ertr3d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝐼 ( *𝑝 ‘ 𝐽 ) 𝑔 ) ) ( ≃ph ‘ 𝐽 ) 𝑔 )
94 62 85 93 ertr3d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ( ≃ph ‘ 𝐽 ) 𝑔 )
95 62 94 erthi ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) = [ 𝑔 ] ( ≃ph ‘ 𝐽 ) )
96 95 opeq2d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ∪ 𝐵 ) → ⟨ [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ = ⟨ [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) , [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ⟩ )
97 96 mpteq2dva ⊢ ( 𝜑 → ( 𝑔 ∈ ∪ 𝐵 ↦ ⟨ [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ ) = ( 𝑔 ∈ ∪ 𝐵 ↦ ⟨ [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) , [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ⟩ ) )
98 60 97 eqtrd ⊢ ( 𝜑 → ( ( ℎ ∈ ∪ ( Base ‘ 𝑄 ) ↦ ⟨ [ ℎ ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ ) ∘ ( 𝑔 ∈ ∪ 𝐵 ↦ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ) ) = ( 𝑔 ∈ ∪ 𝐵 ↦ ⟨ [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) , [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ⟩ ) )
99 98 rneqd ⊢ ( 𝜑 → ran ( ( ℎ ∈ ∪ ( Base ‘ 𝑄 ) ↦ ⟨ [ ℎ ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ ) ∘ ( 𝑔 ∈ ∪ 𝐵 ↦ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ) ) = ran ( 𝑔 ∈ ∪ 𝐵 ↦ ⟨ [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) , [ 𝑔 ] ( ≃ph ‘ 𝐽 ) ⟩ ) )
100 14 99 eqtr4d ⊢ ( 𝜑 → ◡ 𝐺 = ran ( ( ℎ ∈ ∪ ( Base ‘ 𝑄 ) ↦ ⟨ [ ℎ ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ ) ∘ ( 𝑔 ∈ ∪ 𝐵 ↦ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ) ) )
101 rncoss ⊢ ran ( ( ℎ ∈ ∪ ( Base ‘ 𝑄 ) ↦ ⟨ [ ℎ ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ ) ∘ ( 𝑔 ∈ ∪ 𝐵 ↦ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ) ) ⊆ ran ( ℎ ∈ ∪ ( Base ‘ 𝑄 ) ↦ ⟨ [ ℎ ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ )
102 101 8 sseqtrri ⊢ ran ( ( ℎ ∈ ∪ ( Base ‘ 𝑄 ) ↦ ⟨ [ ℎ ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ ) ∘ ( 𝑔 ∈ ∪ 𝐵 ↦ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ) ) ⊆ 𝐻
103 100 102 eqsstrdi ⊢ ( 𝜑 → ◡ 𝐺 ⊆ 𝐻 )