ghmquskerco

Description: In the case of theorem ghmqusker , the composition of the natural homomorphism L with the constructed homomorphism J equals the original homomorphism F . One says that F factors through Q . (Proposed by Saveliy Skresanov, 15-Feb-2025.) (Contributed by Thierry Arnoux, 15-Feb-2025)

	Ref	Expression
Hypotheses	ghmqusker.1	$⊢ \underset{˙}{0} = 0_{H}$
	ghmqusker.f	$⊢ φ \to F \in (G GrpHom H)$
	ghmqusker.k	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
	ghmqusker.q	$⊢ Q = G /_{𝑠} (G ~_{QG} K)$
	ghmqusker.j	$⊢ J = (q \in {Base}_{Q} ⟼ ⋃ F [q])$
	ghmquskerco.b	$⊢ B = {Base}_{G}$
	ghmquskerco.l	$⊢ L = (x \in B ⟼ [x] (G ~_{QG} K))$
Assertion	ghmquskerco	$⊢ φ \to F = J \circ L$

Proof

Step	Hyp	Ref	Expression
1		ghmqusker.1	$⊢ \underset{˙}{0} = 0_{H}$
2		ghmqusker.f	$⊢ φ \to F \in (G GrpHom H)$
3		ghmqusker.k	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
4		ghmqusker.q	$⊢ Q = G /_{𝑠} (G ~_{QG} K)$
5		ghmqusker.j	$⊢ J = (q \in {Base}_{Q} ⟼ ⋃ F [q])$
6		ghmquskerco.b	$⊢ B = {Base}_{G}$
7		ghmquskerco.l	$⊢ L = (x \in B ⟼ [x] (G ~_{QG} K))$
8		eqid	$⊢ {Base}_{H} = {Base}_{H}$
9	6 8	ghmf	$⊢ F \in (G GrpHom H) \to F : B ⟶ {Base}_{H}$
10	2 9	syl	$⊢ φ \to F : B ⟶ {Base}_{H}$
11	10	ffnd	$⊢ φ \to F Fn B$
12	2	adantr	$⊢ (φ \land x \in B) \to F \in (G GrpHom H)$
13	12	imaexd	$⊢ (φ \land x \in B) \to F [[x] (G ~_{QG} K)] \in V$
14	13	uniexd	$⊢ (φ \land x \in B) \to ⋃ F [[x] (G ~_{QG} K)] \in V$
15	14	ralrimiva	$⊢ φ \to \forall x \in B ⋃ F [[x] (G ~_{QG} K)] \in V$
16		eqid	$⊢ (x \in B ⟼ ⋃ F [[x] (G ~_{QG} K)]) = (x \in B ⟼ ⋃ F [[x] (G ~_{QG} K)])$
17	16	fnmpt	$⊢ \forall x \in B ⋃ F [[x] (G ~_{QG} K)] \in V \to (x \in B ⟼ ⋃ F [[x] (G ~_{QG} K)]) Fn B$
18	15 17	syl	$⊢ φ \to (x \in B ⟼ ⋃ F [[x] (G ~_{QG} K)]) Fn B$
19		ovex	$⊢ G ~_{QG} K \in V$
20	19	ecelqsi	$⊢ x \in B \to [x] (G ~_{QG} K) \in (B / (G ~_{QG} K))$
21	20	adantl	$⊢ (φ \land x \in B) \to [x] (G ~_{QG} K) \in (B / (G ~_{QG} K))$
22	4	a1i	$⊢ φ \to Q = G /_{𝑠} (G ~_{QG} K)$
23	6	a1i	$⊢ φ \to B = {Base}_{G}$
24		ovexd	$⊢ φ \to G ~_{QG} K \in V$
25		reldmghm	$⊢ Rel dom GrpHom$
26	25	ovrcl	$⊢ F \in (G GrpHom H) \to (G \in V \land H \in V)$
27	26	simpld	$⊢ F \in (G GrpHom H) \to G \in V$
28	2 27	syl	$⊢ φ \to G \in V$
29	22 23 24 28	qusbas	$⊢ φ \to B / (G ~_{QG} K) = {Base}_{Q}$
30	29	adantr	$⊢ (φ \land x \in B) \to B / (G ~_{QG} K) = {Base}_{Q}$
31	21 30	eleqtrd	$⊢ (φ \land x \in B) \to [x] (G ~_{QG} K) \in {Base}_{Q}$
32	7	a1i	$⊢ φ \to L = (x \in B ⟼ [x] (G ~_{QG} K))$
33	5	a1i	$⊢ φ \to J = (q \in {Base}_{Q} ⟼ ⋃ F [q])$
34		imaeq2	$⊢ q = [x] (G ~_{QG} K) \to F [q] = F [[x] (G ~_{QG} K)]$
35	34	unieqd	$⊢ q = [x] (G ~_{QG} K) \to ⋃ F [q] = ⋃ F [[x] (G ~_{QG} K)]$
36	31 32 33 35	fmptco	$⊢ φ \to J \circ L = (x \in B ⟼ ⋃ F [[x] (G ~_{QG} K)])$
37	36	fneq1d	$⊢ φ \to ((J \circ L) Fn B \leftrightarrow (x \in B ⟼ ⋃ F [[x] (G ~_{QG} K)]) Fn B)$
38	18 37	mpbird	$⊢ φ \to (J \circ L) Fn B$
39		ecexg	$⊢ G ~_{QG} K \in V \to [x] (G ~_{QG} K) \in V$
40	19 39	ax-mp	$⊢ [x] (G ~_{QG} K) \in V$
41	40 7	fnmpti	$⊢ L Fn B$
42		simpr	$⊢ (φ \land x \in B) \to x \in B$
43		fvco2	$⊢ (L Fn B \land x \in B) \to (J \circ L) (x) = J (L (x))$
44	41 42 43	sylancr	$⊢ (φ \land x \in B) \to (J \circ L) (x) = J (L (x))$
45	40	a1i	$⊢ (φ \land x \in B) \to [x] (G ~_{QG} K) \in V$
46	32 45	fvmpt2d	$⊢ (φ \land x \in B) \to L (x) = [x] (G ~_{QG} K)$
47	46	fveq2d	$⊢ (φ \land x \in B) \to J (L (x)) = J ([x] (G ~_{QG} K))$
48	42 6	eleqtrdi	$⊢ (φ \land x \in B) \to x \in {Base}_{G}$
49	1 12 3 4 5 48	ghmquskerlem1	$⊢ (φ \land x \in B) \to J ([x] (G ~_{QG} K)) = F (x)$
50	44 47 49	3eqtrrd	$⊢ (φ \land x \in B) \to F (x) = (J \circ L) (x)$
51	11 38 50	eqfnfvd	$⊢ φ \to F = J \circ L$

Metamath Proof Explorer

Theorem ghmquskerco

Proof