Theorem rhmsubclem1

Description: Lemma 1 for rhmsubc . (Contributed by AV, 2-Mar-2020)

	Ref	Expression
Hypotheses	rngcrescrhm.u	|- ( ph -> U e. V )
	rngcrescrhm.c	|- C = ( RngCat ` U )
	rngcrescrhm.r	|- ( ph -> R = ( Ring i^i U ) )
	rngcrescrhm.h	|- H = ( RingHom |` ( R X. R ) )
Assertion	rhmsubclem1	|- ( ph -> H Fn ( R X. R ) )

Proof

Step	Hyp	Ref	Expression
1		rngcrescrhm.u	|- ( ph -> U e. V )
2		rngcrescrhm.c	|- C = ( RngCat ` U )
3		rngcrescrhm.r	|- ( ph -> R = ( Ring i^i U ) )
4		rngcrescrhm.h	|- H = ( RingHom |` ( R X. R ) )
5		eqid	|- ( x e. R , y e. R |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) ) = ( x e. R , y e. R |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) )
6		ovex	|- ( x GrpHom y ) e. _V
7	6	inex1	|- ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) e. _V
8	5 7	fnmpoi	|- ( x e. R , y e. R |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) ) Fn ( R X. R )
9	4	a1i	|- ( ph -> H = ( RingHom |` ( R X. R ) ) )
10		dfrhm2	|- RingHom = ( x e. Ring , y e. Ring |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) )
11	10	a1i	|- ( ph -> RingHom = ( x e. Ring , y e. Ring |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) ) )
12	11	reseq1d	|- ( ph -> ( RingHom |` ( R X. R ) ) = ( ( x e. Ring , y e. Ring |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) ) |` ( R X. R ) ) )
13		inss1	|- ( Ring i^i U ) C_ Ring
14	3 13	eqsstrdi	|- ( ph -> R C_ Ring )
15		resmpo	|- ( ( R C_ Ring /\ R C_ Ring ) -> ( ( x e. Ring , y e. Ring |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) ) |` ( R X. R ) ) = ( x e. R , y e. R |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) ) )
16	14 14 15	syl2anc	|- ( ph -> ( ( x e. Ring , y e. Ring |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) ) |` ( R X. R ) ) = ( x e. R , y e. R |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) ) )
17	9 12 16	3eqtrd	|- ( ph -> H = ( x e. R , y e. R |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) ) )
18	17	fneq1d	|- ( ph -> ( H Fn ( R X. R ) <-> ( x e. R , y e. R |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) ) Fn ( R X. R ) ) )
19	8 18	mpbiri	|- ( ph -> H Fn ( R X. R ) )