Step |
Hyp |
Ref |
Expression |
1 |
|
ringcbasALTV.c |
|- C = ( RingCatALTV ` U ) |
2 |
|
ringcbasALTV.b |
|- B = ( Base ` C ) |
3 |
|
ringcbasALTV.u |
|- ( ph -> U e. V ) |
4 |
|
ringchomfvalALTV.h |
|- H = ( Hom ` C ) |
5 |
|
ringchomALTV.x |
|- ( ph -> X e. B ) |
6 |
|
ringchomALTV.y |
|- ( ph -> Y e. B ) |
7 |
1 2 3 4 5 6
|
ringchomALTV |
|- ( ph -> ( X H Y ) = ( X RingHom Y ) ) |
8 |
7
|
eleq2d |
|- ( ph -> ( F e. ( X H Y ) <-> F e. ( X RingHom Y ) ) ) |
9 |
|
eqid |
|- ( Base ` X ) = ( Base ` X ) |
10 |
|
eqid |
|- ( Base ` Y ) = ( Base ` Y ) |
11 |
9 10
|
rhmf |
|- ( F e. ( X RingHom Y ) -> F : ( Base ` X ) --> ( Base ` Y ) ) |
12 |
8 11
|
syl6bi |
|- ( ph -> ( F e. ( X H Y ) -> F : ( Base ` X ) --> ( Base ` Y ) ) ) |