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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	nsgqusf1o.s	⊢ 𝑆 = { ℎ ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝑁 ⊆ ℎ }
	nsgqusf1o.t	⊢ 𝑇 = ( SubGrp ‘ 𝑄 )
	nsgqusf1o.1	⊢ ≤ = ( le ‘ ( toInc ‘ 𝑆 ) )
	nsgqusf1o.2	⊢ ≲ = ( le ‘ ( toInc ‘ 𝑇 ) )
	nsgqusf1o.q	⊢ 𝑄 = ( 𝐺 /_s ( 𝐺 ~_QG 𝑁 ) )
	nsgqusf1o.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
	nsgqusf1o.e	⊢ 𝐸 = ( ℎ ∈ 𝑆 ↦ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
	nsgqusf1o.f	⊢ 𝐹 = ( 𝑓 ∈ 𝑇 ↦ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
	nsgqusf1o.n	⊢ ( 𝜑 → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
Assertion	nsgqusf1o	⊢ ( 𝜑 → 𝐸 : 𝑆 –1-1-onto→ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		nsgqusf1o.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		nsgqusf1o.s	⊢ 𝑆 = { ℎ ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝑁 ⊆ ℎ }
3		nsgqusf1o.t	⊢ 𝑇 = ( SubGrp ‘ 𝑄 )
4		nsgqusf1o.1	⊢ ≤ = ( le ‘ ( toInc ‘ 𝑆 ) )
5		nsgqusf1o.2	⊢ ≲ = ( le ‘ ( toInc ‘ 𝑇 ) )
6		nsgqusf1o.q	⊢ 𝑄 = ( 𝐺 /_s ( 𝐺 ~_QG 𝑁 ) )
7		nsgqusf1o.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
8		nsgqusf1o.e	⊢ 𝐸 = ( ℎ ∈ 𝑆 ↦ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
9		nsgqusf1o.f	⊢ 𝐹 = ( 𝑓 ∈ 𝑇 ↦ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
10		nsgqusf1o.n	⊢ ( 𝜑 → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
11		eqid	⊢ ( ( toInc ‘ 𝑆 ) MGalConn ( toInc ‘ 𝑇 ) ) = ( ( toInc ‘ 𝑆 ) MGalConn ( toInc ‘ 𝑇 ) )
12		fvex	⊢ ( SubGrp ‘ 𝐺 ) ∈ V
13	2 12	rabex2	⊢ 𝑆 ∈ V
14		eqid	⊢ ( toInc ‘ 𝑆 ) = ( toInc ‘ 𝑆 )
15	14	ipobas	⊢ ( 𝑆 ∈ V → 𝑆 = ( Base ‘ ( toInc ‘ 𝑆 ) ) )
16	13 15	ax-mp	⊢ 𝑆 = ( Base ‘ ( toInc ‘ 𝑆 ) )
17	3	fvexi	⊢ 𝑇 ∈ V
18		eqid	⊢ ( toInc ‘ 𝑇 ) = ( toInc ‘ 𝑇 )
19	18	ipobas	⊢ ( 𝑇 ∈ V → 𝑇 = ( Base ‘ ( toInc ‘ 𝑇 ) ) )
20	17 19	ax-mp	⊢ 𝑇 = ( Base ‘ ( toInc ‘ 𝑇 ) )
21	14	ipopos	⊢ ( toInc ‘ 𝑆 ) ∈ Poset
22	21	a1i	⊢ ( 𝜑 → ( toInc ‘ 𝑆 ) ∈ Poset )
23	18	ipopos	⊢ ( toInc ‘ 𝑇 ) ∈ Poset
24	23	a1i	⊢ ( 𝜑 → ( toInc ‘ 𝑇 ) ∈ Poset )
25	1 2 3 11 14 18 6 7 8 9 10	nsgmgc	⊢ ( 𝜑 → 𝐸 ( ( toInc ‘ 𝑆 ) MGalConn ( toInc ‘ 𝑇 ) ) 𝐹 )
26	11 16 20 4 5 22 24 25	mgcf1o	⊢ ( 𝜑 → ( 𝐸 ↾ ran 𝐹 ) Isom ≤ , ≲ ( ran 𝐹 , ran 𝐸 ) )
27		isof1o	⊢ ( ( 𝐸 ↾ ran 𝐹 ) Isom ≤ , ≲ ( ran 𝐹 , ran 𝐸 ) → ( 𝐸 ↾ ran 𝐹 ) : ran 𝐹 –1-1-onto→ ran 𝐸 )
28	26 27	syl	⊢ ( 𝜑 → ( 𝐸 ↾ ran 𝐹 ) : ran 𝐹 –1-1-onto→ ran 𝐸 )
29	1 2 3 4 5 6 7 8 9 10	nsgqusf1olem3	⊢ ( 𝜑 → ran 𝐹 = 𝑆 )
30	29	reseq2d	⊢ ( 𝜑 → ( 𝐸 ↾ ran 𝐹 ) = ( 𝐸 ↾ 𝑆 ) )
31		nfv	⊢ Ⅎ ℎ 𝜑
32		vex	⊢ ℎ ∈ V
33	32	mptex	⊢ ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∈ V
34	33	rnex	⊢ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∈ V
35	34	a1i	⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∈ V )
36	31 35 8	fnmptd	⊢ ( 𝜑 → 𝐸 Fn 𝑆 )
37		fnresdm	⊢ ( 𝐸 Fn 𝑆 → ( 𝐸 ↾ 𝑆 ) = 𝐸 )
38	36 37	syl	⊢ ( 𝜑 → ( 𝐸 ↾ 𝑆 ) = 𝐸 )
39	30 38	eqtrd	⊢ ( 𝜑 → ( 𝐸 ↾ ran 𝐹 ) = 𝐸 )
40	1 2 3 4 5 6 7 8 9 10	nsgqusf1olem2	⊢ ( 𝜑 → ran 𝐸 = 𝑇 )
41	39 29 40	f1oeq123d	⊢ ( 𝜑 → ( ( 𝐸 ↾ ran 𝐹 ) : ran 𝐹 –1-1-onto→ ran 𝐸 ↔ 𝐸 : 𝑆 –1-1-onto→ 𝑇 ) )
42	28 41	mpbid	⊢ ( 𝜑 → 𝐸 : 𝑆 –1-1-onto→ 𝑇 )

Metamath Proof Explorer

Theorem nsgqusf1o

Proof