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	syl6eq	⊢ ( 𝑥 = 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	syl6eq	⊢ ( 𝑥 = 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	syl6eqr	⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ( 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 𝑃 ) ) )