Metamath Proof Explorer

Theorem nsgqusf1olem2

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 nsgqusf1olem2 
|- ( ph -> ran E = T )

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 simpr 
 |-  ( ( ( ph /\ h e. S ) /\ f = ran ( x e. h |-> ( { x } .(+) N ) ) ) -> f = ran ( x e. h |-> ( { x } .(+) N ) ) )
12 2 reqabi 
 |-  ( h e. S <-> ( h e. ( SubGrp ` G ) /\ N C_ h ) )
13 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 )
14 13 anasss 
 |-  ( ( ph /\ ( h e. ( SubGrp ` G ) /\ N C_ h ) ) -> ran ( x e. h |-> ( { x } .(+) N ) ) e. T )
15 14 3 eleqtrdi 
 |-  ( ( ph /\ ( h e. ( SubGrp ` G ) /\ N C_ h ) ) -> ran ( x e. h |-> ( { x } .(+) N ) ) e. ( SubGrp ` Q ) )
16 12 15 sylan2b 
 |-  ( ( ph /\ h e. S ) -> ran ( x e. h |-> ( { x } .(+) N ) ) e. ( SubGrp ` Q ) )
17 16 adantr 
 |-  ( ( ( ph /\ h e. S ) /\ f = ran ( x e. h |-> ( { x } .(+) N ) ) ) -> ran ( x e. h |-> ( { x } .(+) N ) ) e. ( SubGrp ` Q ) )
18 11 17 eqeltrd 
 |-  ( ( ( ph /\ h e. S ) /\ f = ran ( x e. h |-> ( { x } .(+) N ) ) ) -> f e. ( SubGrp ` Q ) )
19 18 r19.29an 
 |-  ( ( ph /\ E. h e. S f = ran ( x e. h |-> ( { x } .(+) N ) ) ) -> f e. ( SubGrp ` Q ) )
20 sseq2 
 |-  ( h = { a e. B | ( { a } .(+) N ) e. f } -> ( N C_ h <-> N C_ { a e. B | ( { a } .(+) N ) e. f } ) )
21 10 adantr 
 |-  ( ( ph /\ f e. ( SubGrp ` Q ) ) -> N e. ( NrmSGrp ` G ) )
22 simpr 
 |-  ( ( ph /\ f e. ( SubGrp ` Q ) ) -> f e. ( SubGrp ` Q ) )
23 1 6 7 21 22 nsgmgclem 
 |-  ( ( ph /\ f e. ( SubGrp ` Q ) ) -> { a e. B | ( { a } .(+) N ) e. f } e. ( SubGrp ` G ) )
24 3 eleq2i 
 |-  ( f e. T <-> f e. ( SubGrp ` Q ) )
25 nsgsubg 
 |-  ( N e. ( NrmSGrp ` G ) -> N e. ( SubGrp ` G ) )
26 10 25 syl 
 |-  ( ph -> N e. ( SubGrp ` G ) )
27 1 subgss 
 |-  ( N e. ( SubGrp ` G ) -> N C_ B )
28 26 27 syl 
 |-  ( ph -> N C_ B )
29 28 adantr 
 |-  ( ( ph /\ f e. T ) -> N C_ B )
30 26 ad2antrr 
 |-  ( ( ( ph /\ f e. T ) /\ a e. N ) -> N e. ( SubGrp ` G ) )
31 7 grplsmid 
 |-  ( ( N e. ( SubGrp ` G ) /\ a e. N ) -> ( { a } .(+) N ) = N )
32 30 31 sylancom 
 |-  ( ( ( ph /\ f e. T ) /\ a e. N ) -> ( { a } .(+) N ) = N )
33 24 biimpi 
 |-  ( f e. T -> f e. ( SubGrp ` Q ) )
34 6 nsgqus0 
 |-  ( ( N e. ( NrmSGrp ` G ) /\ f e. ( SubGrp ` Q ) ) -> N e. f )
35 10 33 34 syl2an 
 |-  ( ( ph /\ f e. T ) -> N e. f )
36 35 adantr 
 |-  ( ( ( ph /\ f e. T ) /\ a e. N ) -> N e. f )
37 32 36 eqeltrd 
 |-  ( ( ( ph /\ f e. T ) /\ a e. N ) -> ( { a } .(+) N ) e. f )
38 29 37 ssrabdv 
 |-  ( ( ph /\ f e. T ) -> N C_ { a e. B | ( { a } .(+) N ) e. f } )
39 24 38 sylan2br 
 |-  ( ( ph /\ f e. ( SubGrp ` Q ) ) -> N C_ { a e. B | ( { a } .(+) N ) e. f } )
40 20 23 39 elrabd 
 |-  ( ( ph /\ f e. ( SubGrp ` Q ) ) -> { a e. B | ( { a } .(+) N ) e. f } e. { h e. ( SubGrp ` G ) | N C_ h } )
41 40 2 eleqtrrdi 
 |-  ( ( ph /\ f e. ( SubGrp ` Q ) ) -> { a e. B | ( { a } .(+) N ) e. f } e. S )
42 mpteq1 
 |-  ( h = { a e. B | ( { a } .(+) N ) e. f } -> ( x e. h |-> ( { x } .(+) N ) ) = ( x e. { a e. B | ( { a } .(+) N ) e. f } |-> ( { x } .(+) N ) ) )
43 42 rneqd 
 |-  ( h = { a e. B | ( { a } .(+) N ) e. f } -> ran ( x e. h |-> ( { x } .(+) N ) ) = ran ( x e. { a e. B | ( { a } .(+) N ) e. f } |-> ( { x } .(+) N ) ) )
44 43 eqeq2d 
 |-  ( h = { a e. B | ( { a } .(+) N ) e. f } -> ( f = ran ( x e. h |-> ( { x } .(+) N ) ) <-> f = ran ( x e. { a e. B | ( { a } .(+) N ) e. f } |-> ( { x } .(+) N ) ) ) )
45 44 adantl 
 |-  ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ h = { a e. B | ( { a } .(+) N ) e. f } ) -> ( f = ran ( x e. h |-> ( { x } .(+) N ) ) <-> f = ran ( x e. { a e. B | ( { a } .(+) N ) e. f } |-> ( { x } .(+) N ) ) ) )
46 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
47 46 subgss 
 |-  ( f e. ( SubGrp ` Q ) -> f C_ ( Base ` Q ) )
48 47 adantl 
 |-  ( ( ph /\ f e. ( SubGrp ` Q ) ) -> f C_ ( Base ` Q ) )
49 48 sselda 
 |-  ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i e. f ) -> i e. ( Base ` Q ) )
50 6 a1i 
 |-  ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i e. f ) -> Q = ( G /s ( G ~QG N ) ) )
51 1 a1i 
 |-  ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i e. f ) -> B = ( Base ` G ) )
52 ovexd 
 |-  ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i e. f ) -> ( G ~QG N ) e. _V )
53 subgrcl 
 |-  ( N e. ( SubGrp ` G ) -> G e. Grp )
54 26 53 syl 
 |-  ( ph -> G e. Grp )
55 54 ad2antrr 
 |-  ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i e. f ) -> G e. Grp )
56 50 51 52 55 qusbas 
 |-  ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i e. f ) -> ( B /. ( G ~QG N ) ) = ( Base ` Q ) )
57 49 56 eleqtrrd 
 |-  ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i e. f ) -> i e. ( B /. ( G ~QG N ) ) )
58 elqsi 
 |-  ( i e. ( B /. ( G ~QG N ) ) -> E. x e. B i = [ x ] ( G ~QG N ) )
59 57 58 syl 
 |-  ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i e. f ) -> E. x e. B i = [ x ] ( G ~QG N ) )
60 sneq 
 |-  ( a = x -> { a } = { x } )
61 60 oveq1d 
 |-  ( a = x -> ( { a } .(+) N ) = ( { x } .(+) N ) )
62 61 eleq1d 
 |-  ( a = x -> ( ( { a } .(+) N ) e. f <-> ( { x } .(+) N ) e. f ) )
63 simplr 
 |-  ( ( ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i e. f ) /\ x e. B ) /\ i = [ x ] ( G ~QG N ) ) -> x e. B )
64 simpr 
 |-  ( ( ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i e. f ) /\ x e. B ) /\ i = [ x ] ( G ~QG N ) ) -> i = [ x ] ( G ~QG N ) )
65 26 ad4antr 
 |-  ( ( ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i e. f ) /\ x e. B ) /\ i = [ x ] ( G ~QG N ) ) -> N e. ( SubGrp ` G ) )
66 1 7 65 63 quslsm 
 |-  ( ( ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i e. f ) /\ x e. B ) /\ i = [ x ] ( G ~QG N ) ) -> [ x ] ( G ~QG N ) = ( { x } .(+) N ) )
67 64 66 eqtrd 
 |-  ( ( ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i e. f ) /\ x e. B ) /\ i = [ x ] ( G ~QG N ) ) -> i = ( { x } .(+) N ) )
68 simpllr 
 |-  ( ( ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i e. f ) /\ x e. B ) /\ i = [ x ] ( G ~QG N ) ) -> i e. f )
69 67 68 eqeltrrd 
 |-  ( ( ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i e. f ) /\ x e. B ) /\ i = [ x ] ( G ~QG N ) ) -> ( { x } .(+) N ) e. f )
70 62 63 69 elrabd 
 |-  ( ( ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i e. f ) /\ x e. B ) /\ i = [ x ] ( G ~QG N ) ) -> x e. { a e. B | ( { a } .(+) N ) e. f } )
71 70 67 jca 
 |-  ( ( ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i e. f ) /\ x e. B ) /\ i = [ x ] ( G ~QG N ) ) -> ( x e. { a e. B | ( { a } .(+) N ) e. f } /\ i = ( { x } .(+) N ) ) )
72 71 expl 
 |-  ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i e. f ) -> ( ( x e. B /\ i = [ x ] ( G ~QG N ) ) -> ( x e. { a e. B | ( { a } .(+) N ) e. f } /\ i = ( { x } .(+) N ) ) ) )
73 72 reximdv2 
 |-  ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i e. f ) -> ( E. x e. B i = [ x ] ( G ~QG N ) -> E. x e. { a e. B | ( { a } .(+) N ) e. f } i = ( { x } .(+) N ) ) )
74 59 73 mpd 
 |-  ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i e. f ) -> E. x e. { a e. B | ( { a } .(+) N ) e. f } i = ( { x } .(+) N ) )
75 simplr 
 |-  ( ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ x e. { a e. B | ( { a } .(+) N ) e. f } ) /\ i = ( { x } .(+) N ) ) -> x e. { a e. B | ( { a } .(+) N ) e. f } )
76 62 elrab 
 |-  ( x e. { a e. B | ( { a } .(+) N ) e. f } <-> ( x e. B /\ ( { x } .(+) N ) e. f ) )
77 75 76 sylib 
 |-  ( ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ x e. { a e. B | ( { a } .(+) N ) e. f } ) /\ i = ( { x } .(+) N ) ) -> ( x e. B /\ ( { x } .(+) N ) e. f ) )
78 simpllr 
 |-  ( ( ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i = ( { x } .(+) N ) ) /\ x e. B ) /\ ( { x } .(+) N ) e. f ) -> i = ( { x } .(+) N ) )
79 simpr 
 |-  ( ( ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i = ( { x } .(+) N ) ) /\ x e. B ) /\ ( { x } .(+) N ) e. f ) -> ( { x } .(+) N ) e. f )
80 78 79 eqeltrd 
 |-  ( ( ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i = ( { x } .(+) N ) ) /\ x e. B ) /\ ( { x } .(+) N ) e. f ) -> i e. f )
81 80 anasss 
 |-  ( ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ i = ( { x } .(+) N ) ) /\ ( x e. B /\ ( { x } .(+) N ) e. f ) ) -> i e. f )
82 81 adantllr 
 |-  ( ( ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ x e. { a e. B | ( { a } .(+) N ) e. f } ) /\ i = ( { x } .(+) N ) ) /\ ( x e. B /\ ( { x } .(+) N ) e. f ) ) -> i e. f )
83 77 82 mpdan 
 |-  ( ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ x e. { a e. B | ( { a } .(+) N ) e. f } ) /\ i = ( { x } .(+) N ) ) -> i e. f )
84 83 r19.29an 
 |-  ( ( ( ph /\ f e. ( SubGrp ` Q ) ) /\ E. x e. { a e. B | ( { a } .(+) N ) e. f } i = ( { x } .(+) N ) ) -> i e. f )
85 74 84 impbida 
 |-  ( ( ph /\ f e. ( SubGrp ` Q ) ) -> ( i e. f <-> E. x e. { a e. B | ( { a } .(+) N ) e. f } i = ( { x } .(+) N ) ) )
86 eqid 
 |-  ( x e. { a e. B | ( { a } .(+) N ) e. f } |-> ( { x } .(+) N ) ) = ( x e. { a e. B | ( { a } .(+) N ) e. f } |-> ( { x } .(+) N ) )
87 86 elrnmpt 
 |-  ( i e. _V -> ( i e. ran ( x e. { a e. B | ( { a } .(+) N ) e. f } |-> ( { x } .(+) N ) ) <-> E. x e. { a e. B | ( { a } .(+) N ) e. f } i = ( { x } .(+) N ) ) )
88 87 elv 
 |-  ( i e. ran ( x e. { a e. B | ( { a } .(+) N ) e. f } |-> ( { x } .(+) N ) ) <-> E. x e. { a e. B | ( { a } .(+) N ) e. f } i = ( { x } .(+) N ) )
89 85 88 bitr4di 
 |-  ( ( ph /\ f e. ( SubGrp ` Q ) ) -> ( i e. f <-> i e. ran ( x e. { a e. B | ( { a } .(+) N ) e. f } |-> ( { x } .(+) N ) ) ) )
90 89 eqrdv 
 |-  ( ( ph /\ f e. ( SubGrp ` Q ) ) -> f = ran ( x e. { a e. B | ( { a } .(+) N ) e. f } |-> ( { x } .(+) N ) ) )
91 41 45 90 rspcedvd 
 |-  ( ( ph /\ f e. ( SubGrp ` Q ) ) -> E. h e. S f = ran ( x e. h |-> ( { x } .(+) N ) ) )
92 19 91 impbida 
 |-  ( ph -> ( E. h e. S f = ran ( x e. h |-> ( { x } .(+) N ) ) <-> f e. ( SubGrp ` Q ) ) )
93 92 abbidv 
 |-  ( ph -> { f | E. h e. S f = ran ( x e. h |-> ( { x } .(+) N ) ) } = { f | f e. ( SubGrp ` Q ) } )
94 8 rnmpt 
 |-  ran E = { f | E. h e. S f = ran ( x e. h |-> ( { x } .(+) N ) ) }
95 abid1 
 |-  ( SubGrp ` Q ) = { f | f e. ( SubGrp ` Q ) }
96 93 94 95 3eqtr4g 
 |-  ( ph -> ran E = ( SubGrp ` Q ) )
97 96 3 eqtr4di 
 |-  ( ph -> ran E = T )