Metamath Proof Explorer

Theorem funcringcsetcALTV2lem7

Description: Lemma 7 for funcringcsetcALTV2 . (Contributed by AV, 15-Feb-2020) (New usage is discouraged.)

Ref Expression
Hypotheses funcringcsetcALTV2.r 
|- R = ( RingCat ` U )
funcringcsetcALTV2.s 
|- S = ( SetCat ` U )
funcringcsetcALTV2.b 
|- B = ( Base ` R )
funcringcsetcALTV2.c 
|- C = ( Base ` S )
funcringcsetcALTV2.u 
|- ( ph -> U e. WUni )
funcringcsetcALTV2.f 
|- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )
funcringcsetcALTV2.g 
|- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )
Assertion funcringcsetcALTV2lem7 
|- ( ( ph /\ X e. B ) -> ( ( X G X ) ` ( ( Id ` R ) ` X ) ) = ( ( Id ` S ) ` ( F ` X ) ) )

Proof

Step Hyp Ref Expression
1 funcringcsetcALTV2.r 
 |-  R = ( RingCat ` U )
2 funcringcsetcALTV2.s 
 |-  S = ( SetCat ` U )
3 funcringcsetcALTV2.b 
 |-  B = ( Base ` R )
4 funcringcsetcALTV2.c 
 |-  C = ( Base ` S )
5 funcringcsetcALTV2.u 
 |-  ( ph -> U e. WUni )
6 funcringcsetcALTV2.f 
 |-  ( ph -> F = ( x e. B |-> ( Base ` x ) ) )
7 funcringcsetcALTV2.g 
 |-  ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )
8 1 2 3 4 5 6 7 funcringcsetcALTV2lem5 
 |-  ( ( 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 ringcid 
 |-  ( ( 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 ringcbas 
 |-  ( 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 funcringcsetcALTV2lem1 
 |-  ( ( 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 ringcbasbas 
 |-  ( ( 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 ) ) )