Metamath Proof Explorer

Theorem srhmsubcALTVlem2

Description: Lemma 2 for srhmsubcALTV . (Contributed by AV, 19-Feb-2020) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 srhmsubcALTV.s 
 |-  A. r e. S r e. Ring
2 srhmsubcALTV.c 
 |-  C = ( U i^i S )
3 srhmsubcALTV.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 
 |-  ( RingCatALTV ` U ) = ( RingCatALTV ` U )
14 eqid 
 |-  ( Base ` ( RingCatALTV ` U ) ) = ( Base ` ( RingCatALTV ` U ) )
15 simpl 
 |-  ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> U e. V )
16 eqid 
 |-  ( Hom ` ( RingCatALTV ` U ) ) = ( Hom ` ( RingCatALTV ` U ) )
17 1 2 srhmsubcALTVlem1 
 |-  ( ( U e. V /\ X e. C ) -> X e. ( Base ` ( RingCatALTV ` U ) ) )
18 7 17 sylan2 
 |-  ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> X e. ( Base ` ( RingCatALTV ` U ) ) )
19 1 2 srhmsubcALTVlem1 
 |-  ( ( U e. V /\ Y e. C ) -> Y e. ( Base ` ( RingCatALTV ` U ) ) )
20 9 19 sylan2 
 |-  ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> Y e. ( Base ` ( RingCatALTV ` U ) ) )
21 13 14 15 16 18 20 ringchomALTV 
 |-  ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> ( X ( Hom ` ( RingCatALTV ` U ) ) Y ) = ( X RingHom Y ) )
22 12 21 eqtr4d 
 |-  ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> ( X J Y ) = ( X ( Hom ` ( RingCatALTV ` U ) ) Y ) )