Metamath Proof Explorer

Theorem rhmqusker

Description: A surjective ring homomorphism F from G to H induces an isomorphism J from Q to H , where Q is the factor group of G by F 's kernel K . (Contributed by Thierry Arnoux, 25-Feb-2025)

Ref Expression
Hypotheses rhmqusker.1 ⊢ 0 ˙ = 0 H
rhmqusker.f ⊢ φ → F ∈ G RingHom H
rhmqusker.k ⊢ K = F -1 0 ˙
rhmqusker.q ⊢ Q = G / 𝑠 G ~ QG K
rhmqusker.s ⊢ φ → ran ⁡ F = Base H
rhmqusker.2 ⊢ φ → G ∈ CRing
rhmqusker.j ⊢ J = q ∈ Base Q ⟼ ⋃ F q
Assertion rhmqusker ⊢ φ → J ∈ Q RingIso H

Proof

Step Hyp Ref Expression
1 rhmqusker.1 ⊢ 0 ˙ = 0 H
2 rhmqusker.f ⊢ φ → F ∈ G RingHom H
3 rhmqusker.k ⊢ K = F -1 0 ˙
4 rhmqusker.q ⊢ Q = G / 𝑠 G ~ QG K
5 rhmqusker.s ⊢ φ → ran ⁡ F = Base H
6 rhmqusker.2 ⊢ φ → G ∈ CRing
7 rhmqusker.j ⊢ J = q ∈ Base Q ⟼ ⋃ F q
8 1 2 3 4 7 6 rhmquskerlem ⊢ φ → J ∈ Q RingHom H
9 rhmghm ⊢ F ∈ G RingHom H → F ∈ G GrpHom H
10 2 9 syl ⊢ φ → F ∈ G GrpHom H
11 1 10 3 4 7 5 ghmqusker ⊢ φ → J ∈ Q GrpIso H
12 eqid ⊢ Base Q = Base Q
13 eqid ⊢ Base H = Base H
14 12 13 gimf1o ⊢ J ∈ Q GrpIso H → J : Base Q ⟶ 1-1 onto Base H
15 11 14 syl ⊢ φ → J : Base Q ⟶ 1-1 onto Base H
16 12 13 isrim ⊢ J ∈ Q RingIso H ↔ J ∈ Q RingHom H ∧ J : Base Q ⟶ 1-1 onto Base H
17 8 15 16 sylanbrc ⊢ φ → J ∈ Q RingIso H