# Metamath Proof Explorer

## Theorem rhmsubcsetclem1

Description: Lemma 1 for rhmsubcsetc . (Contributed by AV, 9-Mar-2020)

Ref Expression
Hypotheses rhmsubcsetc.c ${⊢}{C}=\mathrm{ExtStrCat}\left({U}\right)$
rhmsubcsetc.u ${⊢}{\phi }\to {U}\in {V}$
rhmsubcsetc.b ${⊢}{\phi }\to {B}=\mathrm{Ring}\cap {U}$
rhmsubcsetc.h ${⊢}{\phi }\to {H}={\mathrm{RingHom}↾}_{\left({B}×{B}\right)}$
Assertion rhmsubcsetclem1 ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to \mathrm{Id}\left({C}\right)\left({x}\right)\in \left({x}{H}{x}\right)$

### Proof

Step Hyp Ref Expression
1 rhmsubcsetc.c ${⊢}{C}=\mathrm{ExtStrCat}\left({U}\right)$
2 rhmsubcsetc.u ${⊢}{\phi }\to {U}\in {V}$
3 rhmsubcsetc.b ${⊢}{\phi }\to {B}=\mathrm{Ring}\cap {U}$
4 rhmsubcsetc.h ${⊢}{\phi }\to {H}={\mathrm{RingHom}↾}_{\left({B}×{B}\right)}$
5 3 eleq2d ${⊢}{\phi }\to \left({x}\in {B}↔{x}\in \left(\mathrm{Ring}\cap {U}\right)\right)$
6 elin ${⊢}{x}\in \left(\mathrm{Ring}\cap {U}\right)↔\left({x}\in \mathrm{Ring}\wedge {x}\in {U}\right)$
7 6 simplbi ${⊢}{x}\in \left(\mathrm{Ring}\cap {U}\right)\to {x}\in \mathrm{Ring}$
8 5 7 syl6bi ${⊢}{\phi }\to \left({x}\in {B}\to {x}\in \mathrm{Ring}\right)$
9 8 imp ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {x}\in \mathrm{Ring}$
10 eqid ${⊢}{\mathrm{Base}}_{{x}}={\mathrm{Base}}_{{x}}$
11 10 idrhm ${⊢}{x}\in \mathrm{Ring}\to {\mathrm{I}↾}_{{\mathrm{Base}}_{{x}}}\in \left({x}\mathrm{RingHom}{x}\right)$
12 9 11 syl ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {\mathrm{I}↾}_{{\mathrm{Base}}_{{x}}}\in \left({x}\mathrm{RingHom}{x}\right)$
13 eqid ${⊢}\mathrm{Id}\left({C}\right)=\mathrm{Id}\left({C}\right)$
14 2 adantr ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {U}\in {V}$
15 6 simprbi ${⊢}{x}\in \left(\mathrm{Ring}\cap {U}\right)\to {x}\in {U}$
16 5 15 syl6bi ${⊢}{\phi }\to \left({x}\in {B}\to {x}\in {U}\right)$
17 16 imp ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {x}\in {U}$
18 1 13 14 17 estrcid ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to \mathrm{Id}\left({C}\right)\left({x}\right)={\mathrm{I}↾}_{{\mathrm{Base}}_{{x}}}$
19 4 oveqdr ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {x}{H}{x}={x}\left({\mathrm{RingHom}↾}_{\left({B}×{B}\right)}\right){x}$
20 eqid ${⊢}\mathrm{RingCat}\left({U}\right)=\mathrm{RingCat}\left({U}\right)$
21 eqid ${⊢}{\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}={\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}$
22 eqid ${⊢}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right)=\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right)$
23 20 21 2 22 ringchomfval ${⊢}{\phi }\to \mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right)={\mathrm{RingHom}↾}_{\left({\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}×{\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}\right)}$
24 20 21 2 ringcbas ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}={U}\cap \mathrm{Ring}$
25 incom ${⊢}\mathrm{Ring}\cap {U}={U}\cap \mathrm{Ring}$
26 3 25 syl6eq ${⊢}{\phi }\to {B}={U}\cap \mathrm{Ring}$
27 26 eqcomd ${⊢}{\phi }\to {U}\cap \mathrm{Ring}={B}$
28 24 27 eqtrd ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}={B}$
29 28 sqxpeqd ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}×{\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}={B}×{B}$
30 29 reseq2d ${⊢}{\phi }\to {\mathrm{RingHom}↾}_{\left({\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}×{\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}\right)}={\mathrm{RingHom}↾}_{\left({B}×{B}\right)}$
31 23 30 eqtrd ${⊢}{\phi }\to \mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right)={\mathrm{RingHom}↾}_{\left({B}×{B}\right)}$
32 31 adantr ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to \mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right)={\mathrm{RingHom}↾}_{\left({B}×{B}\right)}$
33 32 eqcomd ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {\mathrm{RingHom}↾}_{\left({B}×{B}\right)}=\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right)$
34 33 oveqd ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {x}\left({\mathrm{RingHom}↾}_{\left({B}×{B}\right)}\right){x}={x}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){x}$
35 26 eleq2d ${⊢}{\phi }\to \left({x}\in {B}↔{x}\in \left({U}\cap \mathrm{Ring}\right)\right)$
36 35 biimpa ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {x}\in \left({U}\cap \mathrm{Ring}\right)$
37 24 adantr ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}={U}\cap \mathrm{Ring}$
38 36 37 eleqtrrd ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {x}\in {\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}$
39 20 21 14 22 38 38 ringchom ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {x}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){x}={x}\mathrm{RingHom}{x}$
40 19 34 39 3eqtrd ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {x}{H}{x}={x}\mathrm{RingHom}{x}$
41 12 18 40 3eltr4d ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to \mathrm{Id}\left({C}\right)\left({x}\right)\in \left({x}{H}{x}\right)$