Step |
Hyp |
Ref |
Expression |
1 |
|
ringcbas.c |
|- C = ( RingCat ` U ) |
2 |
|
ringcbas.b |
|- B = ( Base ` C ) |
3 |
|
ringcbas.u |
|- ( ph -> U e. V ) |
4 |
|
ringchomfval.h |
|- H = ( Hom ` C ) |
5 |
1 2 3
|
ringcbas |
|- ( ph -> B = ( U i^i Ring ) ) |
6 |
|
eqidd |
|- ( ph -> ( RingHom |` ( B X. B ) ) = ( RingHom |` ( B X. B ) ) ) |
7 |
1 3 5 6
|
ringcval |
|- ( ph -> C = ( ( ExtStrCat ` U ) |`cat ( RingHom |` ( B X. B ) ) ) ) |
8 |
7
|
fveq2d |
|- ( ph -> ( Hom ` C ) = ( Hom ` ( ( ExtStrCat ` U ) |`cat ( RingHom |` ( B X. B ) ) ) ) ) |
9 |
4 8
|
syl5eq |
|- ( ph -> H = ( Hom ` ( ( ExtStrCat ` U ) |`cat ( RingHom |` ( B X. B ) ) ) ) ) |
10 |
|
eqid |
|- ( ( ExtStrCat ` U ) |`cat ( RingHom |` ( B X. B ) ) ) = ( ( ExtStrCat ` U ) |`cat ( RingHom |` ( B X. B ) ) ) |
11 |
|
eqid |
|- ( Base ` ( ExtStrCat ` U ) ) = ( Base ` ( ExtStrCat ` U ) ) |
12 |
|
fvexd |
|- ( ph -> ( ExtStrCat ` U ) e. _V ) |
13 |
5 6
|
rhmresfn |
|- ( ph -> ( RingHom |` ( B X. B ) ) Fn ( B X. B ) ) |
14 |
|
inss1 |
|- ( U i^i Ring ) C_ U |
15 |
14
|
a1i |
|- ( ph -> ( U i^i Ring ) C_ U ) |
16 |
|
eqid |
|- ( ExtStrCat ` U ) = ( ExtStrCat ` U ) |
17 |
16 3
|
estrcbas |
|- ( ph -> U = ( Base ` ( ExtStrCat ` U ) ) ) |
18 |
17
|
eqcomd |
|- ( ph -> ( Base ` ( ExtStrCat ` U ) ) = U ) |
19 |
15 5 18
|
3sstr4d |
|- ( ph -> B C_ ( Base ` ( ExtStrCat ` U ) ) ) |
20 |
10 11 12 13 19
|
reschom |
|- ( ph -> ( RingHom |` ( B X. B ) ) = ( Hom ` ( ( ExtStrCat ` U ) |`cat ( RingHom |` ( B X. B ) ) ) ) ) |
21 |
9 20
|
eqtr4d |
|- ( ph -> H = ( RingHom |` ( B X. B ) ) ) |