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}=\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 funcringcsetcALTV2lem6 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge {H}\in \left({X}\mathrm{RingHom}{Y}\right)\right)\to \left({X}{G}{Y}\right)\left({H}\right)={H}$

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 1 2 3 4 5 6 7 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)}$
9 8 3adant3 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge {H}\in \left({X}\mathrm{RingHom}{Y}\right)\right)\to {X}{G}{Y}={\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Y}\right)}$
10 9 fveq1d ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge {H}\in \left({X}\mathrm{RingHom}{Y}\right)\right)\to \left({X}{G}{Y}\right)\left({H}\right)=\left({\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Y}\right)}\right)\left({H}\right)$
11 fvresi ${⊢}{H}\in \left({X}\mathrm{RingHom}{Y}\right)\to \left({\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Y}\right)}\right)\left({H}\right)={H}$
12 11 3ad2ant3 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge {H}\in \left({X}\mathrm{RingHom}{Y}\right)\right)\to \left({\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Y}\right)}\right)\left({H}\right)={H}$
13 10 12 eqtrd ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge {H}\in \left({X}\mathrm{RingHom}{Y}\right)\right)\to \left({X}{G}{Y}\right)\left({H}\right)={H}$