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

Metamath Proof Explorer

Theorem 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 H
gicqusker.f ⊢ φ → F ∈ G GrpHom H
gicqusker.k ⊢ K = F -1 0 ˙
gicqusker.q ⊢ Q = G / 𝑠 G ~ QG K
gicqusker.s ⊢ φ → ran ⁡ F = Base H
Assertion gicqusker ⊢ φ → Q ≃ 𝑔 H

Proof

Step Hyp Ref Expression
1 gicqusker.1 ⊢ 0 ˙ = 0 H
2 gicqusker.f ⊢ φ → F ∈ G GrpHom H
3 gicqusker.k ⊢ K = F -1 0 ˙
4 gicqusker.q ⊢ Q = G / 𝑠 G ~ QG K
5 gicqusker.s ⊢ φ → ran ⁡ F = Base H
6 imaeq2 ⊢ p = q → F p = F q
7 6 unieqd ⊢ p = q → ⋃ F p = ⋃ F q
8 7 cbvmptv ⊢ p ∈ Base Q ⟼ ⋃ F p = q ∈ Base Q ⟼ ⋃ F q
9 1 2 3 4 8 5 ghmqusker ⊢ φ → p ∈ Base Q ⟼ ⋃ F p ∈ Q GrpIso H
10 brgici ⊢ p ∈ Base Q ⟼ ⋃ F p ∈ Q GrpIso H → Q ≃ 𝑔 H
11 9 10 syl ⊢ φ → Q ≃ 𝑔 H