# 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 )`
` |-  ( ( 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 ) ) )`