| Step |
Hyp |
Ref |
Expression |
| 1 |
|
rngcval.c |
|- C = ( RngCat ` U ) |
| 2 |
|
rngcval.u |
|- ( ph -> U e. V ) |
| 3 |
|
rngcval.b |
|- ( ph -> B = ( U i^i Rng ) ) |
| 4 |
|
rngcval.h |
|- ( ph -> H = ( RngHom |` ( B X. B ) ) ) |
| 5 |
|
df-rngc |
|- RngCat = ( u e. _V |-> ( ( ExtStrCat ` u ) |`cat ( RngHom |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) ) ) |
| 6 |
|
fveq2 |
|- ( u = U -> ( ExtStrCat ` u ) = ( ExtStrCat ` U ) ) |
| 7 |
6
|
adantl |
|- ( ( ph /\ u = U ) -> ( ExtStrCat ` u ) = ( ExtStrCat ` U ) ) |
| 8 |
|
ineq1 |
|- ( u = U -> ( u i^i Rng ) = ( U i^i Rng ) ) |
| 9 |
8
|
sqxpeqd |
|- ( u = U -> ( ( u i^i Rng ) X. ( u i^i Rng ) ) = ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) |
| 10 |
3
|
sqxpeqd |
|- ( ph -> ( B X. B ) = ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) |
| 11 |
10
|
eqcomd |
|- ( ph -> ( ( U i^i Rng ) X. ( U i^i Rng ) ) = ( B X. B ) ) |
| 12 |
9 11
|
sylan9eqr |
|- ( ( ph /\ u = U ) -> ( ( u i^i Rng ) X. ( u i^i Rng ) ) = ( B X. B ) ) |
| 13 |
12
|
reseq2d |
|- ( ( ph /\ u = U ) -> ( RngHom |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) = ( RngHom |` ( B X. B ) ) ) |
| 14 |
4
|
eqcomd |
|- ( ph -> ( RngHom |` ( B X. B ) ) = H ) |
| 15 |
14
|
adantr |
|- ( ( ph /\ u = U ) -> ( RngHom |` ( B X. B ) ) = H ) |
| 16 |
13 15
|
eqtrd |
|- ( ( ph /\ u = U ) -> ( RngHom |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) = H ) |
| 17 |
7 16
|
oveq12d |
|- ( ( ph /\ u = U ) -> ( ( ExtStrCat ` u ) |`cat ( RngHom |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) ) = ( ( ExtStrCat ` U ) |`cat H ) ) |
| 18 |
2
|
elexd |
|- ( ph -> U e. _V ) |
| 19 |
|
ovexd |
|- ( ph -> ( ( ExtStrCat ` U ) |`cat H ) e. _V ) |
| 20 |
5 17 18 19
|
fvmptd2 |
|- ( ph -> ( RngCat ` U ) = ( ( ExtStrCat ` U ) |`cat H ) ) |
| 21 |
1 20
|
eqtrid |
|- ( ph -> C = ( ( ExtStrCat ` U ) |`cat H ) ) |