This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 reqabi 
 |-  ( 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 bitrid 
 |-  ( 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 )