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