ghmqusnsglem2

	Ref	Expression
Hypotheses	ghmqusnsg.0	$⊢ \underset{˙}{0} = 0_{H}$
	ghmqusnsg.f	$⊢ φ \to F \in (G GrpHom H)$
	ghmqusnsg.k	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
	ghmqusnsg.q	$⊢ Q = G /_{𝑠} (G ~_{QG} N)$
	ghmqusnsg.j	$⊢ J = (q \in {Base}_{Q} ⟼ ⋃ F [q])$
	ghmqusnsg.n	$⊢ φ \to N \subseteq K$
	ghmqusnsg.1	$⊢ φ \to N \in NrmSGrp (G)$
	ghmqusnsglem2.y	$⊢ φ \to Y \in {Base}_{Q}$
Assertion	ghmqusnsglem2	$⊢ φ \to \exists x \in Y J (Y) = F (x)$

Proof

Step	Hyp	Ref	Expression
1		ghmqusnsg.0	$⊢ \underset{˙}{0} = 0_{H}$
2		ghmqusnsg.f	$⊢ φ \to F \in (G GrpHom H)$
3		ghmqusnsg.k	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
4		ghmqusnsg.q	$⊢ Q = G /_{𝑠} (G ~_{QG} N)$
5		ghmqusnsg.j	$⊢ J = (q \in {Base}_{Q} ⟼ ⋃ F [q])$
6		ghmqusnsg.n	$⊢ φ \to N \subseteq K$
7		ghmqusnsg.1	$⊢ φ \to N \in NrmSGrp (G)$
8		ghmqusnsglem2.y	$⊢ φ \to Y \in {Base}_{Q}$
9	4	a1i	$⊢ φ \to Q = G /_{𝑠} (G ~_{QG} N)$
10		eqidd	$⊢ φ \to {Base}_{G} = {Base}_{G}$
11		ovexd	$⊢ φ \to G ~_{QG} N \in V$
12		ghmgrp1	$⊢ F \in (G GrpHom H) \to G \in Grp$
13	2 12	syl	$⊢ φ \to G \in Grp$
14	9 10 11 13	qusbas	$⊢ φ \to {Base}_{G} / (G ~_{QG} N) = {Base}_{Q}$
15	8 14	eleqtrrd	$⊢ φ \to Y \in ({Base}_{G} / (G ~_{QG} N))$
16		elqsg	$⊢ Y \in {Base}_{Q} \to (Y \in ({Base}_{G} / (G ~_{QG} N)) \leftrightarrow \exists x \in {Base}_{G} Y = [x] (G ~_{QG} N))$
17	16	biimpa	$⊢ (Y \in {Base}_{Q} \land Y \in ({Base}_{G} / (G ~_{QG} N))) \to \exists x \in {Base}_{G} Y = [x] (G ~_{QG} N)$
18	8 15 17	syl2anc	$⊢ φ \to \exists x \in {Base}_{G} Y = [x] (G ~_{QG} N)$
19		nsgsubg	$⊢ N \in NrmSGrp (G) \to N \in SubGrp (G)$
20		eqid	$⊢ {Base}_{G} = {Base}_{G}$
21		eqid	$⊢ G ~_{QG} N = G ~_{QG} N$
22	20 21	eqger	$⊢ N \in SubGrp (G) \to (G ~_{QG} N) Er {Base}_{G}$
23	7 19 22	3syl	$⊢ φ \to (G ~_{QG} N) Er {Base}_{G}$
24	23	ad2antrr	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} N)) \to (G ~_{QG} N) Er {Base}_{G}$
25		simplr	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} N)) \to x \in {Base}_{G}$
26		ecref	$⊢ ((G ~_{QG} N) Er {Base}_{G} \land x \in {Base}_{G}) \to x \in [x] (G ~_{QG} N)$
27	24 25 26	syl2anc	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} N)) \to x \in [x] (G ~_{QG} N)$
28		simpr	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} N)) \to Y = [x] (G ~_{QG} N)$
29	27 28	eleqtrrd	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} N)) \to x \in Y$
30	28	fveq2d	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} N)) \to J (Y) = J ([x] (G ~_{QG} N))$
31	2	ad2antrr	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} N)) \to F \in (G GrpHom H)$
32	6	ad2antrr	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} N)) \to N \subseteq K$
33	7	ad2antrr	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} N)) \to N \in NrmSGrp (G)$
34	1 31 3 4 5 32 33 25	ghmqusnsglem1	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} N)) \to J ([x] (G ~_{QG} N)) = F (x)$
35	30 34	eqtrd	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} N)) \to J (Y) = F (x)$
36	29 35	jca	$⊢ ((φ \land x \in {Base}_{G}) \land Y = [x] (G ~_{QG} N)) \to (x \in Y \land J (Y) = F (x))$
37	36	expl	$⊢ φ \to ((x \in {Base}_{G} \land Y = [x] (G ~_{QG} N)) \to (x \in Y \land J (Y) = F (x)))$
38	37	reximdv2	$⊢ φ \to (\exists x \in {Base}_{G} Y = [x] (G ~_{QG} N) \to \exists x \in Y J (Y) = F (x))$
39	18 38	mpd	$⊢ φ \to \exists x \in Y J (Y) = F (x)$

Metamath Proof Explorer

Theorem ghmqusnsglem2

Proof