# Metamath Proof Explorer

## Theorem funcringcsetcALTV2lem5

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

Ref Expression
Hypotheses funcringcsetcALTV2.r ${⊢}{R}=\mathrm{RingCat}\left({U}\right)$
funcringcsetcALTV2.s ${⊢}{S}=\mathrm{SetCat}\left({U}\right)$
funcringcsetcALTV2.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
funcringcsetcALTV2.c ${⊢}{C}={\mathrm{Base}}_{{S}}$
funcringcsetcALTV2.u ${⊢}{\phi }\to {U}\in \mathrm{WUni}$
funcringcsetcALTV2.f ${⊢}{\phi }\to {F}=\left({x}\in {B}⟼{\mathrm{Base}}_{{x}}\right)$
funcringcsetcALTV2.g ${⊢}{\phi }\to {G}=\left({x}\in {B},{y}\in {B}⟼{\mathrm{I}↾}_{\left({x}\mathrm{RingHom}{y}\right)}\right)$
Assertion funcringcsetcALTV2lem5 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}{G}{Y}={\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Y}\right)}$

### Proof

Step Hyp Ref Expression
1 funcringcsetcALTV2.r ${⊢}{R}=\mathrm{RingCat}\left({U}\right)$
2 funcringcsetcALTV2.s ${⊢}{S}=\mathrm{SetCat}\left({U}\right)$
3 funcringcsetcALTV2.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
4 funcringcsetcALTV2.c ${⊢}{C}={\mathrm{Base}}_{{S}}$
5 funcringcsetcALTV2.u ${⊢}{\phi }\to {U}\in \mathrm{WUni}$
6 funcringcsetcALTV2.f ${⊢}{\phi }\to {F}=\left({x}\in {B}⟼{\mathrm{Base}}_{{x}}\right)$
7 funcringcsetcALTV2.g ${⊢}{\phi }\to {G}=\left({x}\in {B},{y}\in {B}⟼{\mathrm{I}↾}_{\left({x}\mathrm{RingHom}{y}\right)}\right)$
8 7 adantr ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {G}=\left({x}\in {B},{y}\in {B}⟼{\mathrm{I}↾}_{\left({x}\mathrm{RingHom}{y}\right)}\right)$
9 oveq12 ${⊢}\left({x}={X}\wedge {y}={Y}\right)\to {x}\mathrm{RingHom}{y}={X}\mathrm{RingHom}{Y}$
10 9 adantl ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\wedge \left({x}={X}\wedge {y}={Y}\right)\right)\to {x}\mathrm{RingHom}{y}={X}\mathrm{RingHom}{Y}$
11 10 reseq2d ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\wedge \left({x}={X}\wedge {y}={Y}\right)\right)\to {\mathrm{I}↾}_{\left({x}\mathrm{RingHom}{y}\right)}={\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Y}\right)}$
12 simprl ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}\in {B}$
13 simprr ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {Y}\in {B}$
14 ovexd ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}\mathrm{RingHom}{Y}\in \mathrm{V}$
15 14 resiexd ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Y}\right)}\in \mathrm{V}$
16 8 11 12 13 15 ovmpod ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}{G}{Y}={\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Y}\right)}$