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 = ( RngHomo |` ( B X. B ) ) ) |
5 |
|
df-rngc |
|- RngCat = ( u e. _V |-> ( ( ExtStrCat ` u ) |`cat ( RngHomo |` ( ( 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 ) -> ( RngHomo |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) = ( RngHomo |` ( B X. B ) ) ) |
14 |
4
|
eqcomd |
|- ( ph -> ( RngHomo |` ( B X. B ) ) = H ) |
15 |
14
|
adantr |
|- ( ( ph /\ u = U ) -> ( RngHomo |` ( B X. B ) ) = H ) |
16 |
13 15
|
eqtrd |
|- ( ( ph /\ u = U ) -> ( RngHomo |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) = H ) |
17 |
7 16
|
oveq12d |
|- ( ( ph /\ u = U ) -> ( ( ExtStrCat ` u ) |`cat ( RngHomo |` ( ( 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
|
syl5eq |
|- ( ph -> C = ( ( ExtStrCat ` U ) |`cat H ) ) |