Metamath Proof Explorer


Theorem rhmsubcsetclem1

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

Ref Expression
Hypotheses rhmsubcsetc.c
|- C = ( ExtStrCat ` U )
rhmsubcsetc.u
|- ( ph -> U e. V )
rhmsubcsetc.b
|- ( ph -> B = ( Ring i^i U ) )
rhmsubcsetc.h
|- ( ph -> H = ( RingHom |` ( B X. B ) ) )
Assertion rhmsubcsetclem1
|- ( ( ph /\ x e. B ) -> ( ( Id ` C ) ` x ) e. ( x H x ) )

Proof

Step Hyp Ref Expression
1 rhmsubcsetc.c
 |-  C = ( ExtStrCat ` U )
2 rhmsubcsetc.u
 |-  ( ph -> U e. V )
3 rhmsubcsetc.b
 |-  ( ph -> B = ( Ring i^i U ) )
4 rhmsubcsetc.h
 |-  ( ph -> H = ( RingHom |` ( B X. B ) ) )
5 3 eleq2d
 |-  ( ph -> ( x e. B <-> x e. ( Ring i^i U ) ) )
6 elin
 |-  ( x e. ( Ring i^i U ) <-> ( x e. Ring /\ x e. U ) )
7 6 simplbi
 |-  ( x e. ( Ring i^i U ) -> x e. Ring )
8 5 7 syl6bi
 |-  ( ph -> ( x e. B -> x e. Ring ) )
9 8 imp
 |-  ( ( ph /\ x e. B ) -> x e. Ring )
10 eqid
 |-  ( Base ` x ) = ( Base ` x )
11 10 idrhm
 |-  ( x e. Ring -> ( _I |` ( Base ` x ) ) e. ( x RingHom x ) )
12 9 11 syl
 |-  ( ( ph /\ x e. B ) -> ( _I |` ( Base ` x ) ) e. ( x RingHom x ) )
13 eqid
 |-  ( Id ` C ) = ( Id ` C )
14 2 adantr
 |-  ( ( ph /\ x e. B ) -> U e. V )
15 6 simprbi
 |-  ( x e. ( Ring i^i U ) -> x e. U )
16 5 15 syl6bi
 |-  ( ph -> ( x e. B -> x e. U ) )
17 16 imp
 |-  ( ( ph /\ x e. B ) -> x e. U )
18 1 13 14 17 estrcid
 |-  ( ( ph /\ x e. B ) -> ( ( Id ` C ) ` x ) = ( _I |` ( Base ` x ) ) )
19 4 oveqdr
 |-  ( ( ph /\ x e. B ) -> ( x H x ) = ( x ( RingHom |` ( B X. B ) ) x ) )
20 eqid
 |-  ( RingCat ` U ) = ( RingCat ` U )
21 eqid
 |-  ( Base ` ( RingCat ` U ) ) = ( Base ` ( RingCat ` U ) )
22 eqid
 |-  ( Hom ` ( RingCat ` U ) ) = ( Hom ` ( RingCat ` U ) )
23 20 21 2 22 ringchomfval
 |-  ( ph -> ( Hom ` ( RingCat ` U ) ) = ( RingHom |` ( ( Base ` ( RingCat ` U ) ) X. ( Base ` ( RingCat ` U ) ) ) ) )
24 20 21 2 ringcbas
 |-  ( ph -> ( Base ` ( RingCat ` U ) ) = ( U i^i Ring ) )
25 incom
 |-  ( Ring i^i U ) = ( U i^i Ring )
26 3 25 eqtrdi
 |-  ( ph -> B = ( U i^i Ring ) )
27 26 eqcomd
 |-  ( ph -> ( U i^i Ring ) = B )
28 24 27 eqtrd
 |-  ( ph -> ( Base ` ( RingCat ` U ) ) = B )
29 28 sqxpeqd
 |-  ( ph -> ( ( Base ` ( RingCat ` U ) ) X. ( Base ` ( RingCat ` U ) ) ) = ( B X. B ) )
30 29 reseq2d
 |-  ( ph -> ( RingHom |` ( ( Base ` ( RingCat ` U ) ) X. ( Base ` ( RingCat ` U ) ) ) ) = ( RingHom |` ( B X. B ) ) )
31 23 30 eqtrd
 |-  ( ph -> ( Hom ` ( RingCat ` U ) ) = ( RingHom |` ( B X. B ) ) )
32 31 adantr
 |-  ( ( ph /\ x e. B ) -> ( Hom ` ( RingCat ` U ) ) = ( RingHom |` ( B X. B ) ) )
33 32 eqcomd
 |-  ( ( ph /\ x e. B ) -> ( RingHom |` ( B X. B ) ) = ( Hom ` ( RingCat ` U ) ) )
34 33 oveqd
 |-  ( ( ph /\ x e. B ) -> ( x ( RingHom |` ( B X. B ) ) x ) = ( x ( Hom ` ( RingCat ` U ) ) x ) )
35 26 eleq2d
 |-  ( ph -> ( x e. B <-> x e. ( U i^i Ring ) ) )
36 35 biimpa
 |-  ( ( ph /\ x e. B ) -> x e. ( U i^i Ring ) )
37 24 adantr
 |-  ( ( ph /\ x e. B ) -> ( Base ` ( RingCat ` U ) ) = ( U i^i Ring ) )
38 36 37 eleqtrrd
 |-  ( ( ph /\ x e. B ) -> x e. ( Base ` ( RingCat ` U ) ) )
39 20 21 14 22 38 38 ringchom
 |-  ( ( ph /\ x e. B ) -> ( x ( Hom ` ( RingCat ` U ) ) x ) = ( x RingHom x ) )
40 19 34 39 3eqtrd
 |-  ( ( ph /\ x e. B ) -> ( x H x ) = ( x RingHom x ) )
41 12 18 40 3eltr4d
 |-  ( ( ph /\ x e. B ) -> ( ( Id ` C ) ` x ) e. ( x H x ) )