# Metamath Proof Explorer

## Theorem funcringcsetcALTV2lem6

Description: Lemma 6 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 funcringcsetcALTV2lem6
`|- ( ( ph /\ ( X e. B /\ Y e. B ) /\ H e. ( X RingHom Y ) ) -> ( ( X G Y ) ` H ) = H )`

### 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 /\ Y e. B ) ) -> ( X G Y ) = ( _I |` ( X RingHom Y ) ) )`
` |-  ( ( ph /\ ( X e. B /\ Y e. B ) /\ H e. ( X RingHom Y ) ) -> ( X G Y ) = ( _I |` ( X RingHom Y ) ) )`
10 9 fveq1d
` |-  ( ( ph /\ ( X e. B /\ Y e. B ) /\ H e. ( X RingHom Y ) ) -> ( ( X G Y ) ` H ) = ( ( _I |` ( X RingHom Y ) ) ` H ) )`
11 fvresi
` |-  ( H e. ( X RingHom Y ) -> ( ( _I |` ( X RingHom Y ) ) ` H ) = H )`
` |-  ( ( ph /\ ( X e. B /\ Y e. B ) /\ H e. ( X RingHom Y ) ) -> ( ( _I |` ( X RingHom Y ) ) ` H ) = H )`
` |-  ( ( ph /\ ( X e. B /\ Y e. B ) /\ H e. ( X RingHom Y ) ) -> ( ( X G Y ) ` H ) = H )`