Metamath Proof Explorer

Theorem nsgqusf1o

Description: The canonical projection homomorphism E defines a bijective correspondence between the set S of subgroups of G containing a normal subgroup N and the subgroups of the quotient group G / N . This theorem is sometimes called the correspondence theorem, or the fourth isomorphism theorem. (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 nsgqusf1o 
|- ( ph -> E : S -1-1-onto-> 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 eqid 
 |-  ( ( toInc ` S ) MGalConn ( toInc ` T ) ) = ( ( toInc ` S ) MGalConn ( toInc ` T ) )
12 fvex 
 |-  ( SubGrp ` G ) e. _V
13 2 12 rabex2 
 |-  S e. _V
14 eqid 
 |-  ( toInc ` S ) = ( toInc ` S )
15 14 ipobas 
 |-  ( S e. _V -> S = ( Base ` ( toInc ` S ) ) )
16 13 15 ax-mp 
 |-  S = ( Base ` ( toInc ` S ) )
17 3 fvexi 
 |-  T e. _V
18 eqid 
 |-  ( toInc ` T ) = ( toInc ` T )
19 18 ipobas 
 |-  ( T e. _V -> T = ( Base ` ( toInc ` T ) ) )
20 17 19 ax-mp 
 |-  T = ( Base ` ( toInc ` T ) )
21 14 ipopos 
 |-  ( toInc ` S ) e. Poset
22 21 a1i 
 |-  ( ph -> ( toInc ` S ) e. Poset )
23 18 ipopos 
 |-  ( toInc ` T ) e. Poset
24 23 a1i 
 |-  ( ph -> ( toInc ` T ) e. Poset )
25 1 2 3 11 14 18 6 7 8 9 10 nsgmgc 
 |-  ( ph -> E ( ( toInc ` S ) MGalConn ( toInc ` T ) ) F )
26 11 16 20 4 5 22 24 25 mgcf1o 
 |-  ( ph -> ( E |` ran F ) Isom .<_ , .c_ ( ran F , ran E ) )
27 isof1o 
 |-  ( ( E |` ran F ) Isom .<_ , .c_ ( ran F , ran E ) -> ( E |` ran F ) : ran F -1-1-onto-> ran E )
28 26 27 syl 
 |-  ( ph -> ( E |` ran F ) : ran F -1-1-onto-> ran E )
29 1 2 3 4 5 6 7 8 9 10 nsgqusf1olem3 
 |-  ( ph -> ran F = S )
30 29 reseq2d 
 |-  ( ph -> ( E |` ran F ) = ( E |` S ) )
31 nfv 
 |-  F/ h ph
32 vex 
 |-  h e. _V
33 32 mptex 
 |-  ( x e. h |-> ( { x } .(+) N ) ) e. _V
34 33 rnex 
 |-  ran ( x e. h |-> ( { x } .(+) N ) ) e. _V
35 34 a1i 
 |-  ( ( ph /\ h e. S ) -> ran ( x e. h |-> ( { x } .(+) N ) ) e. _V )
36 31 35 8 fnmptd 
 |-  ( ph -> E Fn S )
37 fnresdm 
 |-  ( E Fn S -> ( E |` S ) = E )
38 36 37 syl 
 |-  ( ph -> ( E |` S ) = E )
39 30 38 eqtrd 
 |-  ( ph -> ( E |` ran F ) = E )
40 1 2 3 4 5 6 7 8 9 10 nsgqusf1olem2 
 |-  ( ph -> ran E = T )
41 39 29 40 f1oeq123d 
 |-  ( ph -> ( ( E |` ran F ) : ran F -1-1-onto-> ran E <-> E : S -1-1-onto-> T ) )
42 28 41 mpbid 
 |-  ( ph -> E : S -1-1-onto-> T )