Theorem nsgqusf1olem3

Description: Lemma for nsgqusf1o . (Contributed by Thierry Arnoux, 4-Aug-2024)

	Ref	Expression
Hypotheses	nsgqusf1o.b	|- B = ( Base ` G )
	nsgqusf1o.s	|- S = { h e. ( SubGrp ` G ) | N C_ h }
	nsgqusf1o.t	|- T = ( SubGrp ` Q )
	nsgqusf1o.1	|- .<_ = ( le ` ( toInc ` S ) )
	nsgqusf1o.2	|- .c_ = ( le ` ( toInc ` T ) )
	nsgqusf1o.q	|- Q = ( G /s ( G ~QG N ) )
	nsgqusf1o.p	|- .(+) = ( LSSum ` G )
	nsgqusf1o.e	|- E = ( h e. S |-> ran ( x e. h |-> ( { x } .(+) N ) ) )
	nsgqusf1o.f	|- F = ( f e. T |-> { a e. B | ( { a } .(+) N ) e. f } )
	nsgqusf1o.n	|- ( ph -> N e. ( NrmSGrp ` G ) )
Assertion	nsgqusf1olem3	|- ( ph -> ran F = S )

Proof

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