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 biimtrdi 
 |-  ( 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 biimtrdi 
 |-  ( 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 ) )