pi1xfr - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > pi1xfr		Structured version Visualization version GIF version

Theorem pi1xfr 22855

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

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

**Assertion**
Ref	Expression
pi1xfr	⊢ (𝜑 → 𝐺 ∈ (𝑃 GrpHom 𝑄))

Distinct variable groups: 𝑥,𝑔,𝐵 𝑔,𝐹,𝑥 𝑔,𝐼,𝑥 𝜑,𝑔,𝑥 𝑔,𝐽,𝑥 𝑃,𝑔,𝑥 𝑄,𝑔,𝑥 Allowed substitution hints: 𝐺(𝑥,𝑔) 𝑋(𝑥,𝑔)

Proof of Theorem pi1xfr Dummy variables 𝑓 ℎ 𝑢 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		pi1xfr.j	. . . 4 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
2		iitopon 22682	. . . . . . 7 ⊢ II ∈ (TopOn‘(0[,]1))
3	2	a1i 11	. . . . . 6 ⊢ (𝜑 → II ∈ (TopOn‘(0[,]1)))
4		pi1xfr.f	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))
5		cnf2 21053	. . . . . 6 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ 𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (II Cn 𝐽)) → 𝐹:(0[,]1)⟶𝑋)
6	3, 1, 4, 5	syl3anc 1326	. . . . 5 ⊢ (𝜑 → 𝐹:(0[,]1)⟶𝑋)
7		0elunit 12290	. . . . 5 ⊢ 0 ∈ (0[,]1)
8		ffvelrn 6357	. . . . 5 ⊢ ((𝐹:(0[,]1)⟶𝑋 ∧ 0 ∈ (0[,]1)) → (𝐹‘0) ∈ 𝑋)
9	6, 7, 8	sylancl 694	. . . 4 ⊢ (𝜑 → (𝐹‘0) ∈ 𝑋)
10		pi1xfr.p	. . . . 5 ⊢ 𝑃 = (𝐽 π₁ (𝐹‘0))
11	10	pi1grp 22850	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐹‘0) ∈ 𝑋) → 𝑃 ∈ Grp)
12	1, 9, 11	syl2anc 693	. . 3 ⊢ (𝜑 → 𝑃 ∈ Grp)
13		1elunit 12291	. . . . 5 ⊢ 1 ∈ (0[,]1)
14		ffvelrn 6357	. . . . 5 ⊢ ((𝐹:(0[,]1)⟶𝑋 ∧ 1 ∈ (0[,]1)) → (𝐹‘1) ∈ 𝑋)
15	6, 13, 14	sylancl 694	. . . 4 ⊢ (𝜑 → (𝐹‘1) ∈ 𝑋)
16		pi1xfr.q	. . . . 5 ⊢ 𝑄 = (𝐽 π₁ (𝐹‘1))
17	16	pi1grp 22850	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐹‘1) ∈ 𝑋) → 𝑄 ∈ Grp)
18	1, 15, 17	syl2anc 693	. . 3 ⊢ (𝜑 → 𝑄 ∈ Grp)
19	12, 18	jca 554	. 2 ⊢ (𝜑 → (𝑃 ∈ Grp ∧ 𝑄 ∈ Grp))
20		pi1xfr.b	. . . 4 ⊢ 𝐵 = (Base‘𝑃)
21		pi1xfr.g	. . . 4 ⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝐵 ↦ ⟨[𝑔]( ≃_ph‘𝐽), [(𝐼(_𝑝‘𝐽)(𝑔(_𝑝‘𝐽)𝐹))]( ≃_ph‘𝐽)⟩)
22		pi1xfr.i	. . . . . . 7 ⊢ 𝐼 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥)))
23	22	pcorevcl 22825	. . . . . 6 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐼 ∈ (II Cn 𝐽) ∧ (𝐼‘0) = (𝐹‘1) ∧ (𝐼‘1) = (𝐹‘0)))
24	4, 23	syl 17	. . . . 5 ⊢ (𝜑 → (𝐼 ∈ (II Cn 𝐽) ∧ (𝐼‘0) = (𝐹‘1) ∧ (𝐼‘1) = (𝐹‘0)))
25	24	simp1d 1073	. . . 4 ⊢ (𝜑 → 𝐼 ∈ (II Cn 𝐽))
26	24	simp2d 1074	. . . . 5 ⊢ (𝜑 → (𝐼‘0) = (𝐹‘1))
27	26	eqcomd 2628	. . . 4 ⊢ (𝜑 → (𝐹‘1) = (𝐼‘0))
28	24	simp3d 1075	. . . 4 ⊢ (𝜑 → (𝐼‘1) = (𝐹‘0))
29	10, 16, 20, 21, 1, 4, 25, 27, 28	pi1xfrf 22853	. . 3 ⊢ (𝜑 → 𝐺:𝐵⟶(Base‘𝑄))
30	20	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐵 = (Base‘𝑃))
31	10, 1, 9, 30	pi1bas2 22841	. . . . . . 7 ⊢ (𝜑 → 𝐵 = (∪ 𝐵 / ( ≃_ph‘𝐽)))
32	31	eleq2d 2687	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (∪ 𝐵 / ( ≃_ph‘𝐽))))
33	32	biimpa 501	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ (∪ 𝐵 / ( ≃_ph‘𝐽)))
34		eqid 2622	. . . . . 6 ⊢ (∪ 𝐵 / ( ≃_ph‘𝐽)) = (∪ 𝐵 / ( ≃_ph‘𝐽))
35		oveq1 6657	. . . . . . . . 9 ⊢ ([𝑓]( ≃_ph‘𝐽) = 𝑦 → ([𝑓]( ≃_ph‘𝐽)(+_g‘𝑃)𝑧) = (𝑦(+_g‘𝑃)𝑧))
36	35	fveq2d 6195	. . . . . . . 8 ⊢ ([𝑓]( ≃_ph‘𝐽) = 𝑦 → (𝐺‘([𝑓]( ≃_ph‘𝐽)(+_g‘𝑃)𝑧)) = (𝐺‘(𝑦(+_g‘𝑃)𝑧)))
37		fveq2 6191	. . . . . . . . 9 ⊢ ([𝑓]( ≃_ph‘𝐽) = 𝑦 → (𝐺‘[𝑓]( ≃_ph‘𝐽)) = (𝐺‘𝑦))
38	37	oveq1d 6665	. . . . . . . 8 ⊢ ([𝑓]( ≃_ph‘𝐽) = 𝑦 → ((𝐺‘[𝑓]( ≃_ph‘𝐽))(+_g‘𝑄)(𝐺‘𝑧)) = ((𝐺‘𝑦)(+_g‘𝑄)(𝐺‘𝑧)))
39	36, 38	eqeq12d 2637	. . . . . . 7 ⊢ ([𝑓]( ≃_ph‘𝐽) = 𝑦 → ((𝐺‘([𝑓]( ≃_ph‘𝐽)(+_g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃_ph‘𝐽))(+_g‘𝑄)(𝐺‘𝑧)) ↔ (𝐺‘(𝑦(+_g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+_g‘𝑄)(𝐺‘𝑧))))
40	39	ralbidv 2986	. . . . . 6 ⊢ ([𝑓]( ≃_ph‘𝐽) = 𝑦 → (∀𝑧 ∈ 𝐵 (𝐺‘([𝑓]( ≃_ph‘𝐽)(+_g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃_ph‘𝐽))(+_g‘𝑄)(𝐺‘𝑧)) ↔ ∀𝑧 ∈ 𝐵 (𝐺‘(𝑦(+_g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+_g‘𝑄)(𝐺‘𝑧))))
41	31	eleq2d 2687	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ (∪ 𝐵 / ( ≃_ph‘𝐽))))
42	41	biimpa 501	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ (∪ 𝐵 / ( ≃_ph‘𝐽)))
43	42	adantlr 751	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ (∪ 𝐵 / ( ≃_ph‘𝐽)))
44		oveq2 6658	. . . . . . . . . . 11 ⊢ ([ℎ]( ≃_ph‘𝐽) = 𝑧 → ([𝑓]( ≃_ph‘𝐽)(+_g‘𝑃)[ℎ]( ≃_ph‘𝐽)) = ([𝑓]( ≃_ph‘𝐽)(+_g‘𝑃)𝑧))
45	44	fveq2d 6195	. . . . . . . . . 10 ⊢ ([ℎ]( ≃_ph‘𝐽) = 𝑧 → (𝐺‘([𝑓]( ≃_ph‘𝐽)(+_g‘𝑃)[ℎ]( ≃_ph‘𝐽))) = (𝐺‘([𝑓]( ≃_ph‘𝐽)(+_g‘𝑃)𝑧)))
46		fveq2 6191	. . . . . . . . . . 11 ⊢ ([ℎ]( ≃_ph‘𝐽) = 𝑧 → (𝐺‘[ℎ]( ≃_ph‘𝐽)) = (𝐺‘𝑧))
47	46	oveq2d 6666	. . . . . . . . . 10 ⊢ ([ℎ]( ≃_ph‘𝐽) = 𝑧 → ((𝐺‘[𝑓]( ≃_ph‘𝐽))(+_g‘𝑄)(𝐺‘[ℎ]( ≃_ph‘𝐽))) = ((𝐺‘[𝑓]( ≃_ph‘𝐽))(+_g‘𝑄)(𝐺‘𝑧)))
48	45, 47	eqeq12d 2637	. . . . . . . . 9 ⊢ ([ℎ]( ≃_ph‘𝐽) = 𝑧 → ((𝐺‘([𝑓]( ≃_ph‘𝐽)(+_g‘𝑃)[ℎ]( ≃_ph‘𝐽))) = ((𝐺‘[𝑓]( ≃_ph‘𝐽))(+_g‘𝑄)(𝐺‘[ℎ]( ≃_ph‘𝐽))) ↔ (𝐺‘([𝑓]( ≃_ph‘𝐽)(+_g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃_ph‘𝐽))(+_g‘𝑄)(𝐺‘𝑧))))
49		phtpcer 22794	. . . . . . . . . . . . . 14 ⊢ ( ≃_ph‘𝐽) Er (II Cn 𝐽)
50	49	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ( ≃_ph‘𝐽) Er (II Cn 𝐽))
51	10, 1, 9, 30	pi1eluni 22842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑓 ∈ ∪ 𝐵 ↔ (𝑓 ∈ (II Cn 𝐽) ∧ (𝑓‘0) = (𝐹‘0) ∧ (𝑓‘1) = (𝐹‘0))))
52	51	biimpa 501	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (𝑓 ∈ (II Cn 𝐽) ∧ (𝑓‘0) = (𝐹‘0) ∧ (𝑓‘1) = (𝐹‘0)))
53	52	simp1d 1073	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → 𝑓 ∈ (II Cn 𝐽))
54	53	3adant3 1081	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → 𝑓 ∈ (II Cn 𝐽))
55	10, 1, 9, 30	pi1eluni 22842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (ℎ ∈ ∪ 𝐵 ↔ (ℎ ∈ (II Cn 𝐽) ∧ (ℎ‘0) = (𝐹‘0) ∧ (ℎ‘1) = (𝐹‘0))))
56	55	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (ℎ ∈ ∪ 𝐵 ↔ (ℎ ∈ (II Cn 𝐽) ∧ (ℎ‘0) = (𝐹‘0) ∧ (ℎ‘1) = (𝐹‘0))))
57	56	biimp3a 1432	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (ℎ ∈ (II Cn 𝐽) ∧ (ℎ‘0) = (𝐹‘0) ∧ (ℎ‘1) = (𝐹‘0)))
58	57	simp1d 1073	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ℎ ∈ (II Cn 𝐽))
59	54, 58	pco0 22814	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝑓(*_𝑝‘𝐽)ℎ)‘0) = (𝑓‘0))
60	52	simp2d 1074	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (𝑓‘0) = (𝐹‘0))
61	60	3adant3 1081	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝑓‘0) = (𝐹‘0))
62	59, 61	eqtrd 2656	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝑓(*_𝑝‘𝐽)ℎ)‘0) = (𝐹‘0))
63	52	simp3d 1075	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (𝑓‘1) = (𝐹‘0))
64	63	3adant3 1081	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝑓‘1) = (𝐹‘0))
65	57	simp2d 1074	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (ℎ‘0) = (𝐹‘0))
66	64, 65	eqtr4d 2659	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝑓‘1) = (ℎ‘0))
67	54, 58, 66	pcocn 22817	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝑓(*_𝑝‘𝐽)ℎ) ∈ (II Cn 𝐽))
68	4	3ad2ant1 1082	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → 𝐹 ∈ (II Cn 𝐽))
69	67, 68	pco0 22814	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (((𝑓(_𝑝‘𝐽)ℎ)(_𝑝‘𝐽)𝐹)‘0) = ((𝑓(*_𝑝‘𝐽)ℎ)‘0))
70	28	3ad2ant1 1082	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼‘1) = (𝐹‘0))
71	62, 69, 70	3eqtr4rd 2667	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼‘1) = (((𝑓(_𝑝‘𝐽)ℎ)(_𝑝‘𝐽)𝐹)‘0))
72	25	3ad2ant1 1082	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → 𝐼 ∈ (II Cn 𝐽))
73	50, 72	erref 7762	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → 𝐼( ≃_ph‘𝐽)𝐼)
74	57	simp3d 1075	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (ℎ‘1) = (𝐹‘0))
75		eqid 2622	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ (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))))
76	54, 58, 68, 66, 74, 75	pcoass 22824	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝑓(_𝑝‘𝐽)ℎ)(_𝑝‘𝐽)𝐹)( ≃_ph‘𝐽)(𝑓(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹)))
77	58, 68	pco0 22814	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((ℎ(*_𝑝‘𝐽)𝐹)‘0) = (ℎ‘0))
78	66, 77	eqtr4d 2659	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝑓‘1) = ((ℎ(*_𝑝‘𝐽)𝐹)‘0))
79	50, 54	erref 7762	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → 𝑓( ≃_ph‘𝐽)𝑓)
80	68, 72	pco1 22815	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐹(*_𝑝‘𝐽)𝐼)‘1) = (𝐼‘1))
81	65, 77, 70	3eqtr4rd 2667	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼‘1) = ((ℎ(*_𝑝‘𝐽)𝐹)‘0))
82	80, 81	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐹(_𝑝‘𝐽)𝐼)‘1) = ((ℎ(_𝑝‘𝐽)𝐹)‘0))
83		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((0[,]1) × {(𝐹‘0)}) = ((0[,]1) × {(𝐹‘0)})
84	22, 83	pcorev2 22828	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐹(*_𝑝‘𝐽)𝐼)( ≃_ph‘𝐽)((0[,]1) × {(𝐹‘0)}))
85	68, 84	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐹(*_𝑝‘𝐽)𝐼)( ≃_ph‘𝐽)((0[,]1) × {(𝐹‘0)}))
86	58, 68, 74	pcocn 22817	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (ℎ(*_𝑝‘𝐽)𝐹) ∈ (II Cn 𝐽))
87	50, 86	erref 7762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (ℎ(_𝑝‘𝐽)𝐹)( ≃_ph‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))
88	82, 85, 87	pcohtpy 22820	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐹(_𝑝‘𝐽)𝐼)(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))( ≃_ph‘𝐽)(((0[,]1) × {(𝐹‘0)})(_𝑝‘𝐽)(ℎ(*_𝑝‘𝐽)𝐹)))
89	77, 65	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((ℎ(*_𝑝‘𝐽)𝐹)‘0) = (𝐹‘0))
90	83	pcopt 22822	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ(_𝑝‘𝐽)𝐹) ∈ (II Cn 𝐽) ∧ ((ℎ(_𝑝‘𝐽)𝐹)‘0) = (𝐹‘0)) → (((0[,]1) × {(𝐹‘0)})(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))( ≃_ph‘𝐽)(ℎ(*_𝑝‘𝐽)𝐹))
91	86, 89, 90	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (((0[,]1) × {(𝐹‘0)})(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))( ≃_ph‘𝐽)(ℎ(*_𝑝‘𝐽)𝐹))
92	50, 88, 91	ertrd 7758	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐹(_𝑝‘𝐽)𝐼)(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))( ≃_ph‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))
93	26	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼‘0) = (𝐹‘1))
94	93	eqcomd 2628	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐹‘1) = (𝐼‘0))
95	68, 72, 86, 94, 81, 75	pcoass 22824	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐹(_𝑝‘𝐽)𝐼)(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))( ≃_ph‘𝐽)(𝐹(_𝑝‘𝐽)(𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))))
96	50, 92, 95	ertr3d 7760	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (ℎ(_𝑝‘𝐽)𝐹)( ≃_ph‘𝐽)(𝐹(_𝑝‘𝐽)(𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))))
97	78, 79, 96	pcohtpy 22820	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝑓(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))( ≃_ph‘𝐽)(𝑓(_𝑝‘𝐽)(𝐹(_𝑝‘𝐽)(𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹)))))
98	72, 86, 81	pcocn 22817	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹)) ∈ (II Cn 𝐽))
99	72, 86	pco0 22814	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))‘0) = (𝐼‘0))
100	99, 93	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))‘0) = (𝐹‘1))
101	100	eqcomd 2628	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐹‘1) = ((𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))‘0))
102	54, 68, 98, 64, 101, 75	pcoass 22824	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝑓(_𝑝‘𝐽)𝐹)(_𝑝‘𝐽)(𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹)))( ≃_ph‘𝐽)(𝑓(_𝑝‘𝐽)(𝐹(_𝑝‘𝐽)(𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹)))))
103	50, 97, 102	ertr4d 7761	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝑓(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))( ≃_ph‘𝐽)((𝑓(_𝑝‘𝐽)𝐹)(_𝑝‘𝐽)(𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))))
104	50, 76, 103	ertrd 7758	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝑓(_𝑝‘𝐽)ℎ)(_𝑝‘𝐽)𝐹)( ≃_ph‘𝐽)((𝑓(_𝑝‘𝐽)𝐹)(_𝑝‘𝐽)(𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))))
105	71, 73, 104	pcohtpy 22820	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼(_𝑝‘𝐽)((𝑓(_𝑝‘𝐽)ℎ)(_𝑝‘𝐽)𝐹))( ≃_ph‘𝐽)(𝐼(_𝑝‘𝐽)((𝑓(_𝑝‘𝐽)𝐹)(_𝑝‘𝐽)(𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹)))))
106	4	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → 𝐹 ∈ (II Cn 𝐽))
107	53, 106, 63	pcocn 22817	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (𝑓(*_𝑝‘𝐽)𝐹) ∈ (II Cn 𝐽))
108	107	3adant3 1081	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝑓(*_𝑝‘𝐽)𝐹) ∈ (II Cn 𝐽))
109	53, 106	pco0 22814	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → ((𝑓(*_𝑝‘𝐽)𝐹)‘0) = (𝑓‘0))
110	28	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (𝐼‘1) = (𝐹‘0))
111	60, 109, 110	3eqtr4rd 2667	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (𝐼‘1) = ((𝑓(*_𝑝‘𝐽)𝐹)‘0))
112	111	3adant3 1081	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼‘1) = ((𝑓(*_𝑝‘𝐽)𝐹)‘0))
113	54, 68	pco1 22815	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝑓(*_𝑝‘𝐽)𝐹)‘1) = (𝐹‘1))
114	113, 100	eqtr4d 2659	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝑓(_𝑝‘𝐽)𝐹)‘1) = ((𝐼(_𝑝‘𝐽)(ℎ(*_𝑝‘𝐽)𝐹))‘0))
115	72, 108, 98, 112, 114, 75	pcoass 22824	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹))(_𝑝‘𝐽)(𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹)))( ≃_ph‘𝐽)(𝐼(_𝑝‘𝐽)((𝑓(_𝑝‘𝐽)𝐹)(_𝑝‘𝐽)(𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹)))))
116	50, 105, 115	ertr4d 7761	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼(_𝑝‘𝐽)((𝑓(_𝑝‘𝐽)ℎ)(_𝑝‘𝐽)𝐹))( ≃_ph‘𝐽)((𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹))(_𝑝‘𝐽)(𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))))
117	50, 116	erthi 7793	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → [(𝐼(_𝑝‘𝐽)((𝑓(_𝑝‘𝐽)ℎ)(_𝑝‘𝐽)𝐹))]( ≃_ph‘𝐽) = [((𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹))(_𝑝‘𝐽)(𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹)))]( ≃_ph‘𝐽))
118	1	3ad2ant1 1082	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → 𝐽 ∈ (TopOn‘𝑋))
119	54, 58	pco1 22815	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝑓(*_𝑝‘𝐽)ℎ)‘1) = (ℎ‘1))
120	119, 74	eqtrd 2656	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝑓(*_𝑝‘𝐽)ℎ)‘1) = (𝐹‘0))
121	10, 1, 9, 30	pi1eluni 22842	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑓(_𝑝‘𝐽)ℎ) ∈ ∪ 𝐵 ↔ ((𝑓(_𝑝‘𝐽)ℎ) ∈ (II Cn 𝐽) ∧ ((𝑓(_𝑝‘𝐽)ℎ)‘0) = (𝐹‘0) ∧ ((𝑓(_𝑝‘𝐽)ℎ)‘1) = (𝐹‘0))))
122	121	3ad2ant1 1082	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝑓(_𝑝‘𝐽)ℎ) ∈ ∪ 𝐵 ↔ ((𝑓(_𝑝‘𝐽)ℎ) ∈ (II Cn 𝐽) ∧ ((𝑓(_𝑝‘𝐽)ℎ)‘0) = (𝐹‘0) ∧ ((𝑓(_𝑝‘𝐽)ℎ)‘1) = (𝐹‘0))))
123	67, 62, 120, 122	mpbir3and 1245	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝑓(*_𝑝‘𝐽)ℎ) ∈ ∪ 𝐵)
124	10, 16, 20, 21, 118, 68, 72, 94, 70, 123	pi1xfrval 22854	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐺‘[(𝑓(_𝑝‘𝐽)ℎ)]( ≃_ph‘𝐽)) = [(𝐼(_𝑝‘𝐽)((𝑓(_𝑝‘𝐽)ℎ)(_𝑝‘𝐽)𝐹))]( ≃_ph‘𝐽))
125		eqid 2622	. . . . . . . . . . . . 13 ⊢ (Base‘𝑄) = (Base‘𝑄)
126	15	3ad2ant1 1082	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐹‘1) ∈ 𝑋)
127		eqid 2622	. . . . . . . . . . . . 13 ⊢ (+_g‘𝑄) = (+_g‘𝑄)
128	25	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → 𝐼 ∈ (II Cn 𝐽))
129	128, 107, 111	pcocn 22817	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹)) ∈ (II Cn 𝐽))
130	129	3adant3 1081	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹)) ∈ (II Cn 𝐽))
131	128, 107	pco0 22814	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → ((𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹))‘0) = (𝐼‘0))
132	26	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (𝐼‘0) = (𝐹‘1))
133	131, 132	eqtrd 2656	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → ((𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹))‘0) = (𝐹‘1))
134	133	3adant3 1081	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹))‘0) = (𝐹‘1))
135	128, 107	pco1 22815	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → ((𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹))‘1) = ((𝑓(*_𝑝‘𝐽)𝐹)‘1))
136	53, 106	pco1 22815	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → ((𝑓(*_𝑝‘𝐽)𝐹)‘1) = (𝐹‘1))
137	135, 136	eqtrd 2656	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → ((𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹))‘1) = (𝐹‘1))
138	137	3adant3 1081	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹))‘1) = (𝐹‘1))
139		eqidd 2623	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (Base‘𝑄) = (Base‘𝑄))
140	16, 118, 126, 139	pi1eluni 22842	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹)) ∈ ∪ (Base‘𝑄) ↔ ((𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹)) ∈ (II Cn 𝐽) ∧ ((𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹))‘0) = (𝐹‘1) ∧ ((𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹))‘1) = (𝐹‘1))))
141	130, 134, 138, 140	mpbir3and 1245	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹)) ∈ ∪ (Base‘𝑄))
142	72, 86	pco1 22815	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))‘1) = ((ℎ(*_𝑝‘𝐽)𝐹)‘1))
143	58, 68	pco1 22815	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((ℎ(*_𝑝‘𝐽)𝐹)‘1) = (𝐹‘1))
144	142, 143	eqtrd 2656	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))‘1) = (𝐹‘1))
145	16, 118, 126, 139	pi1eluni 22842	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹)) ∈ ∪ (Base‘𝑄) ↔ ((𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹)) ∈ (II Cn 𝐽) ∧ ((𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))‘0) = (𝐹‘1) ∧ ((𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))‘1) = (𝐹‘1))))
146	98, 100, 144, 145	mpbir3and 1245	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹)) ∈ ∪ (Base‘𝑄))
147	16, 125, 118, 126, 127, 141, 146	pi1addval 22848	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ([(𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹))]( ≃_ph‘𝐽)(+_g‘𝑄)[(𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))]( ≃_ph‘𝐽)) = [((𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹))(_𝑝‘𝐽)(𝐼(_𝑝‘𝐽)(ℎ(*_𝑝‘𝐽)𝐹)))]( ≃_ph‘𝐽))
148	117, 124, 147	3eqtr4d 2666	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐺‘[(𝑓(_𝑝‘𝐽)ℎ)]( ≃_ph‘𝐽)) = ([(𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹))]( ≃_ph‘𝐽)(+_g‘𝑄)[(𝐼(_𝑝‘𝐽)(ℎ(*_𝑝‘𝐽)𝐹))]( ≃_ph‘𝐽)))
149	9	3ad2ant1 1082	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐹‘0) ∈ 𝑋)
150		eqid 2622	. . . . . . . . . . . . 13 ⊢ (+_g‘𝑃) = (+_g‘𝑃)
151		simp2 1062	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → 𝑓 ∈ ∪ 𝐵)
152		simp3 1063	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ℎ ∈ ∪ 𝐵)
153	10, 20, 118, 149, 150, 151, 152	pi1addval 22848	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ([𝑓]( ≃_ph‘𝐽)(+_g‘𝑃)[ℎ]( ≃_ph‘𝐽)) = [(𝑓(*_𝑝‘𝐽)ℎ)]( ≃_ph‘𝐽))
154	153	fveq2d 6195	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐺‘([𝑓]( ≃_ph‘𝐽)(+_g‘𝑃)[ℎ]( ≃_ph‘𝐽))) = (𝐺‘[(𝑓(*_𝑝‘𝐽)ℎ)]( ≃_ph‘𝐽)))
155	1	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → 𝐽 ∈ (TopOn‘𝑋))
156	27	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (𝐹‘1) = (𝐼‘0))
157		simpr 477	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → 𝑓 ∈ ∪ 𝐵)
158	10, 16, 20, 21, 155, 106, 128, 156, 110, 157	pi1xfrval 22854	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → (𝐺‘[𝑓]( ≃_ph‘𝐽)) = [(𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹))]( ≃_ph‘𝐽))
159	158	3adant3 1081	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐺‘[𝑓]( ≃_ph‘𝐽)) = [(𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹))]( ≃_ph‘𝐽))
160	10, 16, 20, 21, 118, 68, 72, 94, 70, 152	pi1xfrval 22854	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐺‘[ℎ]( ≃_ph‘𝐽)) = [(𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))]( ≃_ph‘𝐽))
161	159, 160	oveq12d 6668	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → ((𝐺‘[𝑓]( ≃_ph‘𝐽))(+_g‘𝑄)(𝐺‘[ℎ]( ≃_ph‘𝐽))) = ([(𝐼(_𝑝‘𝐽)(𝑓(_𝑝‘𝐽)𝐹))]( ≃_ph‘𝐽)(+_g‘𝑄)[(𝐼(_𝑝‘𝐽)(ℎ(_𝑝‘𝐽)𝐹))]( ≃_ph‘𝐽)))
162	148, 154, 161	3eqtr4d 2666	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵 ∧ ℎ ∈ ∪ 𝐵) → (𝐺‘([𝑓]( ≃_ph‘𝐽)(+_g‘𝑃)[ℎ]( ≃_ph‘𝐽))) = ((𝐺‘[𝑓]( ≃_ph‘𝐽))(+_g‘𝑄)(𝐺‘[ℎ]( ≃_ph‘𝐽))))
163	162	3expa 1265	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) ∧ ℎ ∈ ∪ 𝐵) → (𝐺‘([𝑓]( ≃_ph‘𝐽)(+_g‘𝑃)[ℎ]( ≃_ph‘𝐽))) = ((𝐺‘[𝑓]( ≃_ph‘𝐽))(+_g‘𝑄)(𝐺‘[ℎ]( ≃_ph‘𝐽))))
164	34, 48, 163	ectocld 7814	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) ∧ 𝑧 ∈ (∪ 𝐵 / ( ≃_ph‘𝐽))) → (𝐺‘([𝑓]( ≃_ph‘𝐽)(+_g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃_ph‘𝐽))(+_g‘𝑄)(𝐺‘𝑧)))
165	43, 164	syldan 487	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝐺‘([𝑓]( ≃_ph‘𝐽)(+_g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃_ph‘𝐽))(+_g‘𝑄)(𝐺‘𝑧)))
166	165	ralrimiva 2966	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ ∪ 𝐵) → ∀𝑧 ∈ 𝐵 (𝐺‘([𝑓]( ≃_ph‘𝐽)(+_g‘𝑃)𝑧)) = ((𝐺‘[𝑓]( ≃_ph‘𝐽))(+_g‘𝑄)(𝐺‘𝑧)))
167	34, 40, 166	ectocld 7814	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (∪ 𝐵 / ( ≃_ph‘𝐽))) → ∀𝑧 ∈ 𝐵 (𝐺‘(𝑦(+_g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+_g‘𝑄)(𝐺‘𝑧)))
168	33, 167	syldan 487	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐵 (𝐺‘(𝑦(+_g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+_g‘𝑄)(𝐺‘𝑧)))
169	168	ralrimiva 2966	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝐺‘(𝑦(+_g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+_g‘𝑄)(𝐺‘𝑧)))
170	29, 169	jca 554	. 2 ⊢ (𝜑 → (𝐺:𝐵⟶(Base‘𝑄) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝐺‘(𝑦(+_g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+_g‘𝑄)(𝐺‘𝑧))))
171	20, 125, 150, 127	isghm 17660	. 2 ⊢ (𝐺 ∈ (𝑃 GrpHom 𝑄) ↔ ((𝑃 ∈ Grp ∧ 𝑄 ∈ Grp) ∧ (𝐺:𝐵⟶(Base‘𝑄) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝐺‘(𝑦(+_g‘𝑃)𝑧)) = ((𝐺‘𝑦)(+_g‘𝑄)(𝐺‘𝑧)))))
172	19, 170, 171	sylanbrc 698	1 ⊢ (𝜑 → 𝐺 ∈ (𝑃 GrpHom 𝑄))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ∀wral 2912 ifcif 4086 {csn 4177 ⟨cop 4183 ∪ cuni 4436 class class class wbr 4653 ↦ cmpt 4729 × cxp 5112 ran crn 5115 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 Er wer 7739 [cec 7740 / cqs 7741 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 ≤ cle 10075 − cmin 10266 / cdiv 10684 2c2 11070 4c4 11072 [,]cicc 12178 Basecbs 15857 +_gcplusg 15941 Grpcgrp 17422 GrpHom cghm 17657 TopOnctopon 20715 Cn ccn 21028 IIcii 22678 ≃_phcphtpc 22768 *_𝑝cpco 22800 π₁ cpi1 22803

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-ec 7744 df-qs 7748 df-map 7859 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-icc 12182 df-fz 12327 df-fzo 12466 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-qus 16169 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-grp 17425 df-mulg 17541 df-ghm 17658 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-cn 21031 df-cnp 21032 df-tx 21365 df-hmeo 21558 df-xms 22125 df-ms 22126 df-tms 22127 df-ii 22680 df-htpy 22769 df-phtpy 22770 df-phtpc 22791 df-pco 22805 df-om1 22806 df-pi1 22808

This theorem is referenced by: pi1xfrcnv 22857 pi1xfrgim 22858

W3C validator