nsgqusf1olem3

	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	nsgqusf1olem3	$⊢ φ \to ran F = S$

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	9	elrnmpt	$⊢ h \in V \to (h \in ran F \leftrightarrow \exists f \in T h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\})$
12	11	elv	$⊢ h \in ran F \leftrightarrow \exists f \in T h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}$
13	2	rabeq2i	$⊢ h \in S \leftrightarrow (h \in SubGrp (G) \land N \subseteq h)$
14	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$
15		eleq2	$⊢ f = ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \to (\{a\} \underset{˙}{\oplus} N \in f \leftrightarrow \{a\} \underset{˙}{\oplus} N \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N))$
16	15	rabbidv	$⊢ f = ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \to \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)\}$
17	16	eqeq2d	$⊢ f = ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \to (h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \leftrightarrow h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)\})$
18	17	adantl	$⊢ (((φ \land h \in SubGrp (G)) \land N \subseteq h) \land f = ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)) \to (h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \leftrightarrow h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)\})$
19		nfv	$⊢ Ⅎ x (((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B)$
20		nfmpt1	$⊢ \underline{Ⅎ} x (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
21	20	nfrn	$⊢ \underline{Ⅎ} x ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
22	21	nfel2	$⊢ Ⅎ x \{a\} \underset{˙}{\oplus} N \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
23	19 22	nfan	$⊢ Ⅎ x ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land \{a\} \underset{˙}{\oplus} N \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N))$
24		nsgsubg	$⊢ N \in NrmSGrp (G) \to N \in SubGrp (G)$
25	10 24	syl	$⊢ φ \to N \in SubGrp (G)$
26		subgrcl	$⊢ N \in SubGrp (G) \to G \in Grp$
27	25 26	syl	$⊢ φ \to G \in Grp$
28	27	ad4antr	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \to G \in Grp$
29	28	adantr	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \land \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N) \to G \in Grp$
30	1	subgss	$⊢ h \in SubGrp (G) \to h \subseteq B$
31	30	ad3antlr	$⊢ (((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \to h \subseteq B$
32	31	sselda	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \to x \in B$
33	32	adantr	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \land \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N) \to x \in B$
34		simplr	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \to a \in B$
35	34	adantr	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \land \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N) \to a \in B$
36		eqid	$⊢ +_{G} = +_{G}$
37		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
38	1 36 37	grpasscan1	$⊢ (G \in Grp \land x \in B \land a \in B) \to x +_{G} ({inv}_{g} (G) (x) +_{G} a) = a$
39	29 33 35 38	syl3anc	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \land \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N) \to x +_{G} ({inv}_{g} (G) (x) +_{G} a) = a$
40		simp-5r	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \land \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N) \to h \in SubGrp (G)$
41		simplr	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \land \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N) \to x \in h$
42		simp-4r	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \land \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N) \to N \subseteq h$
43	1	subgss	$⊢ N \in SubGrp (G) \to N \subseteq B$
44	25 43	syl	$⊢ φ \to N \subseteq B$
45	44	ad5antr	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \land \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N) \to N \subseteq B$
46		eqid	$⊢ G ~_{QG} N = G ~_{QG} N$
47	1 46	eqger	$⊢ N \in SubGrp (G) \to (G ~_{QG} N) Er B$
48	25 47	syl	$⊢ φ \to (G ~_{QG} N) Er B$
49	48	ad4antr	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \to (G ~_{QG} N) Er B$
50	49	adantr	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \land \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N) \to (G ~_{QG} N) Er B$
51	49 34	erth	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \to (a (G ~_{QG} N) x \leftrightarrow [a] (G ~_{QG} N) = [x] (G ~_{QG} N))$
52	25	ad4antr	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \to N \in SubGrp (G)$
53	1 7 52 34	quslsm	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \to [a] (G ~_{QG} N) = \{a\} \underset{˙}{\oplus} N$
54	1 7 52 32	quslsm	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \to [x] (G ~_{QG} N) = \{x\} \underset{˙}{\oplus} N$
55	53 54	eqeq12d	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \to ([a] (G ~_{QG} N) = [x] (G ~_{QG} N) \leftrightarrow \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N)$
56	51 55	bitrd	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \to (a (G ~_{QG} N) x \leftrightarrow \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N)$
57	56	biimpar	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \land \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N) \to a (G ~_{QG} N) x$
58	50 57	ersym	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \land \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N) \to x (G ~_{QG} N) a$
59	1 37 36 46	eqgval	$⊢ (G \in Grp \land N \subseteq B) \to (x (G ~_{QG} N) a \leftrightarrow (x \in B \land a \in B \land {inv}_{g} (G) (x) +_{G} a \in N))$
60	59	biimpa	$⊢ ((G \in Grp \land N \subseteq B) \land x (G ~_{QG} N) a) \to (x \in B \land a \in B \land {inv}_{g} (G) (x) +_{G} a \in N)$
61	60	simp3d	$⊢ ((G \in Grp \land N \subseteq B) \land x (G ~_{QG} N) a) \to {inv}_{g} (G) (x) +_{G} a \in N$
62	29 45 58 61	syl21anc	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \land \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N) \to {inv}_{g} (G) (x) +_{G} a \in N$
63	42 62	sseldd	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \land \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N) \to {inv}_{g} (G) (x) +_{G} a \in h$
64	36	subgcl	$⊢ (h \in SubGrp (G) \land x \in h \land {inv}_{g} (G) (x) +_{G} a \in h) \to x +_{G} ({inv}_{g} (G) (x) +_{G} a) \in h$
65	40 41 63 64	syl3anc	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \land \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N) \to x +_{G} ({inv}_{g} (G) (x) +_{G} a) \in h$
66	39 65	eqeltrrd	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land x \in h) \land \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N) \to a \in h$
67	66	adantllr	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land \{a\} \underset{˙}{\oplus} N \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)) \land x \in h) \land \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N) \to a \in h$
68		eqid	$⊢ (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) = (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
69		ovex	$⊢ \{x\} \underset{˙}{\oplus} N \in V$
70	68 69	elrnmpti	$⊢ \{a\} \underset{˙}{\oplus} N \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \leftrightarrow \exists x \in h \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N$
71	70	biimpi	$⊢ \{a\} \underset{˙}{\oplus} N \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \to \exists x \in h \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N$
72	71	adantl	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land \{a\} \underset{˙}{\oplus} N \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)) \to \exists x \in h \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N$
73	23 67 72	r19.29af	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land \{a\} \underset{˙}{\oplus} N \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)) \to a \in h$
74		simpr	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land a \in h) \to a \in h$
75		ovexd	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land a \in h) \to \{a\} \underset{˙}{\oplus} N \in V$
76		sneq	$⊢ x = a \to \{x\} = \{a\}$
77	76	oveq1d	$⊢ x = a \to \{x\} \underset{˙}{\oplus} N = \{a\} \underset{˙}{\oplus} N$
78	77	eqcomd	$⊢ x = a \to \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N$
79	78	adantl	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land a \in h) \land x = a) \to \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N$
80	68 74 75 79	elrnmptdv	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \land a \in h) \to \{a\} \underset{˙}{\oplus} N \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
81	73 80	impbida	$⊢ (((φ \land h \in SubGrp (G)) \land N \subseteq h) \land a \in B) \to (\{a\} \underset{˙}{\oplus} N \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \leftrightarrow a \in h)$
82	81	rabbidva	$⊢ ((φ \land h \in SubGrp (G)) \land N \subseteq h) \to \{a \in B \| \{a\} \underset{˙}{\oplus} N \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)\} = \{a \in B \| a \in h\}$
83	30	adantl	$⊢ (φ \land h \in SubGrp (G)) \to h \subseteq B$
84		dfss7	$⊢ h \subseteq B \leftrightarrow \{a \in B \| a \in h\} = h$
85	83 84	sylib	$⊢ (φ \land h \in SubGrp (G)) \to \{a \in B \| a \in h\} = h$
86	85	adantr	$⊢ ((φ \land h \in SubGrp (G)) \land N \subseteq h) \to \{a \in B \| a \in h\} = h$
87	82 86	eqtr2d	$⊢ ((φ \land h \in SubGrp (G)) \land N \subseteq h) \to h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)\}$
88	14 18 87	rspcedvd	$⊢ ((φ \land h \in SubGrp (G)) \land N \subseteq h) \to \exists f \in T h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}$
89	88	anasss	$⊢ (φ \land (h \in SubGrp (G) \land N \subseteq h)) \to \exists f \in T h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}$
90	10	adantr	$⊢ (φ \land f \in T) \to N \in NrmSGrp (G)$
91	3	eleq2i	$⊢ f \in T \leftrightarrow f \in SubGrp (Q)$
92	91	biimpi	$⊢ f \in T \to f \in SubGrp (Q)$
93	92	adantl	$⊢ (φ \land f \in T) \to f \in SubGrp (Q)$
94	1 6 7 90 93	nsgmgclem	$⊢ (φ \land f \in T) \to \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \in SubGrp (G)$
95	94	adantr	$⊢ ((φ \land f \in T) \land h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}) \to \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \in SubGrp (G)$
96		eleq1	$⊢ h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \to (h \in SubGrp (G) \leftrightarrow \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \in SubGrp (G))$
97	96	adantl	$⊢ ((φ \land f \in T) \land h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}) \to (h \in SubGrp (G) \leftrightarrow \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \in SubGrp (G))$
98	95 97	mpbird	$⊢ ((φ \land f \in T) \land h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}) \to h \in SubGrp (G)$
99	44	adantr	$⊢ (φ \land f \in T) \to N \subseteq B$
100	25	ad2antrr	$⊢ ((φ \land f \in T) \land a \in N) \to N \in SubGrp (G)$
101		simpr	$⊢ ((φ \land f \in T) \land a \in N) \to a \in N$
102	7	grplsmid	$⊢ (N \in SubGrp (G) \land a \in N) \to \{a\} \underset{˙}{\oplus} N = N$
103	100 101 102	syl2anc	$⊢ ((φ \land f \in T) \land a \in N) \to \{a\} \underset{˙}{\oplus} N = N$
104	6	nsgqus0	$⊢ (N \in NrmSGrp (G) \land f \in SubGrp (Q)) \to N \in f$
105	90 93 104	syl2anc	$⊢ (φ \land f \in T) \to N \in f$
106	105	adantr	$⊢ ((φ \land f \in T) \land a \in N) \to N \in f$
107	103 106	eqeltrd	$⊢ ((φ \land f \in T) \land a \in N) \to \{a\} \underset{˙}{\oplus} N \in f$
108	99 107	ssrabdv	$⊢ (φ \land f \in T) \to N \subseteq \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}$
109	108	adantr	$⊢ ((φ \land f \in T) \land h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}) \to N \subseteq \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}$
110		simpr	$⊢ ((φ \land f \in T) \land h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}) \to h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}$
111	109 110	sseqtrrd	$⊢ ((φ \land f \in T) \land h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}) \to N \subseteq h$
112	98 111	jca	$⊢ ((φ \land f \in T) \land h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}) \to (h \in SubGrp (G) \land N \subseteq h)$
113	112	r19.29an	$⊢ (φ \land \exists f \in T h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}) \to (h \in SubGrp (G) \land N \subseteq h)$
114	89 113	impbida	$⊢ φ \to ((h \in SubGrp (G) \land N \subseteq h) \leftrightarrow \exists f \in T h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\})$
115	13 114	syl5bb	$⊢ φ \to (h \in S \leftrightarrow \exists f \in T h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\})$
116	12 115	bitr4id	$⊢ φ \to (h \in ran F \leftrightarrow h \in S)$
117	116	eqrdv	$⊢ φ \to ran F = S$

Metamath Proof Explorer

Theorem nsgqusf1olem3

Proof