# 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}=\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 funcringcsetcALTV2lem7 ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to \left({X}{G}{X}\right)\left(\mathrm{Id}\left({R}\right)\left({X}\right)\right)=\mathrm{Id}\left({S}\right)\left({F}\left({X}\right)\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 1 2 3 4 5 6 7 funcringcsetcALTV2lem5 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {X}\in {B}\right)\right)\to {X}{G}{X}={\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{X}\right)}$
9 8 anabsan2 ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to {X}{G}{X}={\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{X}\right)}$
10 eqid ${⊢}\mathrm{Id}\left({R}\right)=\mathrm{Id}\left({R}\right)$
11 5 adantr ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to {U}\in \mathrm{WUni}$
12 simpr ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to {X}\in {B}$
13 eqid ${⊢}{\mathrm{Base}}_{{X}}={\mathrm{Base}}_{{X}}$
14 1 3 10 11 12 13 ringcid ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to \mathrm{Id}\left({R}\right)\left({X}\right)={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}$
15 9 14 fveq12d ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to \left({X}{G}{X}\right)\left(\mathrm{Id}\left({R}\right)\left({X}\right)\right)=\left({\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{X}\right)}\right)\left({\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)$
16 1 3 5 ringcbas ${⊢}{\phi }\to {B}={U}\cap \mathrm{Ring}$
17 16 eleq2d ${⊢}{\phi }\to \left({X}\in {B}↔{X}\in \left({U}\cap \mathrm{Ring}\right)\right)$
18 elin ${⊢}{X}\in \left({U}\cap \mathrm{Ring}\right)↔\left({X}\in {U}\wedge {X}\in \mathrm{Ring}\right)$
19 18 simprbi ${⊢}{X}\in \left({U}\cap \mathrm{Ring}\right)\to {X}\in \mathrm{Ring}$
20 17 19 syl6bi ${⊢}{\phi }\to \left({X}\in {B}\to {X}\in \mathrm{Ring}\right)$
21 20 imp ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to {X}\in \mathrm{Ring}$
22 13 idrhm ${⊢}{X}\in \mathrm{Ring}\to {\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\in \left({X}\mathrm{RingHom}{X}\right)$
23 fvresi ${⊢}{\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\in \left({X}\mathrm{RingHom}{X}\right)\to \left({\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{X}\right)}\right)\left({\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}$
24 21 22 23 3syl ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to \left({\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{X}\right)}\right)\left({\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}$
25 1 2 3 4 5 6 funcringcsetcALTV2lem1 ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to {F}\left({X}\right)={\mathrm{Base}}_{{X}}$
26 25 fveq2d ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to \mathrm{Id}\left({S}\right)\left({F}\left({X}\right)\right)=\mathrm{Id}\left({S}\right)\left({\mathrm{Base}}_{{X}}\right)$
27 eqid ${⊢}\mathrm{Id}\left({S}\right)=\mathrm{Id}\left({S}\right)$
28 1 3 5 ringcbasbas ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to {\mathrm{Base}}_{{X}}\in {U}$
29 2 27 11 28 setcid ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to \mathrm{Id}\left({S}\right)\left({\mathrm{Base}}_{{X}}\right)={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}$
30 26 29 eqtr2d ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to {\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}=\mathrm{Id}\left({S}\right)\left({F}\left({X}\right)\right)$
31 15 24 30 3eqtrd ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to \left({X}{G}{X}\right)\left(\mathrm{Id}\left({R}\right)\left({X}\right)\right)=\mathrm{Id}\left({S}\right)\left({F}\left({X}\right)\right)$