ghmquskerlem2

	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])$
	ghmquskerlem2.y	$⊢ φ \to Y \in {Base}_{Q}$
Assertion	ghmquskerlem2	$⊢ φ \to \exists x \in Y J (Y) = F (x)$

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		ghmquskerlem2.y	$⊢ φ \to Y \in {Base}_{Q}$
7	4	a1i	$⊢ φ \to Q = G /_{𝑠} (G ~_{QG} K)$
8		eqidd	$⊢ φ \to {Base}_{G} = {Base}_{G}$
9		ovexd	$⊢ φ \to G ~_{QG} K \in V$
10		ghmgrp1	$⊢ F \in (G GrpHom H) \to G \in Grp$
11	2 10	syl	$⊢ φ \to G \in Grp$
12	7 8 9 11	qusbas	$⊢ φ \to {Base}_{G} / (G ~_{QG} K) = {Base}_{Q}$
13	6 12	eleqtrrd	$⊢ φ \to Y \in ({Base}_{G} / (G ~_{QG} K))$
14		elqsg	$⊢ Y \in {Base}_{Q} \to (Y \in ({Base}_{G} / (G ~_{QG} K)) \leftrightarrow \exists x \in {Base}_{G} Y = [x] (G ~_{QG} K))$
15	14	biimpa	$⊢ (Y \in {Base}_{Q} \land Y \in ({Base}_{G} / (G ~_{QG} K))) \to \exists x \in {Base}_{G} Y = [x] (G ~_{QG} K)$
16	6 13 15	syl2anc	$⊢ φ \to \exists x \in {Base}_{G} Y = [x] (G ~_{QG} K)$
17	1	ghmker	$⊢ F \in (G GrpHom H) \to F^{-1} [\{\underset{˙}{0}\}] \in NrmSGrp (G)$
18		nsgsubg	$⊢ F^{-1} [\{\underset{˙}{0}\}] \in NrmSGrp (G) \to F^{-1} [\{\underset{˙}{0}\}] \in SubGrp (G)$
19	2 17 18	3syl	$⊢ φ \to F^{-1} [\{\underset{˙}{0}\}] \in SubGrp (G)$
20	3 19	eqeltrid	$⊢ φ \to K \in SubGrp (G)$
21		eqid	$⊢ {Base}_{G} = {Base}_{G}$
22		eqid	$⊢ G ~_{QG} K = G ~_{QG} K$
23	21 22	eqger	$⊢ K \in SubGrp (G) \to (G ~_{QG} K) Er {Base}_{G}$
24	20 23	syl	$⊢ φ \to (G ~_{QG} K) Er {Base}_{G}$
25	24	ad2antrr	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} K)) \to (G ~_{QG} K) Er {Base}_{G}$
26		simplr	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} K)) \to x \in {Base}_{G}$
27		ecref	$⊢ ((G ~_{QG} K) Er {Base}_{G} \land x \in {Base}_{G}) \to x \in [x] (G ~_{QG} K)$
28	25 26 27	syl2anc	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} K)) \to x \in [x] (G ~_{QG} K)$
29		simpr	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} K)) \to Y = [x] (G ~_{QG} K)$
30	28 29	eleqtrrd	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} K)) \to x \in Y$
31	29	fveq2d	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} K)) \to J (Y) = J ([x] (G ~_{QG} K))$
32	2	ad2antrr	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} K)) \to F \in (G GrpHom H)$
33	1 32 3 4 5 26	ghmquskerlem1	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} K)) \to J ([x] (G ~_{QG} K)) = F (x)$
34	31 33	eqtrd	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} K)) \to J (Y) = F (x)$
35	30 34	jca	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} K)) \to (x \in Y \land J (Y) = F (x))$
36	35	expl	$⊢ φ \to ((x \in {Base}_{G} \land Y = [x] (G ~_{QG} K)) \to (x \in Y \land J (Y) = F (x)))$
37	36	reximdv2	$⊢ φ \to (\exists x \in {Base}_{G} Y = [x] (G ~_{QG} K) \to \exists x \in Y J (Y) = F (x))$
38	16 37	mpd	$⊢ φ \to \exists x \in Y J (Y) = F (x)$

Metamath Proof Explorer

Theorem ghmquskerlem2

Proof