gicqusker

Description: The image H of a group homomorphism F is isomorphic with the quotient group Q over F 's kernel K . Together with ghmker and ghmima , this is sometimes called the first isomorphism theorem for groups. (Contributed by Thierry Arnoux, 10-Mar-2025)

	Ref	Expression
Hypotheses	gicqusker.1	⊢ 0 = ( 0_g ‘ 𝐻 )
	gicqusker.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
	gicqusker.k	⊢ 𝐾 = ( ^◡ 𝐹 “ { 0 } )
	gicqusker.q	⊢ 𝑄 = ( 𝐺 /_s ( 𝐺 ~_QG 𝐾 ) )
	gicqusker.s	⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ 𝐻 ) )
Assertion	gicqusker	⊢ ( 𝜑 → 𝑄 ≃_𝑔 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		gicqusker.1	⊢ 0 = ( 0_g ‘ 𝐻 )
2		gicqusker.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
3		gicqusker.k	⊢ 𝐾 = ( ^◡ 𝐹 “ { 0 } )
4		gicqusker.q	⊢ 𝑄 = ( 𝐺 /_s ( 𝐺 ~_QG 𝐾 ) )
5		gicqusker.s	⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ 𝐻 ) )
6		imaeq2	⊢ ( 𝑝 = 𝑞 → ( 𝐹 “ 𝑝 ) = ( 𝐹 “ 𝑞 ) )
7	6	unieqd	⊢ ( 𝑝 = 𝑞 → ∪ ( 𝐹 “ 𝑝 ) = ∪ ( 𝐹 “ 𝑞 ) )
8	7	cbvmptv	⊢ ( 𝑝 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑝 ) ) = ( 𝑞 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑞 ) )
9	1 2 3 4 8 5	ghmqusker	⊢ ( 𝜑 → ( 𝑝 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑝 ) ) ∈ ( 𝑄 GrpIso 𝐻 ) )
10		brgici	⊢ ( ( 𝑝 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑝 ) ) ∈ ( 𝑄 GrpIso 𝐻 ) → 𝑄 ≃_𝑔 𝐻 )
11	9 10	syl	⊢ ( 𝜑 → 𝑄 ≃_𝑔 𝐻 )

Metamath Proof Explorer

Theorem gicqusker

Proof