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

Metamath Proof Explorer

Theorem ricqusker

Description: The image H of a ring homomorphism F is isomorphic with the quotient ring Q over F 's kernel K . This a part of what is sometimes called the first isomorphism theorem for rings. (Contributed by Thierry Arnoux, 10-Mar-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 )
	Assertion	ricqusker	\|- ( ph -> Q ~=r 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		imaeq2	\|- ( p = q -> ( F " p ) = ( F " q ) )
8	7	unieqd	\|- ( p = q -> U. ( F " p ) = U. ( F " q ) )
9	8	cbvmptv	\|- ( p e. ( Base ` Q ) \|-> U. ( F " p ) ) = ( q e. ( Base ` Q ) \|-> U. ( F " q ) )
10	1 2 3 4 5 6 9	rhmqusker	\|- ( ph -> ( p e. ( Base ` Q ) \|-> U. ( F " p ) ) e. ( Q RingIso H ) )
11		brrici	\|- ( ( p e. ( Base ` Q ) \|-> U. ( F " p ) ) e. ( Q RingIso H ) -> Q ~=r H )
12	10 11	syl	\|- ( ph -> Q ~=r H )