Step |
Hyp |
Ref |
Expression |
1 |
|
rhmsubcsetc.c |
|- C = ( ExtStrCat ` U ) |
2 |
|
rhmsubcsetc.u |
|- ( ph -> U e. V ) |
3 |
|
rhmsubcsetc.b |
|- ( ph -> B = ( Ring i^i U ) ) |
4 |
|
rhmsubcsetc.h |
|- ( ph -> H = ( RingHom |` ( B X. B ) ) ) |
5 |
3
|
eleq2d |
|- ( ph -> ( x e. B <-> x e. ( Ring i^i U ) ) ) |
6 |
|
elin |
|- ( x e. ( Ring i^i U ) <-> ( x e. Ring /\ x e. U ) ) |
7 |
6
|
simplbi |
|- ( x e. ( Ring i^i U ) -> x e. Ring ) |
8 |
5 7
|
syl6bi |
|- ( ph -> ( x e. B -> x e. Ring ) ) |
9 |
8
|
imp |
|- ( ( ph /\ x e. B ) -> x e. Ring ) |
10 |
|
eqid |
|- ( Base ` x ) = ( Base ` x ) |
11 |
10
|
idrhm |
|- ( x e. Ring -> ( _I |` ( Base ` x ) ) e. ( x RingHom x ) ) |
12 |
9 11
|
syl |
|- ( ( ph /\ x e. B ) -> ( _I |` ( Base ` x ) ) e. ( x RingHom x ) ) |
13 |
|
eqid |
|- ( Id ` C ) = ( Id ` C ) |
14 |
2
|
adantr |
|- ( ( ph /\ x e. B ) -> U e. V ) |
15 |
6
|
simprbi |
|- ( x e. ( Ring i^i U ) -> x e. U ) |
16 |
5 15
|
syl6bi |
|- ( ph -> ( x e. B -> x e. U ) ) |
17 |
16
|
imp |
|- ( ( ph /\ x e. B ) -> x e. U ) |
18 |
1 13 14 17
|
estrcid |
|- ( ( ph /\ x e. B ) -> ( ( Id ` C ) ` x ) = ( _I |` ( Base ` x ) ) ) |
19 |
4
|
oveqdr |
|- ( ( ph /\ x e. B ) -> ( x H x ) = ( x ( RingHom |` ( B X. B ) ) x ) ) |
20 |
|
eqid |
|- ( RingCat ` U ) = ( RingCat ` U ) |
21 |
|
eqid |
|- ( Base ` ( RingCat ` U ) ) = ( Base ` ( RingCat ` U ) ) |
22 |
|
eqid |
|- ( Hom ` ( RingCat ` U ) ) = ( Hom ` ( RingCat ` U ) ) |
23 |
20 21 2 22
|
ringchomfval |
|- ( ph -> ( Hom ` ( RingCat ` U ) ) = ( RingHom |` ( ( Base ` ( RingCat ` U ) ) X. ( Base ` ( RingCat ` U ) ) ) ) ) |
24 |
20 21 2
|
ringcbas |
|- ( ph -> ( Base ` ( RingCat ` U ) ) = ( U i^i Ring ) ) |
25 |
|
incom |
|- ( Ring i^i U ) = ( U i^i Ring ) |
26 |
3 25
|
eqtrdi |
|- ( ph -> B = ( U i^i Ring ) ) |
27 |
26
|
eqcomd |
|- ( ph -> ( U i^i Ring ) = B ) |
28 |
24 27
|
eqtrd |
|- ( ph -> ( Base ` ( RingCat ` U ) ) = B ) |
29 |
28
|
sqxpeqd |
|- ( ph -> ( ( Base ` ( RingCat ` U ) ) X. ( Base ` ( RingCat ` U ) ) ) = ( B X. B ) ) |
30 |
29
|
reseq2d |
|- ( ph -> ( RingHom |` ( ( Base ` ( RingCat ` U ) ) X. ( Base ` ( RingCat ` U ) ) ) ) = ( RingHom |` ( B X. B ) ) ) |
31 |
23 30
|
eqtrd |
|- ( ph -> ( Hom ` ( RingCat ` U ) ) = ( RingHom |` ( B X. B ) ) ) |
32 |
31
|
adantr |
|- ( ( ph /\ x e. B ) -> ( Hom ` ( RingCat ` U ) ) = ( RingHom |` ( B X. B ) ) ) |
33 |
32
|
eqcomd |
|- ( ( ph /\ x e. B ) -> ( RingHom |` ( B X. B ) ) = ( Hom ` ( RingCat ` U ) ) ) |
34 |
33
|
oveqd |
|- ( ( ph /\ x e. B ) -> ( x ( RingHom |` ( B X. B ) ) x ) = ( x ( Hom ` ( RingCat ` U ) ) x ) ) |
35 |
26
|
eleq2d |
|- ( ph -> ( x e. B <-> x e. ( U i^i Ring ) ) ) |
36 |
35
|
biimpa |
|- ( ( ph /\ x e. B ) -> x e. ( U i^i Ring ) ) |
37 |
24
|
adantr |
|- ( ( ph /\ x e. B ) -> ( Base ` ( RingCat ` U ) ) = ( U i^i Ring ) ) |
38 |
36 37
|
eleqtrrd |
|- ( ( ph /\ x e. B ) -> x e. ( Base ` ( RingCat ` U ) ) ) |
39 |
20 21 14 22 38 38
|
ringchom |
|- ( ( ph /\ x e. B ) -> ( x ( Hom ` ( RingCat ` U ) ) x ) = ( x RingHom x ) ) |
40 |
19 34 39
|
3eqtrd |
|- ( ( ph /\ x e. B ) -> ( x H x ) = ( x RingHom x ) ) |
41 |
12 18 40
|
3eltr4d |
|- ( ( ph /\ x e. B ) -> ( ( Id ` C ) ` x ) e. ( x H x ) ) |