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

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 ∈ SubGrp ⁡ G | N ⊆ h
nsgqusf1o.t ⊢ T = SubGrp ⁡ Q
nsgqusf1o.1 ⊢ ≤ ˙ = ≤ toInc ⁡ S
nsgqusf1o.2 No typesetting found for |- .c_ = ( le ` ( toInc ` T ) ) with typecode |-
nsgqusf1o.q ⊢ Q = G / 𝑠 G ~ QG N
nsgqusf1o.p ⊢ ⊕ ˙ = LSSum ⁡ G
nsgqusf1o.e ⊢ E = h ∈ S ⟼ ran ⁡ x ∈ h ⟼ x ⊕ ˙ N
nsgqusf1o.f ⊢ F = f ∈ T ⟼ a ∈ B | a ⊕ ˙ N ∈ f
nsgqusf1o.n ⊢ φ → N ∈ NrmSGrp ⁡ G
Assertion nsgqusf1o ⊢ φ → E : S ⟶ 1-1 onto T

Proof

Step Hyp Ref Expression
1 nsgqusf1o.b ⊢ B = Base G
2 nsgqusf1o.s ⊢ S = h ∈ SubGrp ⁡ G | N ⊆ h
3 nsgqusf1o.t ⊢ T = SubGrp ⁡ Q
4 nsgqusf1o.1 ⊢ ≤ ˙ = ≤ toInc ⁡ S
5 nsgqusf1o.2 Could not format .c_ = ( le ` ( toInc ` T ) ) : No typesetting found for |- .c_ = ( le ` ( toInc ` T ) ) with typecode |-
6 nsgqusf1o.q ⊢ Q = G / 𝑠 G ~ QG N
7 nsgqusf1o.p ⊢ ⊕ ˙ = LSSum ⁡ G
8 nsgqusf1o.e ⊢ E = h ∈ S ⟼ ran ⁡ x ∈ h ⟼ x ⊕ ˙ N
9 nsgqusf1o.f ⊢ F = f ∈ T ⟼ a ∈ B | a ⊕ ˙ N ∈ f
10 nsgqusf1o.n ⊢ φ → N ∈ NrmSGrp ⁡ G
11 eqid ⊢ toInc ⁡ S MGalConn toInc ⁡ T = toInc ⁡ S MGalConn toInc ⁡ T
12 fvex ⊢ SubGrp ⁡ G ∈ V
13 2 12 rabex2 ⊢ S ∈ V
14 eqid ⊢ toInc ⁡ S = toInc ⁡ S
15 14 ipobas ⊢ S ∈ V → S = Base toInc ⁡ S
16 13 15 ax-mp ⊢ S = Base toInc ⁡ S
17 3 fvexi ⊢ T ∈ V
18 eqid ⊢ toInc ⁡ T = toInc ⁡ T
19 18 ipobas ⊢ T ∈ V → T = Base toInc ⁡ T
20 17 19 ax-mp ⊢ T = Base toInc ⁡ T
21 14 ipopos ⊢ toInc ⁡ S ∈ Poset
22 21 a1i ⊢ φ → toInc ⁡ S ∈ Poset
23 18 ipopos ⊢ toInc ⁡ T ∈ Poset
24 23 a1i ⊢ φ → toInc ⁡ T ∈ Poset
25 1 2 3 11 14 18 6 7 8 9 10 nsgmgc ⊢ φ → E toInc ⁡ S MGalConn toInc ⁡ T F
26 11 16 20 4 5 22 24 25 mgcf1o Could not format ( ph -> ( E |` ran F ) Isom .<_ , .c_ ( ran F , ran E ) ) : No typesetting found for |- ( ph -> ( E |` ran F ) Isom .<_ , .c_ ( ran F , ran E ) ) with typecode |-
27 isof1o Could not format ( ( E |` ran F ) Isom .<_ , .c_ ( ran F , ran E ) -> ( E |` ran F ) : ran F -1-1-onto-> ran E ) : No typesetting found for |- ( ( E |` ran F ) Isom .<_ , .c_ ( ran F , ran E ) -> ( E |` ran F ) : ran F -1-1-onto-> ran E ) with typecode |-
28 26 27 syl ⊢ φ → E ↾ ran ⁡ F : ran ⁡ F ⟶ 1-1 onto ran ⁡ E
29 1 2 3 4 5 6 7 8 9 10 nsgqusf1olem3 ⊢ φ → ran ⁡ F = S
30 29 reseq2d ⊢ φ → E ↾ ran ⁡ F = E ↾ S
31 nfv ⊢ Ⅎ h φ
32 vex ⊢ h ∈ V
33 32 mptex ⊢ x ∈ h ⟼ x ⊕ ˙ N ∈ V
34 33 rnex ⊢ ran ⁡ x ∈ h ⟼ x ⊕ ˙ N ∈ V
35 34 a1i ⊢ φ ∧ h ∈ S → ran ⁡ x ∈ h ⟼ x ⊕ ˙ N ∈ V
36 31 35 8 fnmptd ⊢ φ → E Fn S
37 fnresdm ⊢ E Fn S → E ↾ S = E
38 36 37 syl ⊢ φ → E ↾ S = E
39 30 38 eqtrd ⊢ φ → E ↾ ran ⁡ F = E
40 1 2 3 4 5 6 7 8 9 10 nsgqusf1olem2 ⊢ φ → ran ⁡ E = T
41 39 29 40 f1oeq123d ⊢ φ → E ↾ ran ⁡ F : ran ⁡ F ⟶ 1-1 onto ran ⁡ E ↔ E : S ⟶ 1-1 onto T
42 28 41 mpbid ⊢ φ → E : S ⟶ 1-1 onto T