Metamath Proof Explorer


Theorem pi1xfrcnv

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 pi1xfrcnv ( 𝜑 → ( 𝐺 = 𝐻 𝐺 ∈ ( 𝑄 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 pi1xfrcnv.h 𝐻 = ran ( ( Base ‘ 𝑄 ) ↦ ⟨ [ ] ( ≃ph𝐽 ) , [ ( 𝐹 ( *𝑝𝐽 ) ( ( *𝑝𝐽 ) 𝐼 ) ) ] ( ≃ph𝐽 ) ⟩ )
9 1 2 3 4 5 6 7 8 pi1xfrcnvlem ( 𝜑 𝐺𝐻 )
10 fvex ( ≃ph𝐽 ) ∈ V
11 ecexg ( ( ≃ph𝐽 ) ∈ V → [ ] ( ≃ph𝐽 ) ∈ V )
12 10 11 mp1i ( ( 𝜑 ( Base ‘ 𝑄 ) ) → [ ] ( ≃ph𝐽 ) ∈ V )
13 ecexg ( ( ≃ph𝐽 ) ∈ V → [ ( 𝐹 ( *𝑝𝐽 ) ( ( *𝑝𝐽 ) 𝐼 ) ) ] ( ≃ph𝐽 ) ∈ V )
14 10 13 mp1i ( ( 𝜑 ( Base ‘ 𝑄 ) ) → [ ( 𝐹 ( *𝑝𝐽 ) ( ( *𝑝𝐽 ) 𝐼 ) ) ] ( ≃ph𝐽 ) ∈ V )
15 8 12 14 fliftrel ( 𝜑𝐻 ⊆ ( V × V ) )
16 df-rel ( Rel 𝐻𝐻 ⊆ ( V × V ) )
17 15 16 sylibr ( 𝜑 → Rel 𝐻 )
18 dfrel2 ( Rel 𝐻 𝐻 = 𝐻 )
19 17 18 sylib ( 𝜑 𝐻 = 𝐻 )
20 0elunit 0 ∈ ( 0 [,] 1 )
21 oveq2 ( 𝑥 = 0 → ( 1 − 𝑥 ) = ( 1 − 0 ) )
22 1m0e1 ( 1 − 0 ) = 1
23 21 22 eqtrdi ( 𝑥 = 0 → ( 1 − 𝑥 ) = 1 )
24 23 fveq2d ( 𝑥 = 0 → ( 𝐹 ‘ ( 1 − 𝑥 ) ) = ( 𝐹 ‘ 1 ) )
25 fvex ( 𝐹 ‘ 1 ) ∈ V
26 24 7 25 fvmpt ( 0 ∈ ( 0 [,] 1 ) → ( 𝐼 ‘ 0 ) = ( 𝐹 ‘ 1 ) )
27 20 26 ax-mp ( 𝐼 ‘ 0 ) = ( 𝐹 ‘ 1 )
28 27 oveq2i ( 𝐽 π1 ( 𝐼 ‘ 0 ) ) = ( 𝐽 π1 ( 𝐹 ‘ 1 ) )
29 2 28 eqtr4i 𝑄 = ( 𝐽 π1 ( 𝐼 ‘ 0 ) )
30 1elunit 1 ∈ ( 0 [,] 1 )
31 oveq2 ( 𝑥 = 1 → ( 1 − 𝑥 ) = ( 1 − 1 ) )
32 31 fveq2d ( 𝑥 = 1 → ( 𝐹 ‘ ( 1 − 𝑥 ) ) = ( 𝐹 ‘ ( 1 − 1 ) ) )
33 1m1e0 ( 1 − 1 ) = 0
34 33 fveq2i ( 𝐹 ‘ ( 1 − 1 ) ) = ( 𝐹 ‘ 0 )
35 32 34 eqtrdi ( 𝑥 = 1 → ( 𝐹 ‘ ( 1 − 𝑥 ) ) = ( 𝐹 ‘ 0 ) )
36 fvex ( 𝐹 ‘ 0 ) ∈ V
37 35 7 36 fvmpt ( 1 ∈ ( 0 [,] 1 ) → ( 𝐼 ‘ 1 ) = ( 𝐹 ‘ 0 ) )
38 30 37 ax-mp ( 𝐼 ‘ 1 ) = ( 𝐹 ‘ 0 )
39 38 oveq2i ( 𝐽 π1 ( 𝐼 ‘ 1 ) ) = ( 𝐽 π1 ( 𝐹 ‘ 0 ) )
40 1 39 eqtr4i 𝑃 = ( 𝐽 π1 ( 𝐼 ‘ 1 ) )
41 eqid ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
42 eqid ran ( ( Base ‘ 𝑄 ) ↦ ⟨ [ ] ( ≃ph𝐽 ) , [ ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ( *𝑝𝐽 ) ( ( *𝑝𝐽 ) 𝐼 ) ) ] ( ≃ph𝐽 ) ⟩ ) = ran ( ( Base ‘ 𝑄 ) ↦ ⟨ [ ] ( ≃ph𝐽 ) , [ ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ( *𝑝𝐽 ) ( ( *𝑝𝐽 ) 𝐼 ) ) ] ( ≃ph𝐽 ) ⟩ )
43 7 pcorevcl ( 𝐹 ∈ ( II Cn 𝐽 ) → ( 𝐼 ∈ ( II Cn 𝐽 ) ∧ ( 𝐼 ‘ 0 ) = ( 𝐹 ‘ 1 ) ∧ ( 𝐼 ‘ 1 ) = ( 𝐹 ‘ 0 ) ) )
44 6 43 syl ( 𝜑 → ( 𝐼 ∈ ( II Cn 𝐽 ) ∧ ( 𝐼 ‘ 0 ) = ( 𝐹 ‘ 1 ) ∧ ( 𝐼 ‘ 1 ) = ( 𝐹 ‘ 0 ) ) )
45 44 simp1d ( 𝜑𝐼 ∈ ( II Cn 𝐽 ) )
46 oveq2 ( 𝑧 = 𝑦 → ( 1 − 𝑧 ) = ( 1 − 𝑦 ) )
47 46 fveq2d ( 𝑧 = 𝑦 → ( 𝐼 ‘ ( 1 − 𝑧 ) ) = ( 𝐼 ‘ ( 1 − 𝑦 ) ) )
48 47 cbvmptv ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) = ( 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑦 ) ) )
49 eqid ran ( 𝑔 ( Base ‘ 𝑃 ) ↦ ⟨ [ 𝑔 ] ( ≃ph𝐽 ) , [ ( 𝐼 ( *𝑝𝐽 ) ( 𝑔 ( *𝑝𝐽 ) ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ) ) ] ( ≃ph𝐽 ) ⟩ ) = ran ( 𝑔 ( Base ‘ 𝑃 ) ↦ ⟨ [ 𝑔 ] ( ≃ph𝐽 ) , [ ( 𝐼 ( *𝑝𝐽 ) ( 𝑔 ( *𝑝𝐽 ) ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ) ) ] ( ≃ph𝐽 ) ⟩ )
50 29 40 41 42 5 45 48 49 pi1xfrcnvlem ( 𝜑 ran ( ( Base ‘ 𝑄 ) ↦ ⟨ [ ] ( ≃ph𝐽 ) , [ ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ( *𝑝𝐽 ) ( ( *𝑝𝐽 ) 𝐼 ) ) ] ( ≃ph𝐽 ) ⟩ ) ⊆ ran ( 𝑔 ( Base ‘ 𝑃 ) ↦ ⟨ [ 𝑔 ] ( ≃ph𝐽 ) , [ ( 𝐼 ( *𝑝𝐽 ) ( 𝑔 ( *𝑝𝐽 ) ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ) ) ] ( ≃ph𝐽 ) ⟩ ) )
51 iitopon II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
52 cnf2 ( ( II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( II Cn 𝐽 ) ) → 𝐹 : ( 0 [,] 1 ) ⟶ 𝑋 )
53 51 5 6 52 mp3an2i ( 𝜑𝐹 : ( 0 [,] 1 ) ⟶ 𝑋 )
54 53 feqmptd ( 𝜑𝐹 = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐹𝑧 ) ) )
55 iirev ( 𝑧 ∈ ( 0 [,] 1 ) → ( 1 − 𝑧 ) ∈ ( 0 [,] 1 ) )
56 oveq2 ( 𝑥 = ( 1 − 𝑧 ) → ( 1 − 𝑥 ) = ( 1 − ( 1 − 𝑧 ) ) )
57 56 fveq2d ( 𝑥 = ( 1 − 𝑧 ) → ( 𝐹 ‘ ( 1 − 𝑥 ) ) = ( 𝐹 ‘ ( 1 − ( 1 − 𝑧 ) ) ) )
58 fvex ( 𝐹 ‘ ( 1 − ( 1 − 𝑧 ) ) ) ∈ V
59 57 7 58 fvmpt ( ( 1 − 𝑧 ) ∈ ( 0 [,] 1 ) → ( 𝐼 ‘ ( 1 − 𝑧 ) ) = ( 𝐹 ‘ ( 1 − ( 1 − 𝑧 ) ) ) )
60 55 59 syl ( 𝑧 ∈ ( 0 [,] 1 ) → ( 𝐼 ‘ ( 1 − 𝑧 ) ) = ( 𝐹 ‘ ( 1 − ( 1 − 𝑧 ) ) ) )
61 ax-1cn 1 ∈ ℂ
62 unitssre ( 0 [,] 1 ) ⊆ ℝ
63 62 sseli ( 𝑧 ∈ ( 0 [,] 1 ) → 𝑧 ∈ ℝ )
64 63 recnd ( 𝑧 ∈ ( 0 [,] 1 ) → 𝑧 ∈ ℂ )
65 nncan ( ( 1 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 1 − ( 1 − 𝑧 ) ) = 𝑧 )
66 61 64 65 sylancr ( 𝑧 ∈ ( 0 [,] 1 ) → ( 1 − ( 1 − 𝑧 ) ) = 𝑧 )
67 66 fveq2d ( 𝑧 ∈ ( 0 [,] 1 ) → ( 𝐹 ‘ ( 1 − ( 1 − 𝑧 ) ) ) = ( 𝐹𝑧 ) )
68 60 67 eqtrd ( 𝑧 ∈ ( 0 [,] 1 ) → ( 𝐼 ‘ ( 1 − 𝑧 ) ) = ( 𝐹𝑧 ) )
69 68 mpteq2ia ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐹𝑧 ) )
70 54 69 eqtr4di ( 𝜑𝐹 = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) )
71 70 oveq1d ( 𝜑 → ( 𝐹 ( *𝑝𝐽 ) ( ( *𝑝𝐽 ) 𝐼 ) ) = ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ( *𝑝𝐽 ) ( ( *𝑝𝐽 ) 𝐼 ) ) )
72 71 eceq1d ( 𝜑 → [ ( 𝐹 ( *𝑝𝐽 ) ( ( *𝑝𝐽 ) 𝐼 ) ) ] ( ≃ph𝐽 ) = [ ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ( *𝑝𝐽 ) ( ( *𝑝𝐽 ) 𝐼 ) ) ] ( ≃ph𝐽 ) )
73 72 opeq2d ( 𝜑 → ⟨ [ ] ( ≃ph𝐽 ) , [ ( 𝐹 ( *𝑝𝐽 ) ( ( *𝑝𝐽 ) 𝐼 ) ) ] ( ≃ph𝐽 ) ⟩ = ⟨ [ ] ( ≃ph𝐽 ) , [ ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ( *𝑝𝐽 ) ( ( *𝑝𝐽 ) 𝐼 ) ) ] ( ≃ph𝐽 ) ⟩ )
74 73 mpteq2dv ( 𝜑 → ( ( Base ‘ 𝑄 ) ↦ ⟨ [ ] ( ≃ph𝐽 ) , [ ( 𝐹 ( *𝑝𝐽 ) ( ( *𝑝𝐽 ) 𝐼 ) ) ] ( ≃ph𝐽 ) ⟩ ) = ( ( Base ‘ 𝑄 ) ↦ ⟨ [ ] ( ≃ph𝐽 ) , [ ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ( *𝑝𝐽 ) ( ( *𝑝𝐽 ) 𝐼 ) ) ] ( ≃ph𝐽 ) ⟩ ) )
75 74 rneqd ( 𝜑 → ran ( ( Base ‘ 𝑄 ) ↦ ⟨ [ ] ( ≃ph𝐽 ) , [ ( 𝐹 ( *𝑝𝐽 ) ( ( *𝑝𝐽 ) 𝐼 ) ) ] ( ≃ph𝐽 ) ⟩ ) = ran ( ( Base ‘ 𝑄 ) ↦ ⟨ [ ] ( ≃ph𝐽 ) , [ ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ( *𝑝𝐽 ) ( ( *𝑝𝐽 ) 𝐼 ) ) ] ( ≃ph𝐽 ) ⟩ ) )
76 8 75 syl5eq ( 𝜑𝐻 = ran ( ( Base ‘ 𝑄 ) ↦ ⟨ [ ] ( ≃ph𝐽 ) , [ ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ( *𝑝𝐽 ) ( ( *𝑝𝐽 ) 𝐼 ) ) ] ( ≃ph𝐽 ) ⟩ ) )
77 76 cnveqd ( 𝜑 𝐻 = ran ( ( Base ‘ 𝑄 ) ↦ ⟨ [ ] ( ≃ph𝐽 ) , [ ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ( *𝑝𝐽 ) ( ( *𝑝𝐽 ) 𝐼 ) ) ] ( ≃ph𝐽 ) ⟩ ) )
78 3 a1i ( 𝜑𝐵 = ( Base ‘ 𝑃 ) )
79 78 unieqd ( 𝜑 𝐵 = ( Base ‘ 𝑃 ) )
80 70 oveq2d ( 𝜑 → ( 𝑔 ( *𝑝𝐽 ) 𝐹 ) = ( 𝑔 ( *𝑝𝐽 ) ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ) )
81 80 oveq2d ( 𝜑 → ( 𝐼 ( *𝑝𝐽 ) ( 𝑔 ( *𝑝𝐽 ) 𝐹 ) ) = ( 𝐼 ( *𝑝𝐽 ) ( 𝑔 ( *𝑝𝐽 ) ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ) ) )
82 81 eceq1d ( 𝜑 → [ ( 𝐼 ( *𝑝𝐽 ) ( 𝑔 ( *𝑝𝐽 ) 𝐹 ) ) ] ( ≃ph𝐽 ) = [ ( 𝐼 ( *𝑝𝐽 ) ( 𝑔 ( *𝑝𝐽 ) ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ) ) ] ( ≃ph𝐽 ) )
83 82 opeq2d ( 𝜑 → ⟨ [ 𝑔 ] ( ≃ph𝐽 ) , [ ( 𝐼 ( *𝑝𝐽 ) ( 𝑔 ( *𝑝𝐽 ) 𝐹 ) ) ] ( ≃ph𝐽 ) ⟩ = ⟨ [ 𝑔 ] ( ≃ph𝐽 ) , [ ( 𝐼 ( *𝑝𝐽 ) ( 𝑔 ( *𝑝𝐽 ) ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ) ) ] ( ≃ph𝐽 ) ⟩ )
84 79 83 mpteq12dv ( 𝜑 → ( 𝑔 𝐵 ↦ ⟨ [ 𝑔 ] ( ≃ph𝐽 ) , [ ( 𝐼 ( *𝑝𝐽 ) ( 𝑔 ( *𝑝𝐽 ) 𝐹 ) ) ] ( ≃ph𝐽 ) ⟩ ) = ( 𝑔 ( Base ‘ 𝑃 ) ↦ ⟨ [ 𝑔 ] ( ≃ph𝐽 ) , [ ( 𝐼 ( *𝑝𝐽 ) ( 𝑔 ( *𝑝𝐽 ) ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ) ) ] ( ≃ph𝐽 ) ⟩ ) )
85 84 rneqd ( 𝜑 → ran ( 𝑔 𝐵 ↦ ⟨ [ 𝑔 ] ( ≃ph𝐽 ) , [ ( 𝐼 ( *𝑝𝐽 ) ( 𝑔 ( *𝑝𝐽 ) 𝐹 ) ) ] ( ≃ph𝐽 ) ⟩ ) = ran ( 𝑔 ( Base ‘ 𝑃 ) ↦ ⟨ [ 𝑔 ] ( ≃ph𝐽 ) , [ ( 𝐼 ( *𝑝𝐽 ) ( 𝑔 ( *𝑝𝐽 ) ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ) ) ] ( ≃ph𝐽 ) ⟩ ) )
86 4 85 syl5eq ( 𝜑𝐺 = ran ( 𝑔 ( Base ‘ 𝑃 ) ↦ ⟨ [ 𝑔 ] ( ≃ph𝐽 ) , [ ( 𝐼 ( *𝑝𝐽 ) ( 𝑔 ( *𝑝𝐽 ) ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ) ) ] ( ≃ph𝐽 ) ⟩ ) )
87 50 77 86 3sstr4d ( 𝜑 𝐻𝐺 )
88 cnvss ( 𝐻𝐺 𝐻 𝐺 )
89 87 88 syl ( 𝜑 𝐻 𝐺 )
90 19 89 eqsstrrd ( 𝜑𝐻 𝐺 )
91 9 90 eqssd ( 𝜑 𝐺 = 𝐻 )
92 91 76 eqtrd ( 𝜑 𝐺 = ran ( ( Base ‘ 𝑄 ) ↦ ⟨ [ ] ( ≃ph𝐽 ) , [ ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ( *𝑝𝐽 ) ( ( *𝑝𝐽 ) 𝐼 ) ) ] ( ≃ph𝐽 ) ⟩ ) )
93 29 40 41 42 5 45 48 pi1xfr ( 𝜑 → ran ( ( Base ‘ 𝑄 ) ↦ ⟨ [ ] ( ≃ph𝐽 ) , [ ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐼 ‘ ( 1 − 𝑧 ) ) ) ( *𝑝𝐽 ) ( ( *𝑝𝐽 ) 𝐼 ) ) ] ( ≃ph𝐽 ) ⟩ ) ∈ ( 𝑄 GrpHom 𝑃 ) )
94 92 93 eqeltrd ( 𝜑 𝐺 ∈ ( 𝑄 GrpHom 𝑃 ) )
95 91 94 jca ( 𝜑 → ( 𝐺 = 𝐻 𝐺 ∈ ( 𝑄 GrpHom 𝑃 ) ) )