Step |
Hyp |
Ref |
Expression |
1 |
|
funcringcsetcALTV.r |
|- R = ( RingCatALTV ` U ) |
2 |
|
funcringcsetcALTV.s |
|- S = ( SetCat ` U ) |
3 |
|
funcringcsetcALTV.b |
|- B = ( Base ` R ) |
4 |
|
funcringcsetcALTV.c |
|- C = ( Base ` S ) |
5 |
|
funcringcsetcALTV.u |
|- ( ph -> U e. WUni ) |
6 |
|
funcringcsetcALTV.f |
|- ( ph -> F = ( x e. B |-> ( Base ` x ) ) ) |
7 |
|
funcringcsetcALTV.g |
|- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) ) |
8 |
1 2 3 4 5 6 7
|
funcringcsetclem5ALTV |
|- ( ( ph /\ ( X e. B /\ X e. B ) ) -> ( X G X ) = ( _I |` ( X RingHom X ) ) ) |
9 |
8
|
anabsan2 |
|- ( ( ph /\ X e. B ) -> ( X G X ) = ( _I |` ( X RingHom X ) ) ) |
10 |
|
eqid |
|- ( Id ` R ) = ( Id ` R ) |
11 |
5
|
adantr |
|- ( ( ph /\ X e. B ) -> U e. WUni ) |
12 |
|
simpr |
|- ( ( ph /\ X e. B ) -> X e. B ) |
13 |
|
eqid |
|- ( Base ` X ) = ( Base ` X ) |
14 |
1 3 10 11 12 13
|
ringcidALTV |
|- ( ( ph /\ X e. B ) -> ( ( Id ` R ) ` X ) = ( _I |` ( Base ` X ) ) ) |
15 |
9 14
|
fveq12d |
|- ( ( ph /\ X e. B ) -> ( ( X G X ) ` ( ( Id ` R ) ` X ) ) = ( ( _I |` ( X RingHom X ) ) ` ( _I |` ( Base ` X ) ) ) ) |
16 |
1 3 5
|
ringcbasALTV |
|- ( ph -> B = ( U i^i Ring ) ) |
17 |
16
|
eleq2d |
|- ( ph -> ( X e. B <-> X e. ( U i^i Ring ) ) ) |
18 |
|
elin |
|- ( X e. ( U i^i Ring ) <-> ( X e. U /\ X e. Ring ) ) |
19 |
18
|
simprbi |
|- ( X e. ( U i^i Ring ) -> X e. Ring ) |
20 |
17 19
|
syl6bi |
|- ( ph -> ( X e. B -> X e. Ring ) ) |
21 |
20
|
imp |
|- ( ( ph /\ X e. B ) -> X e. Ring ) |
22 |
13
|
idrhm |
|- ( X e. Ring -> ( _I |` ( Base ` X ) ) e. ( X RingHom X ) ) |
23 |
|
fvresi |
|- ( ( _I |` ( Base ` X ) ) e. ( X RingHom X ) -> ( ( _I |` ( X RingHom X ) ) ` ( _I |` ( Base ` X ) ) ) = ( _I |` ( Base ` X ) ) ) |
24 |
21 22 23
|
3syl |
|- ( ( ph /\ X e. B ) -> ( ( _I |` ( X RingHom X ) ) ` ( _I |` ( Base ` X ) ) ) = ( _I |` ( Base ` X ) ) ) |
25 |
1 2 3 4 5 6
|
funcringcsetclem1ALTV |
|- ( ( ph /\ X e. B ) -> ( F ` X ) = ( Base ` X ) ) |
26 |
25
|
fveq2d |
|- ( ( ph /\ X e. B ) -> ( ( Id ` S ) ` ( F ` X ) ) = ( ( Id ` S ) ` ( Base ` X ) ) ) |
27 |
|
eqid |
|- ( Id ` S ) = ( Id ` S ) |
28 |
1 3 5
|
ringcbasbasALTV |
|- ( ( ph /\ X e. B ) -> ( Base ` X ) e. U ) |
29 |
2 27 11 28
|
setcid |
|- ( ( ph /\ X e. B ) -> ( ( Id ` S ) ` ( Base ` X ) ) = ( _I |` ( Base ` X ) ) ) |
30 |
26 29
|
eqtr2d |
|- ( ( ph /\ X e. B ) -> ( _I |` ( Base ` X ) ) = ( ( Id ` S ) ` ( F ` X ) ) ) |
31 |
15 24 30
|
3eqtrd |
|- ( ( ph /\ X e. B ) -> ( ( X G X ) ` ( ( Id ` R ) ` X ) ) = ( ( Id ` S ) ` ( F ` X ) ) ) |