Metamath Proof Explorer

Theorem rhmsubcrngclem1

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

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

Proof

Step Hyp Ref Expression
1 rhmsubcrngc.c 
 |-  C = ( RngCat ` U )
2 rhmsubcrngc.u 
 |-  ( ph -> U e. V )
3 rhmsubcrngc.b 
 |-  ( ph -> B = ( Ring i^i U ) )
4 rhmsubcrngc.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 
 |-  ( Base ` C ) = ( Base ` C )
14 eqid 
 |-  ( Id ` C ) = ( Id ` C )
15 2 adantr 
 |-  ( ( ph /\ x e. B ) -> U e. V )
16 ringrng 
 |-  ( x e. Ring -> x e. Rng )
17 16 anim2i 
 |-  ( ( x e. U /\ x e. Ring ) -> ( x e. U /\ x e. Rng ) )
18 17 ancoms 
 |-  ( ( x e. Ring /\ x e. U ) -> ( x e. U /\ x e. Rng ) )
19 6 18 sylbi 
 |-  ( x e. ( Ring i^i U ) -> ( x e. U /\ x e. Rng ) )
20 19 adantl 
 |-  ( ( ph /\ x e. ( Ring i^i U ) ) -> ( x e. U /\ x e. Rng ) )
21 elin 
 |-  ( x e. ( U i^i Rng ) <-> ( x e. U /\ x e. Rng ) )
22 20 21 sylibr 
 |-  ( ( ph /\ x e. ( Ring i^i U ) ) -> x e. ( U i^i Rng ) )
23 1 13 2 rngcbas 
 |-  ( ph -> ( Base ` C ) = ( U i^i Rng ) )
24 23 adantr 
 |-  ( ( ph /\ x e. ( Ring i^i U ) ) -> ( Base ` C ) = ( U i^i Rng ) )
25 22 24 eleqtrrd 
 |-  ( ( ph /\ x e. ( Ring i^i U ) ) -> x e. ( Base ` C ) )
26 25 ex 
 |-  ( ph -> ( x e. ( Ring i^i U ) -> x e. ( Base ` C ) ) )
27 5 26 sylbid 
 |-  ( ph -> ( x e. B -> x e. ( Base ` C ) ) )
28 27 imp 
 |-  ( ( ph /\ x e. B ) -> x e. ( Base ` C ) )
29 1 13 14 15 28 10 rngcid 
 |-  ( ( ph /\ x e. B ) -> ( ( Id ` C ) ` x ) = ( _I |` ( Base ` x ) ) )
30 4 oveqdr 
 |-  ( ( ph /\ x e. B ) -> ( x H x ) = ( x ( RingHom |` ( B X. B ) ) x ) )
31 eqid 
 |-  ( RingCat ` U ) = ( RingCat ` U )
32 eqid 
 |-  ( Base ` ( RingCat ` U ) ) = ( Base ` ( RingCat ` U ) )
33 eqid 
 |-  ( Hom ` ( RingCat ` U ) ) = ( Hom ` ( RingCat ` U ) )
34 31 32 2 33 ringchomfval 
 |-  ( ph -> ( Hom ` ( RingCat ` U ) ) = ( RingHom |` ( ( Base ` ( RingCat ` U ) ) X. ( Base ` ( RingCat ` U ) ) ) ) )
35 31 32 2 ringcbas 
 |-  ( ph -> ( Base ` ( RingCat ` U ) ) = ( U i^i Ring ) )
36 incom 
 |-  ( Ring i^i U ) = ( U i^i Ring )
37 3 36 eqtrdi 
 |-  ( ph -> B = ( U i^i Ring ) )
38 37 eqcomd 
 |-  ( ph -> ( U i^i Ring ) = B )
39 35 38 eqtrd 
 |-  ( ph -> ( Base ` ( RingCat ` U ) ) = B )
40 39 sqxpeqd 
 |-  ( ph -> ( ( Base ` ( RingCat ` U ) ) X. ( Base ` ( RingCat ` U ) ) ) = ( B X. B ) )
41 40 reseq2d 
 |-  ( ph -> ( RingHom |` ( ( Base ` ( RingCat ` U ) ) X. ( Base ` ( RingCat ` U ) ) ) ) = ( RingHom |` ( B X. B ) ) )
42 34 41 eqtrd 
 |-  ( ph -> ( Hom ` ( RingCat ` U ) ) = ( RingHom |` ( B X. B ) ) )
43 42 adantr 
 |-  ( ( ph /\ x e. B ) -> ( Hom ` ( RingCat ` U ) ) = ( RingHom |` ( B X. B ) ) )
44 43 eqcomd 
 |-  ( ( ph /\ x e. B ) -> ( RingHom |` ( B X. B ) ) = ( Hom ` ( RingCat ` U ) ) )
45 44 oveqd 
 |-  ( ( ph /\ x e. B ) -> ( x ( RingHom |` ( B X. B ) ) x ) = ( x ( Hom ` ( RingCat ` U ) ) x ) )
46 37 eleq2d 
 |-  ( ph -> ( x e. B <-> x e. ( U i^i Ring ) ) )
47 46 biimpa 
 |-  ( ( ph /\ x e. B ) -> x e. ( U i^i Ring ) )
48 35 adantr 
 |-  ( ( ph /\ x e. B ) -> ( Base ` ( RingCat ` U ) ) = ( U i^i Ring ) )
49 47 48 eleqtrrd 
 |-  ( ( ph /\ x e. B ) -> x e. ( Base ` ( RingCat ` U ) ) )
50 31 32 15 33 49 49 ringchom 
 |-  ( ( ph /\ x e. B ) -> ( x ( Hom ` ( RingCat ` U ) ) x ) = ( x RingHom x ) )
51 30 45 50 3eqtrd 
 |-  ( ( ph /\ x e. B ) -> ( x H x ) = ( x RingHom x ) )
52 12 29 51 3eltr4d 
 |-  ( ( ph /\ x e. B ) -> ( ( Id ` C ) ` x ) e. ( x H x ) )