Metamath Proof Explorer

Theorem rhmsubcALTVlem3

Description: Lemma 3 for rhmsubcALTV . (Contributed by AV, 2-Mar-2020) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 rngcrescrhmALTV.u 
 |-  ( ph -> U e. V )
2 rngcrescrhmALTV.c 
 |-  C = ( RngCatALTV ` U )
3 rngcrescrhmALTV.r 
 |-  ( ph -> R = ( Ring i^i U ) )
4 rngcrescrhmALTV.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 biimtrdi 
 |-  ( 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 1 adantr 
 |-  ( ( ph /\ x e. R ) -> U e. V )
13 eqid 
 |-  ( RngCatALTV ` U ) = ( RngCatALTV ` U )
14 eqid 
 |-  ( Base ` ( RngCatALTV ` U ) ) = ( Base ` ( RngCatALTV ` U ) )
15 13 14 rngccatidALTV 
 |-  ( U e. V -> ( ( RngCatALTV ` U ) e. Cat /\ ( Id ` ( RngCatALTV ` U ) ) = ( y e. ( Base ` ( RngCatALTV ` U ) ) |-> ( _I |` ( Base ` y ) ) ) ) )
16 simpr 
 |-  ( ( ( RngCatALTV ` U ) e. Cat /\ ( Id ` ( RngCatALTV ` U ) ) = ( y e. ( Base ` ( RngCatALTV ` U ) ) |-> ( _I |` ( Base ` y ) ) ) ) -> ( Id ` ( RngCatALTV ` U ) ) = ( y e. ( Base ` ( RngCatALTV ` U ) ) |-> ( _I |` ( Base ` y ) ) ) )
17 12 15 16 3syl 
 |-  ( ( ph /\ x e. R ) -> ( Id ` ( RngCatALTV ` U ) ) = ( y e. ( Base ` ( RngCatALTV ` U ) ) |-> ( _I |` ( Base ` y ) ) ) )
18 fveq2 
 |-  ( y = x -> ( Base ` y ) = ( Base ` x ) )
19 18 reseq2d 
 |-  ( y = x -> ( _I |` ( Base ` y ) ) = ( _I |` ( Base ` x ) ) )
20 19 adantl 
 |-  ( ( ( ph /\ x e. R ) /\ y = x ) -> ( _I |` ( Base ` y ) ) = ( _I |` ( Base ` x ) ) )
21 incom 
 |-  ( Ring i^i U ) = ( U i^i Ring )
22 3 21 eqtrdi 
 |-  ( ph -> R = ( U i^i Ring ) )
23 22 eleq2d 
 |-  ( ph -> ( x e. R <-> x e. ( U i^i Ring ) ) )
24 ringrng 
 |-  ( x e. Ring -> x e. Rng )
25 24 anim2i 
 |-  ( ( x e. U /\ x e. Ring ) -> ( x e. U /\ x e. Rng ) )
26 elin 
 |-  ( x e. ( U i^i Ring ) <-> ( x e. U /\ x e. Ring ) )
27 elin 
 |-  ( x e. ( U i^i Rng ) <-> ( x e. U /\ x e. Rng ) )
28 25 26 27 3imtr4i 
 |-  ( x e. ( U i^i Ring ) -> x e. ( U i^i Rng ) )
29 23 28 biimtrdi 
 |-  ( ph -> ( x e. R -> x e. ( U i^i Rng ) ) )
30 29 imp 
 |-  ( ( ph /\ x e. R ) -> x e. ( U i^i Rng ) )
31 2 eqcomi 
 |-  ( RngCatALTV ` U ) = C
32 31 fveq2i 
 |-  ( Base ` ( RngCatALTV ` U ) ) = ( Base ` C )
33 2 32 1 rngcbasALTV 
 |-  ( ph -> ( Base ` ( RngCatALTV ` U ) ) = ( U i^i Rng ) )
34 33 adantr 
 |-  ( ( ph /\ x e. R ) -> ( Base ` ( RngCatALTV ` U ) ) = ( U i^i Rng ) )
35 30 34 eleqtrrd 
 |-  ( ( ph /\ x e. R ) -> x e. ( Base ` ( RngCatALTV ` U ) ) )
36 fvexd 
 |-  ( ( ph /\ x e. R ) -> ( Base ` x ) e. _V )
37 36 resiexd 
 |-  ( ( ph /\ x e. R ) -> ( _I |` ( Base ` x ) ) e. _V )
38 17 20 35 37 fvmptd 
 |-  ( ( ph /\ x e. R ) -> ( ( Id ` ( RngCatALTV ` U ) ) ` x ) = ( _I |` ( Base ` x ) ) )
39 1 2 3 4 rhmsubcALTVlem2 
 |-  ( ( ph /\ x e. R /\ x e. R ) -> ( x H x ) = ( x RingHom x ) )
40 39 3anidm23 
 |-  ( ( ph /\ x e. R ) -> ( x H x ) = ( x RingHom x ) )
41 11 38 40 3eltr4d 
 |-  ( ( ph /\ x e. R ) -> ( ( Id ` ( RngCatALTV ` U ) ) ` x ) e. ( x H x ) )