Theorem rhmsubcALTVlem2

Description: Lemma 2 for rhmsubcALTV . (Contributed by AV, 2-Mar-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rngcrescrhmALTV.u	|- ( ph -> U e. V )
	rngcrescrhmALTV.c	|- C = ( RngCatALTV ` U )
	rngcrescrhmALTV.r	|- ( ph -> R = ( Ring i^i U ) )
	rngcrescrhmALTV.h	|- H = ( RingHom |` ( R X. R ) )
Assertion	rhmsubcALTVlem2	|- ( ( ph /\ X e. R /\ Y e. R ) -> ( X H Y ) = ( X RingHom Y ) )

Proof

Step	Hyp	Ref	Expression
1		rngcrescrhmALTV.u	|- ( ph -> U e. V )
2		rngcrescrhmALTV.c	|- C = ( RngCatALTV ` U )
3		rngcrescrhmALTV.r	|- ( ph -> R = ( Ring i^i U ) )
4		rngcrescrhmALTV.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 ) )