Metamath Proof Explorer


Theorem rhmsubclem3

Description: Lemma 3 for rhmsubc . (Contributed by AV, 2-Mar-2020)

Ref Expression
Hypotheses rngcrescrhm.u
|- ( ph -> U e. V )
rngcrescrhm.c
|- C = ( RngCat ` U )
rngcrescrhm.r
|- ( ph -> R = ( Ring i^i U ) )
rngcrescrhm.h
|- H = ( RingHom |` ( R X. R ) )
Assertion rhmsubclem3
|- ( ( ph /\ x e. R ) -> ( ( Id ` ( RngCat ` U ) ) ` x ) e. ( x H x ) )

Proof

Step Hyp Ref Expression
1 rngcrescrhm.u
 |-  ( ph -> U e. V )
2 rngcrescrhm.c
 |-  C = ( RngCat ` U )
3 rngcrescrhm.r
 |-  ( ph -> R = ( Ring i^i U ) )
4 rngcrescrhm.h
 |-  H = ( RingHom |` ( R X. R ) )
5 3 eleq2d
 |-  ( ph -> ( x e. R <-> x e. ( Ring i^i U ) ) )
6 elinel1
 |-  ( x e. ( Ring i^i U ) -> x e. Ring )
7 5 6 syl6bi
 |-  ( ph -> ( x e. R -> x e. Ring ) )
8 7 imp
 |-  ( ( ph /\ x e. R ) -> x e. Ring )
9 eqid
 |-  ( Base ` x ) = ( Base ` x )
10 9 idrhm
 |-  ( x e. Ring -> ( _I |` ( Base ` x ) ) e. ( x RingHom x ) )
11 8 10 syl
 |-  ( ( ph /\ x e. R ) -> ( _I |` ( Base ` x ) ) e. ( x RingHom x ) )
12 eqid
 |-  ( Base ` C ) = ( Base ` C )
13 2 eqcomi
 |-  ( RngCat ` U ) = C
14 13 fveq2i
 |-  ( Id ` ( RngCat ` U ) ) = ( Id ` C )
15 1 adantr
 |-  ( ( ph /\ x e. R ) -> U e. V )
16 incom
 |-  ( Ring i^i U ) = ( U i^i Ring )
17 ringssrng
 |-  Ring C_ Rng
18 sslin
 |-  ( Ring C_ Rng -> ( U i^i Ring ) C_ ( U i^i Rng ) )
19 17 18 mp1i
 |-  ( ph -> ( U i^i Ring ) C_ ( U i^i Rng ) )
20 16 19 eqsstrid
 |-  ( ph -> ( Ring i^i U ) C_ ( U i^i Rng ) )
21 2 12 1 rngcbas
 |-  ( ph -> ( Base ` C ) = ( U i^i Rng ) )
22 20 3 21 3sstr4d
 |-  ( ph -> R C_ ( Base ` C ) )
23 22 sselda
 |-  ( ( ph /\ x e. R ) -> x e. ( Base ` C ) )
24 2 12 14 15 23 9 rngcid
 |-  ( ( ph /\ x e. R ) -> ( ( Id ` ( RngCat ` U ) ) ` x ) = ( _I |` ( Base ` x ) ) )
25 1 2 3 4 rhmsubclem2
 |-  ( ( ph /\ x e. R /\ x e. R ) -> ( x H x ) = ( x RingHom x ) )
26 25 3anidm23
 |-  ( ( ph /\ x e. R ) -> ( x H x ) = ( x RingHom x ) )
27 11 24 26 3eltr4d
 |-  ( ( ph /\ x e. R ) -> ( ( Id ` ( RngCat ` U ) ) ` x ) e. ( x H x ) )