nsgqusf1olem2

	Ref	Expression
Hypotheses	nsgqusf1o.b	$⊢ B = {Base}_{G}$
	nsgqusf1o.s	$⊢ S = \{h \in SubGrp (G) \| N \subseteq h\}$
	nsgqusf1o.t	$⊢ T = SubGrp (Q)$
	nsgqusf1o.1	$⊢ \underset{˙}{\leq} = \leq_{toInc (S)}$
	nsgqusf1o.2	No typesetting found for \|- .c_ = ( le ` ( toInc ` T ) ) with typecode \|-
	nsgqusf1o.q	$⊢ Q = G /_{𝑠} (G ~_{QG} N)$
	nsgqusf1o.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	nsgqusf1o.e	$⊢ E = (h \in S ⟼ ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N))$
	nsgqusf1o.f	$⊢ F = (f \in T ⟼ \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\})$
	nsgqusf1o.n	$⊢ φ \to N \in NrmSGrp (G)$
Assertion	nsgqusf1olem2	$⊢ φ \to ran E = T$

Proof

Step	Hyp	Ref	Expression
1		nsgqusf1o.b	$⊢ B = {Base}_{G}$
2		nsgqusf1o.s	$⊢ S = \{h \in SubGrp (G) \| N \subseteq h\}$
3		nsgqusf1o.t	$⊢ T = SubGrp (Q)$
4		nsgqusf1o.1	$⊢ \underset{˙}{\leq} = \leq_{toInc (S)}$
5		nsgqusf1o.2	Could not format .c_ = ( le ` ( toInc ` T ) ) : No typesetting found for \|- .c_ = ( le ` ( toInc ` T ) ) with typecode \|-
6		nsgqusf1o.q	$⊢ Q = G /_{𝑠} (G ~_{QG} N)$
7		nsgqusf1o.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
8		nsgqusf1o.e	$⊢ E = (h \in S ⟼ ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N))$
9		nsgqusf1o.f	$⊢ F = (f \in T ⟼ \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\})$
10		nsgqusf1o.n	$⊢ φ \to N \in NrmSGrp (G)$
11		simpr	$⊢ ((φ \land h \in S) \land f = ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)) \to f = ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
12	2	rabeq2i	$⊢ h \in S \leftrightarrow (h \in SubGrp (G) \land N \subseteq h)$
13	1 2 3 4 5 6 7 8 9 10	nsgqusf1olem1	$⊢ ((φ \land h \in SubGrp (G)) \land N \subseteq h) \to ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \in T$
14	13	anasss	$⊢ (φ \land (h \in SubGrp (G) \land N \subseteq h)) \to ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \in T$
15	14 3	eleqtrdi	$⊢ (φ \land (h \in SubGrp (G) \land N \subseteq h)) \to ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \in SubGrp (Q)$
16	12 15	sylan2b	$⊢ (φ \land h \in S) \to ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \in SubGrp (Q)$
17	16	adantr	$⊢ ((φ \land h \in S) \land f = ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)) \to ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \in SubGrp (Q)$
18	11 17	eqeltrd	$⊢ ((φ \land h \in S) \land f = ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)) \to f \in SubGrp (Q)$
19	18	r19.29an	$⊢ (φ \land \exists h \in S f = ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)) \to f \in SubGrp (Q)$
20		sseq2	$⊢ h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \to (N \subseteq h \leftrightarrow N \subseteq \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\})$
21	10	adantr	$⊢ (φ \land f \in SubGrp (Q)) \to N \in NrmSGrp (G)$
22		simpr	$⊢ (φ \land f \in SubGrp (Q)) \to f \in SubGrp (Q)$
23	1 6 7 21 22	nsgmgclem	$⊢ (φ \land f \in SubGrp (Q)) \to \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \in SubGrp (G)$
24	3	eleq2i	$⊢ f \in T \leftrightarrow f \in SubGrp (Q)$
25		nsgsubg	$⊢ N \in NrmSGrp (G) \to N \in SubGrp (G)$
26	10 25	syl	$⊢ φ \to N \in SubGrp (G)$
27	1	subgss	$⊢ N \in SubGrp (G) \to N \subseteq B$
28	26 27	syl	$⊢ φ \to N \subseteq B$
29	28	adantr	$⊢ (φ \land f \in T) \to N \subseteq B$
30	26	ad2antrr	$⊢ ((φ \land f \in T) \land a \in N) \to N \in SubGrp (G)$
31	7	grplsmid	$⊢ (N \in SubGrp (G) \land a \in N) \to \{a\} \underset{˙}{\oplus} N = N$
32	30 31	sylancom	$⊢ ((φ \land f \in T) \land a \in N) \to \{a\} \underset{˙}{\oplus} N = N$
33	24	biimpi	$⊢ f \in T \to f \in SubGrp (Q)$
34	6	nsgqus0	$⊢ (N \in NrmSGrp (G) \land f \in SubGrp (Q)) \to N \in f$
35	10 33 34	syl2an	$⊢ (φ \land f \in T) \to N \in f$
36	35	adantr	$⊢ ((φ \land f \in T) \land a \in N) \to N \in f$
37	32 36	eqeltrd	$⊢ ((φ \land f \in T) \land a \in N) \to \{a\} \underset{˙}{\oplus} N \in f$
38	29 37	ssrabdv	$⊢ (φ \land f \in T) \to N \subseteq \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}$
39	24 38	sylan2br	$⊢ (φ \land f \in SubGrp (Q)) \to N \subseteq \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}$
40	20 23 39	elrabd	$⊢ (φ \land f \in SubGrp (Q)) \to \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \in \{h \in SubGrp (G) \| N \subseteq h\}$
41	40 2	eleqtrrdi	$⊢ (φ \land f \in SubGrp (Q)) \to \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \in S$
42		mpteq1	$⊢ h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \to (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) = (x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} ⟼ \{x\} \underset{˙}{\oplus} N)$
43	42	rneqd	$⊢ h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \to ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) = ran (x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} ⟼ \{x\} \underset{˙}{\oplus} N)$
44	43	eqeq2d	$⊢ h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \to (f = ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \leftrightarrow f = ran (x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} ⟼ \{x\} \underset{˙}{\oplus} N))$
45	44	adantl	$⊢ ((φ \land f \in SubGrp (Q)) \land h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}) \to (f = ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \leftrightarrow f = ran (x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} ⟼ \{x\} \underset{˙}{\oplus} N))$
46		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
47	46	subgss	$⊢ f \in SubGrp (Q) \to f \subseteq {Base}_{Q}$
48	47	adantl	$⊢ (φ \land f \in SubGrp (Q)) \to f \subseteq {Base}_{Q}$
49	48	sselda	$⊢ ((φ \land f \in SubGrp (Q)) \land i \in f) \to i \in {Base}_{Q}$
50	6	a1i	$⊢ ((φ \land f \in SubGrp (Q)) \land i \in f) \to Q = G /_{𝑠} (G ~_{QG} N)$
51	1	a1i	$⊢ ((φ \land f \in SubGrp (Q)) \land i \in f) \to B = {Base}_{G}$
52		ovexd	$⊢ ((φ \land f \in SubGrp (Q)) \land i \in f) \to G ~_{QG} N \in V$
53		subgrcl	$⊢ N \in SubGrp (G) \to G \in Grp$
54	26 53	syl	$⊢ φ \to G \in Grp$
55	54	ad2antrr	$⊢ ((φ \land f \in SubGrp (Q)) \land i \in f) \to G \in Grp$
56	50 51 52 55	qusbas	$⊢ ((φ \land f \in SubGrp (Q)) \land i \in f) \to B / (G ~_{QG} N) = {Base}_{Q}$
57	49 56	eleqtrrd	$⊢ ((φ \land f \in SubGrp (Q)) \land i \in f) \to i \in (B / (G ~_{QG} N))$
58		elqsi	$⊢ i \in (B / (G ~_{QG} N)) \to \exists x \in B i = [x] (G ~_{QG} N)$
59	57 58	syl	$⊢ ((φ \land f \in SubGrp (Q)) \land i \in f) \to \exists x \in B i = [x] (G ~_{QG} N)$
60		sneq	$⊢ a = x \to \{a\} = \{x\}$
61	60	oveq1d	$⊢ a = x \to \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N$
62	61	eleq1d	$⊢ a = x \to (\{a\} \underset{˙}{\oplus} N \in f \leftrightarrow \{x\} \underset{˙}{\oplus} N \in f)$
63		simplr	$⊢ ((((φ \land f \in SubGrp (Q)) \land i \in f) \land x \in B) \land i = [x] (G ~_{QG} N)) \to x \in B$
64		simpr	$⊢ ((((φ \land f \in SubGrp (Q)) \land i \in f) \land x \in B) \land i = [x] (G ~_{QG} N)) \to i = [x] (G ~_{QG} N)$
65	26	ad4antr	$⊢ ((((φ \land f \in SubGrp (Q)) \land i \in f) \land x \in B) \land i = [x] (G ~_{QG} N)) \to N \in SubGrp (G)$
66	1 7 65 63	quslsm	$⊢ ((((φ \land f \in SubGrp (Q)) \land i \in f) \land x \in B) \land i = [x] (G ~_{QG} N)) \to [x] (G ~_{QG} N) = \{x\} \underset{˙}{\oplus} N$
67	64 66	eqtrd	$⊢ ((((φ \land f \in SubGrp (Q)) \land i \in f) \land x \in B) \land i = [x] (G ~_{QG} N)) \to i = \{x\} \underset{˙}{\oplus} N$
68		simpllr	$⊢ ((((φ \land f \in SubGrp (Q)) \land i \in f) \land x \in B) \land i = [x] (G ~_{QG} N)) \to i \in f$
69	67 68	eqeltrrd	$⊢ ((((φ \land f \in SubGrp (Q)) \land i \in f) \land x \in B) \land i = [x] (G ~_{QG} N)) \to \{x\} \underset{˙}{\oplus} N \in f$
70	62 63 69	elrabd	$⊢ ((((φ \land f \in SubGrp (Q)) \land i \in f) \land x \in B) \land i = [x] (G ~_{QG} N)) \to x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}$
71	70 67	jca	$⊢ ((((φ \land f \in SubGrp (Q)) \land i \in f) \land x \in B) \land i = [x] (G ~_{QG} N)) \to (x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \land i = \{x\} \underset{˙}{\oplus} N)$
72	71	expl	$⊢ ((φ \land f \in SubGrp (Q)) \land i \in f) \to ((x \in B \land i = [x] (G ~_{QG} N)) \to (x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \land i = \{x\} \underset{˙}{\oplus} N))$
73	72	reximdv2	$⊢ ((φ \land f \in SubGrp (Q)) \land i \in f) \to (\exists x \in B i = [x] (G ~_{QG} N) \to \exists x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} i = \{x\} \underset{˙}{\oplus} N)$
74	59 73	mpd	$⊢ ((φ \land f \in SubGrp (Q)) \land i \in f) \to \exists x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} i = \{x\} \underset{˙}{\oplus} N$
75		simplr	$⊢ (((φ \land f \in SubGrp (Q)) \land x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}) \land i = \{x\} \underset{˙}{\oplus} N) \to x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}$
76	62	elrab	$⊢ x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \leftrightarrow (x \in B \land \{x\} \underset{˙}{\oplus} N \in f)$
77	75 76	sylib	$⊢ (((φ \land f \in SubGrp (Q)) \land x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}) \land i = \{x\} \underset{˙}{\oplus} N) \to (x \in B \land \{x\} \underset{˙}{\oplus} N \in f)$
78		simpllr	$⊢ ((((φ \land f \in SubGrp (Q)) \land i = \{x\} \underset{˙}{\oplus} N) \land x \in B) \land \{x\} \underset{˙}{\oplus} N \in f) \to i = \{x\} \underset{˙}{\oplus} N$
79		simpr	$⊢ ((((φ \land f \in SubGrp (Q)) \land i = \{x\} \underset{˙}{\oplus} N) \land x \in B) \land \{x\} \underset{˙}{\oplus} N \in f) \to \{x\} \underset{˙}{\oplus} N \in f$
80	78 79	eqeltrd	$⊢ ((((φ \land f \in SubGrp (Q)) \land i = \{x\} \underset{˙}{\oplus} N) \land x \in B) \land \{x\} \underset{˙}{\oplus} N \in f) \to i \in f$
81	80	anasss	$⊢ (((φ \land f \in SubGrp (Q)) \land i = \{x\} \underset{˙}{\oplus} N) \land (x \in B \land \{x\} \underset{˙}{\oplus} N \in f)) \to i \in f$
82	81	adantllr	$⊢ ((((φ \land f \in SubGrp (Q)) \land x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}) \land i = \{x\} \underset{˙}{\oplus} N) \land (x \in B \land \{x\} \underset{˙}{\oplus} N \in f)) \to i \in f$
83	77 82	mpdan	$⊢ (((φ \land f \in SubGrp (Q)) \land x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}) \land i = \{x\} \underset{˙}{\oplus} N) \to i \in f$
84	83	r19.29an	$⊢ ((φ \land f \in SubGrp (Q)) \land \exists x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} i = \{x\} \underset{˙}{\oplus} N) \to i \in f$
85	74 84	impbida	$⊢ (φ \land f \in SubGrp (Q)) \to (i \in f \leftrightarrow \exists x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} i = \{x\} \underset{˙}{\oplus} N)$
86		eqid	$⊢ (x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} ⟼ \{x\} \underset{˙}{\oplus} N) = (x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} ⟼ \{x\} \underset{˙}{\oplus} N)$
87	86	elrnmpt	$⊢ i \in V \to (i \in ran (x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} ⟼ \{x\} \underset{˙}{\oplus} N) \leftrightarrow \exists x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} i = \{x\} \underset{˙}{\oplus} N)$
88	87	elv	$⊢ i \in ran (x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} ⟼ \{x\} \underset{˙}{\oplus} N) \leftrightarrow \exists x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} i = \{x\} \underset{˙}{\oplus} N$
89	85 88	bitr4di	$⊢ (φ \land f \in SubGrp (Q)) \to (i \in f \leftrightarrow i \in ran (x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} ⟼ \{x\} \underset{˙}{\oplus} N))$
90	89	eqrdv	$⊢ (φ \land f \in SubGrp (Q)) \to f = ran (x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} ⟼ \{x\} \underset{˙}{\oplus} N)$
91	41 45 90	rspcedvd	$⊢ (φ \land f \in SubGrp (Q)) \to \exists h \in S f = ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
92	19 91	impbida	$⊢ φ \to (\exists h \in S f = ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \leftrightarrow f \in SubGrp (Q))$
93	92	abbidv	$⊢ φ \to \{f \| \exists h \in S f = ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)\} = \{f \| f \in SubGrp (Q)\}$
94	8	rnmpt	$⊢ ran E = \{f \| \exists h \in S f = ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)\}$
95		abid1	$⊢ SubGrp (Q) = \{f \| f \in SubGrp (Q)\}$
96	93 94 95	3eqtr4g	$⊢ φ \to ran E = SubGrp (Q)$
97	96 3	eqtr4di	$⊢ φ \to ran E = T$

Metamath Proof Explorer

Theorem nsgqusf1olem2

Proof