Theorem srhmsubclem3

Description: Lemma 3 for srhmsubc . (Contributed by AV, 19-Feb-2020)

	Ref	Expression
Hypotheses	srhmsubc.s	|- A. r e. S r e. Ring
	srhmsubc.c	|- C = ( U i^i S )
	srhmsubc.j	|- J = ( r e. C , s e. C |-> ( r RingHom s ) )
Assertion	srhmsubclem3	|- ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> ( X J Y ) = ( X ( Hom ` ( RingCat ` U ) ) Y ) )

Proof

Step	Hyp	Ref	Expression
1		srhmsubc.s	|- A. r e. S r e. Ring
2		srhmsubc.c	|- C = ( U i^i S )
3		srhmsubc.j	|- J = ( r e. C , s e. C |-> ( r RingHom s ) )
4	3	a1i	|- ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> J = ( r e. C , s e. C |-> ( r RingHom s ) ) )
5		oveq12	|- ( ( r = X /\ s = Y ) -> ( r RingHom s ) = ( X RingHom Y ) )
6	5	adantl	|- ( ( ( U e. V /\ ( X e. C /\ Y e. C ) ) /\ ( r = X /\ s = Y ) ) -> ( r RingHom s ) = ( X RingHom Y ) )
7		simpl	|- ( ( X e. C /\ Y e. C ) -> X e. C )
8	7	adantl	|- ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> X e. C )
9		simpr	|- ( ( X e. C /\ Y e. C ) -> Y e. C )
10	9	adantl	|- ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> Y e. C )
11		ovexd	|- ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> ( X RingHom Y ) e. _V )
12	4 6 8 10 11	ovmpod	|- ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> ( X J Y ) = ( X RingHom Y ) )
13		eqid	|- ( RingCat ` U ) = ( RingCat ` U )
14		eqid	|- ( Base ` ( RingCat ` U ) ) = ( Base ` ( RingCat ` U ) )
15		simpl	|- ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> U e. V )
16		eqid	|- ( Hom ` ( RingCat ` U ) ) = ( Hom ` ( RingCat ` U ) )
17	1 2	srhmsubclem2	|- ( ( U e. V /\ X e. C ) -> X e. ( Base ` ( RingCat ` U ) ) )
18	7 17	sylan2	|- ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> X e. ( Base ` ( RingCat ` U ) ) )
19	1 2	srhmsubclem2	|- ( ( U e. V /\ Y e. C ) -> Y e. ( Base ` ( RingCat ` U ) ) )
20	9 19	sylan2	|- ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> Y e. ( Base ` ( RingCat ` U ) ) )
21	13 14 15 16 18 20	ringchom	|- ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> ( X ( Hom ` ( RingCat ` U ) ) Y ) = ( X RingHom Y ) )
22	12 21	eqtr4d	|- ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> ( X J Y ) = ( X ( Hom ` ( RingCat ` U ) ) Y ) )