Metamath Proof Explorer

Theorem nsgmgc

Description: There is a monotone Galois connection between the lattice of subgroups of a group G containing a normal subgroup N and the lattice of subgroups of the quotient group G / N . This is sometimes called the lattice theorem. (Contributed by Thierry Arnoux, 27-Jul-2024)

Ref Expression
Hypotheses nsgmgc.b 
|- B = ( Base ` G )
nsgmgc.s 
|- S = { h e. ( SubGrp ` G ) | N C_ h }
nsgmgc.t 
|- T = ( SubGrp ` Q )
nsgmgc.j 
|- J = ( V MGalConn W )
nsgmgc.v 
|- V = ( toInc ` S )
nsgmgc.w 
|- W = ( toInc ` T )
nsgmgc.q 
|- Q = ( G /s ( G ~QG N ) )
nsgmgc.p 
|- .(+) = ( LSSum ` G )
nsgmgc.e 
|- E = ( h e. S |-> ran ( x e. h |-> ( { x } .(+) N ) ) )
nsgmgc.f 
|- F = ( f e. T |-> { a e. B | ( { a } .(+) N ) e. f } )
nsgmgc.n 
|- ( ph -> N e. ( NrmSGrp ` G ) )
Assertion nsgmgc 
|- ( ph -> E J F )

Proof

Step Hyp Ref Expression
1 nsgmgc.b 
 |-  B = ( Base ` G )
2 nsgmgc.s 
 |-  S = { h e. ( SubGrp ` G ) | N C_ h }
3 nsgmgc.t 
 |-  T = ( SubGrp ` Q )
4 nsgmgc.j 
 |-  J = ( V MGalConn W )
5 nsgmgc.v 
 |-  V = ( toInc ` S )
6 nsgmgc.w 
 |-  W = ( toInc ` T )
7 nsgmgc.q 
 |-  Q = ( G /s ( G ~QG N ) )
8 nsgmgc.p 
 |-  .(+) = ( LSSum ` G )
9 nsgmgc.e 
 |-  E = ( h e. S |-> ran ( x e. h |-> ( { x } .(+) N ) ) )
10 nsgmgc.f 
 |-  F = ( f e. T |-> { a e. B | ( { a } .(+) N ) e. f } )
11 nsgmgc.n 
 |-  ( ph -> N e. ( NrmSGrp ` G ) )
12 nfv 
 |-  F/ h ph
13 vex 
 |-  h e. _V
14 13 mptex 
 |-  ( x e. h |-> ( { x } .(+) N ) ) e. _V
15 14 rnex 
 |-  ran ( x e. h |-> ( { x } .(+) N ) ) e. _V
16 15 a1i 
 |-  ( ( ph /\ h e. S ) -> ran ( x e. h |-> ( { x } .(+) N ) ) e. _V )
17 12 16 9 fnmptd 
 |-  ( ph -> E Fn S )
18 mpteq1 
 |-  ( h = k -> ( x e. h |-> ( { x } .(+) N ) ) = ( x e. k |-> ( { x } .(+) N ) ) )
19 18 rneqd 
 |-  ( h = k -> ran ( x e. h |-> ( { x } .(+) N ) ) = ran ( x e. k |-> ( { x } .(+) N ) ) )
20 19 cbvmptv 
 |-  ( h e. S |-> ran ( x e. h |-> ( { x } .(+) N ) ) ) = ( k e. S |-> ran ( x e. k |-> ( { x } .(+) N ) ) )
21 9 20 eqtri 
 |-  E = ( k e. S |-> ran ( x e. k |-> ( { x } .(+) N ) ) )
22 eqid 
 |-  ( x e. B |-> [ x ] ( G ~QG N ) ) = ( x e. B |-> [ x ] ( G ~QG N ) )
23 11 adantr 
 |-  ( ( ph /\ h e. S ) -> N e. ( NrmSGrp ` G ) )
24 simpr 
 |-  ( ( ph /\ h e. S ) -> h e. S )
25 2 ssrab3 
 |-  S C_ ( SubGrp ` G )
26 25 a1i 
 |-  ( ( ph /\ h e. S ) -> S C_ ( SubGrp ` G ) )
27 1 7 8 21 22 23 24 26 qusima 
 |-  ( ( ph /\ h e. S ) -> ( E ` h ) = ( ( x e. B |-> [ x ] ( G ~QG N ) ) " h ) )
28 1 7 22 qusghm 
 |-  ( N e. ( NrmSGrp ` G ) -> ( x e. B |-> [ x ] ( G ~QG N ) ) e. ( G GrpHom Q ) )
29 23 28 syl 
 |-  ( ( ph /\ h e. S ) -> ( x e. B |-> [ x ] ( G ~QG N ) ) e. ( G GrpHom Q ) )
30 25 a1i 
 |-  ( ph -> S C_ ( SubGrp ` G ) )
31 30 sselda 
 |-  ( ( ph /\ h e. S ) -> h e. ( SubGrp ` G ) )
32 ghmima 
 |-  ( ( ( x e. B |-> [ x ] ( G ~QG N ) ) e. ( G GrpHom Q ) /\ h e. ( SubGrp ` G ) ) -> ( ( x e. B |-> [ x ] ( G ~QG N ) ) " h ) e. ( SubGrp ` Q ) )
33 29 31 32 syl2anc 
 |-  ( ( ph /\ h e. S ) -> ( ( x e. B |-> [ x ] ( G ~QG N ) ) " h ) e. ( SubGrp ` Q ) )
34 27 33 eqeltrd 
 |-  ( ( ph /\ h e. S ) -> ( E ` h ) e. ( SubGrp ` Q ) )
35 34 3 eleqtrrdi 
 |-  ( ( ph /\ h e. S ) -> ( E ` h ) e. T )
36 35 ralrimiva 
 |-  ( ph -> A. h e. S ( E ` h ) e. T )
37 ffnfv 
 |-  ( E : S --> T <-> ( E Fn S /\ A. h e. S ( E ` h ) e. T ) )
38 17 36 37 sylanbrc 
 |-  ( ph -> E : S --> T )
39 sseq2 
 |-  ( h = { a e. B | ( { a } .(+) N ) e. f } -> ( N C_ h <-> N C_ { a e. B | ( { a } .(+) N ) e. f } ) )
40 11 adantr 
 |-  ( ( ph /\ f e. T ) -> N e. ( NrmSGrp ` G ) )
41 simpr 
 |-  ( ( ph /\ f e. T ) -> f e. T )
42 41 3 eleqtrdi 
 |-  ( ( ph /\ f e. T ) -> f e. ( SubGrp ` Q ) )
43 1 7 8 40 42 nsgmgclem 
 |-  ( ( ph /\ f e. T ) -> { a e. B | ( { a } .(+) N ) e. f } e. ( SubGrp ` G ) )
44 nsgsubg 
 |-  ( N e. ( NrmSGrp ` G ) -> N e. ( SubGrp ` G ) )
45 11 44 syl 
 |-  ( ph -> N e. ( SubGrp ` G ) )
46 1 subgss 
 |-  ( N e. ( SubGrp ` G ) -> N C_ B )
47 45 46 syl 
 |-  ( ph -> N C_ B )
48 47 adantr 
 |-  ( ( ph /\ f e. T ) -> N C_ B )
49 45 ad2antrr 
 |-  ( ( ( ph /\ f e. T ) /\ a e. N ) -> N e. ( SubGrp ` G ) )
50 simpr 
 |-  ( ( ( ph /\ f e. T ) /\ a e. N ) -> a e. N )
51 8 grplsmid 
 |-  ( ( N e. ( SubGrp ` G ) /\ a e. N ) -> ( { a } .(+) N ) = N )
52 49 50 51 syl2anc 
 |-  ( ( ( ph /\ f e. T ) /\ a e. N ) -> ( { a } .(+) N ) = N )
53 11 ad2antrr 
 |-  ( ( ( ph /\ f e. T ) /\ a e. N ) -> N e. ( NrmSGrp ` G ) )
54 42 adantr 
 |-  ( ( ( ph /\ f e. T ) /\ a e. N ) -> f e. ( SubGrp ` Q ) )
55 7 nsgqus0 
 |-  ( ( N e. ( NrmSGrp ` G ) /\ f e. ( SubGrp ` Q ) ) -> N e. f )
56 53 54 55 syl2anc 
 |-  ( ( ( ph /\ f e. T ) /\ a e. N ) -> N e. f )
57 52 56 eqeltrd 
 |-  ( ( ( ph /\ f e. T ) /\ a e. N ) -> ( { a } .(+) N ) e. f )
58 48 57 ssrabdv 
 |-  ( ( ph /\ f e. T ) -> N C_ { a e. B | ( { a } .(+) N ) e. f } )
59 39 43 58 elrabd 
 |-  ( ( ph /\ f e. T ) -> { a e. B | ( { a } .(+) N ) e. f } e. { h e. ( SubGrp ` G ) | N C_ h } )
60 59 2 eleqtrrdi 
 |-  ( ( ph /\ f e. T ) -> { a e. B | ( { a } .(+) N ) e. f } e. S )
61 60 10 fmptd 
 |-  ( ph -> F : T --> S )
62 38 61 jca 
 |-  ( ph -> ( E : S --> T /\ F : T --> S ) )
63 1 subgss 
 |-  ( h e. ( SubGrp ` G ) -> h C_ B )
64 31 63 syl 
 |-  ( ( ph /\ h e. S ) -> h C_ B )
65 64 ad2antrr 
 |-  ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ ( E ` h ) C_ f ) -> h C_ B )
66 9 fvmpt2 
 |-  ( ( h e. S /\ ran ( x e. h |-> ( { x } .(+) N ) ) e. _V ) -> ( E ` h ) = ran ( x e. h |-> ( { x } .(+) N ) ) )
67 24 15 66 sylancl 
 |-  ( ( ph /\ h e. S ) -> ( E ` h ) = ran ( x e. h |-> ( { x } .(+) N ) ) )
68 67 ad5ant12 
 |-  ( ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ ( E ` h ) C_ f ) /\ a e. h ) -> ( E ` h ) = ran ( x e. h |-> ( { x } .(+) N ) ) )
69 simplr 
 |-  ( ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ ( E ` h ) C_ f ) /\ a e. h ) -> ( E ` h ) C_ f )
70 68 69 eqsstrrd 
 |-  ( ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ ( E ` h ) C_ f ) /\ a e. h ) -> ran ( x e. h |-> ( { x } .(+) N ) ) C_ f )
71 eqid 
 |-  ( x e. h |-> ( { x } .(+) N ) ) = ( x e. h |-> ( { x } .(+) N ) )
72 simpr 
 |-  ( ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ ( E ` h ) C_ f ) /\ a e. h ) -> a e. h )
73 sneq 
 |-  ( x = a -> { x } = { a } )
74 73 oveq1d 
 |-  ( x = a -> ( { x } .(+) N ) = ( { a } .(+) N ) )
75 74 eqeq2d 
 |-  ( x = a -> ( ( { a } .(+) N ) = ( { x } .(+) N ) <-> ( { a } .(+) N ) = ( { a } .(+) N ) ) )
76 75 adantl 
 |-  ( ( ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ ( E ` h ) C_ f ) /\ a e. h ) /\ x = a ) -> ( ( { a } .(+) N ) = ( { x } .(+) N ) <-> ( { a } .(+) N ) = ( { a } .(+) N ) ) )
77 eqidd 
 |-  ( ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ ( E ` h ) C_ f ) /\ a e. h ) -> ( { a } .(+) N ) = ( { a } .(+) N ) )
78 72 76 77 rspcedvd 
 |-  ( ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ ( E ` h ) C_ f ) /\ a e. h ) -> E. x e. h ( { a } .(+) N ) = ( { x } .(+) N ) )
79 ovexd 
 |-  ( ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ ( E ` h ) C_ f ) /\ a e. h ) -> ( { a } .(+) N ) e. _V )
80 71 78 79 elrnmptd 
 |-  ( ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ ( E ` h ) C_ f ) /\ a e. h ) -> ( { a } .(+) N ) e. ran ( x e. h |-> ( { x } .(+) N ) ) )
81 70 80 sseldd 
 |-  ( ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ ( E ` h ) C_ f ) /\ a e. h ) -> ( { a } .(+) N ) e. f )
82 65 81 ssrabdv 
 |-  ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ ( E ` h ) C_ f ) -> h C_ { a e. B | ( { a } .(+) N ) e. f } )
83 simpr 
 |-  ( ( ( ph /\ h e. S ) /\ f e. T ) -> f e. T )
84 1 fvexi 
 |-  B e. _V
85 84 rabex 
 |-  { a e. B | ( { a } .(+) N ) e. f } e. _V
86 10 fvmpt2 
 |-  ( ( f e. T /\ { a e. B | ( { a } .(+) N ) e. f } e. _V ) -> ( F ` f ) = { a e. B | ( { a } .(+) N ) e. f } )
87 83 85 86 sylancl 
 |-  ( ( ( ph /\ h e. S ) /\ f e. T ) -> ( F ` f ) = { a e. B | ( { a } .(+) N ) e. f } )
88 87 adantr 
 |-  ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ ( E ` h ) C_ f ) -> ( F ` f ) = { a e. B | ( { a } .(+) N ) e. f } )
89 82 88 sseqtrrd 
 |-  ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ ( E ` h ) C_ f ) -> h C_ ( F ` f ) )
90 67 ad2antrr 
 |-  ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ h C_ ( F ` f ) ) -> ( E ` h ) = ran ( x e. h |-> ( { x } .(+) N ) ) )
91 simpr 
 |-  ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ h C_ ( F ` f ) ) -> h C_ ( F ` f ) )
92 91 sselda 
 |-  ( ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ h C_ ( F ` f ) ) /\ x e. h ) -> x e. ( F ` f ) )
93 87 ad2antrr 
 |-  ( ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ h C_ ( F ` f ) ) /\ x e. h ) -> ( F ` f ) = { a e. B | ( { a } .(+) N ) e. f } )
94 92 93 eleqtrd 
 |-  ( ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ h C_ ( F ` f ) ) /\ x e. h ) -> x e. { a e. B | ( { a } .(+) N ) e. f } )
95 sneq 
 |-  ( a = x -> { a } = { x } )
96 95 oveq1d 
 |-  ( a = x -> ( { a } .(+) N ) = ( { x } .(+) N ) )
97 96 eleq1d 
 |-  ( a = x -> ( ( { a } .(+) N ) e. f <-> ( { x } .(+) N ) e. f ) )
98 97 elrab 
 |-  ( x e. { a e. B | ( { a } .(+) N ) e. f } <-> ( x e. B /\ ( { x } .(+) N ) e. f ) )
99 98 simprbi 
 |-  ( x e. { a e. B | ( { a } .(+) N ) e. f } -> ( { x } .(+) N ) e. f )
100 94 99 syl 
 |-  ( ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ h C_ ( F ` f ) ) /\ x e. h ) -> ( { x } .(+) N ) e. f )
101 100 ralrimiva 
 |-  ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ h C_ ( F ` f ) ) -> A. x e. h ( { x } .(+) N ) e. f )
102 71 rnmptss 
 |-  ( A. x e. h ( { x } .(+) N ) e. f -> ran ( x e. h |-> ( { x } .(+) N ) ) C_ f )
103 101 102 syl 
 |-  ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ h C_ ( F ` f ) ) -> ran ( x e. h |-> ( { x } .(+) N ) ) C_ f )
104 90 103 eqsstrd 
 |-  ( ( ( ( ph /\ h e. S ) /\ f e. T ) /\ h C_ ( F ` f ) ) -> ( E ` h ) C_ f )
105 89 104 impbida 
 |-  ( ( ( ph /\ h e. S ) /\ f e. T ) -> ( ( E ` h ) C_ f <-> h C_ ( F ` f ) ) )
106 3 fvexi 
 |-  T e. _V
107 eqid 
 |-  ( le ` W ) = ( le ` W )
108 6 107 ipole 
 |-  ( ( T e. _V /\ ( E ` h ) e. T /\ f e. T ) -> ( ( E ` h ) ( le ` W ) f <-> ( E ` h ) C_ f ) )
109 106 35 83 108 mp3an2ani 
 |-  ( ( ( ph /\ h e. S ) /\ f e. T ) -> ( ( E ` h ) ( le ` W ) f <-> ( E ` h ) C_ f ) )
110 fvex 
 |-  ( SubGrp ` G ) e. _V
111 2 110 rabex2 
 |-  S e. _V
112 61 ffvelcdmda 
 |-  ( ( ph /\ f e. T ) -> ( F ` f ) e. S )
113 112 adantlr 
 |-  ( ( ( ph /\ h e. S ) /\ f e. T ) -> ( F ` f ) e. S )
114 eqid 
 |-  ( le ` V ) = ( le ` V )
115 5 114 ipole 
 |-  ( ( S e. _V /\ h e. S /\ ( F ` f ) e. S ) -> ( h ( le ` V ) ( F ` f ) <-> h C_ ( F ` f ) ) )
116 111 24 113 115 mp3an2ani 
 |-  ( ( ( ph /\ h e. S ) /\ f e. T ) -> ( h ( le ` V ) ( F ` f ) <-> h C_ ( F ` f ) ) )
117 105 109 116 3bitr4d 
 |-  ( ( ( ph /\ h e. S ) /\ f e. T ) -> ( ( E ` h ) ( le ` W ) f <-> h ( le ` V ) ( F ` f ) ) )
118 117 anasss 
 |-  ( ( ph /\ ( h e. S /\ f e. T ) ) -> ( ( E ` h ) ( le ` W ) f <-> h ( le ` V ) ( F ` f ) ) )
119 118 ralrimivva 
 |-  ( ph -> A. h e. S A. f e. T ( ( E ` h ) ( le ` W ) f <-> h ( le ` V ) ( F ` f ) ) )
120 5 ipobas 
 |-  ( S e. _V -> S = ( Base ` V ) )
121 111 120 ax-mp 
 |-  S = ( Base ` V )
122 6 ipobas 
 |-  ( T e. _V -> T = ( Base ` W ) )
123 106 122 ax-mp 
 |-  T = ( Base ` W )
124 5 ipopos 
 |-  V e. Poset
125 posprs 
 |-  ( V e. Poset -> V e. Proset )
126 124 125 mp1i 
 |-  ( ph -> V e. Proset )
127 6 ipopos 
 |-  W e. Poset
128 posprs 
 |-  ( W e. Poset -> W e. Proset )
129 127 128 mp1i 
 |-  ( ph -> W e. Proset )
130 121 123 114 107 4 126 129 mgcval 
 |-  ( ph -> ( E J F <-> ( ( E : S --> T /\ F : T --> S ) /\ A. h e. S A. f e. T ( ( E ` h ) ( le ` W ) f <-> h ( le ` V ) ( F ` f ) ) ) ) )
131 62 119 130 mpbir2and 
 |-  ( ph -> E J F )