| 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 ) ) |