Metamath Proof Explorer


Theorem funcringcsetclem7ALTV

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

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

Proof

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 ) ) )