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

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. = ( 0g ` H )
rhmqusker.f 
|- ( ph -> F e. ( G RingHom H ) )
rhmqusker.k 
|- K = ( `' F " { .0. } )
rhmqusker.q 
|- Q = ( G /s ( G ~QG K ) )
rhmqusker.s 
|- ( ph -> ran F = ( Base ` H ) )
rhmqusker.2 
|- ( ph -> G e. CRing )
rhmqusker.j 
|- J = ( q e. ( Base ` Q ) |-> U. ( F " q ) )
Assertion rhmqusker 
|- ( ph -> J e. ( Q RingIso H ) )

Proof

Step Hyp Ref Expression
1 rhmqusker.1 
 |-  .0. = ( 0g ` H )
2 rhmqusker.f 
 |-  ( ph -> F e. ( G RingHom H ) )
3 rhmqusker.k 
 |-  K = ( `' F " { .0. } )
4 rhmqusker.q 
 |-  Q = ( G /s ( G ~QG K ) )
5 rhmqusker.s 
 |-  ( ph -> ran F = ( Base ` H ) )
6 rhmqusker.2 
 |-  ( ph -> G e. CRing )
7 rhmqusker.j 
 |-  J = ( q e. ( Base ` Q ) |-> U. ( F " q ) )
8 1 2 3 4 7 6 rhmquskerlem 
 |-  ( ph -> J e. ( Q RingHom H ) )
9 rhmghm 
 |-  ( F e. ( G RingHom H ) -> F e. ( G GrpHom H ) )
10 2 9 syl 
 |-  ( ph -> F e. ( G GrpHom H ) )
11 1 10 3 4 7 5 ghmqusker 
 |-  ( ph -> J e. ( Q GrpIso H ) )
12 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
13 eqid 
 |-  ( Base ` H ) = ( Base ` H )
14 12 13 gimf1o 
 |-  ( J e. ( Q GrpIso H ) -> J : ( Base ` Q ) -1-1-onto-> ( Base ` H ) )
15 11 14 syl 
 |-  ( ph -> J : ( Base ` Q ) -1-1-onto-> ( Base ` H ) )
16 12 13 isrim 
 |-  ( J e. ( Q RingIso H ) <-> ( J e. ( Q RingHom H ) /\ J : ( Base ` Q ) -1-1-onto-> ( Base ` H ) ) )
17 8 15 16 sylanbrc 
 |-  ( ph -> J e. ( Q RingIso H ) )