Theorem rhmsubclem2

Description: Lemma 2 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	rhmsubclem2	|- ( ( ph /\ X e. R /\ Y e. R ) -> ( X H Y ) = ( X RingHom Y ) )

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		opelxpi	|- ( ( X e. R /\ Y e. R ) -> <. X , Y >. e. ( R X. R ) )
6	5	3adant1	|- ( ( ph /\ X e. R /\ Y e. R ) -> <. X , Y >. e. ( R X. R ) )
7	6	fvresd	|- ( ( ph /\ X e. R /\ Y e. R ) -> ( ( RingHom |` ( R X. R ) ) ` <. X , Y >. ) = ( RingHom ` <. X , Y >. ) )
8		df-ov	|- ( X H Y ) = ( H ` <. X , Y >. )
9	4	fveq1i	|- ( H ` <. X , Y >. ) = ( ( RingHom |` ( R X. R ) ) ` <. X , Y >. )
10	8 9	eqtri	|- ( X H Y ) = ( ( RingHom |` ( R X. R ) ) ` <. X , Y >. )
11		df-ov	|- ( X RingHom Y ) = ( RingHom ` <. X , Y >. )
12	7 10 11	3eqtr4g	|- ( ( ph /\ X e. R /\ Y e. R ) -> ( X H Y ) = ( X RingHom Y ) )