This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rhmsubclem1

Description: Lemma 1 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 rhmsubclem1 
|- ( ph -> H Fn ( R X. R ) )

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 eqid 
 |-  ( x e. R , y e. R |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) ) = ( x e. R , y e. R |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) )
6 ovex 
 |-  ( x GrpHom y ) e. _V
7 6 inex1 
 |-  ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) e. _V
8 5 7 fnmpoi 
 |-  ( x e. R , y e. R |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) ) Fn ( R X. R )
9 4 a1i 
 |-  ( ph -> H = ( RingHom |` ( R X. R ) ) )
10 dfrhm2 
 |-  RingHom = ( x e. Ring , y e. Ring |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) )
11 10 a1i 
 |-  ( ph -> RingHom = ( x e. Ring , y e. Ring |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) ) )
12 11 reseq1d 
 |-  ( ph -> ( RingHom |` ( R X. R ) ) = ( ( x e. Ring , y e. Ring |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) ) |` ( R X. R ) ) )
13 inss1 
 |-  ( Ring i^i U ) C_ Ring
14 3 13 eqsstrdi 
 |-  ( ph -> R C_ Ring )
15 resmpo 
 |-  ( ( R C_ Ring /\ R C_ Ring ) -> ( ( x e. Ring , y e. Ring |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) ) |` ( R X. R ) ) = ( x e. R , y e. R |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) ) )
16 14 14 15 syl2anc 
 |-  ( ph -> ( ( x e. Ring , y e. Ring |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) ) |` ( R X. R ) ) = ( x e. R , y e. R |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) ) )
17 9 12 16 3eqtrd 
 |-  ( ph -> H = ( x e. R , y e. R |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) ) )
18 17 fneq1d 
 |-  ( ph -> ( H Fn ( R X. R ) <-> ( x e. R , y e. R |-> ( ( x GrpHom y ) i^i ( ( mulGrp ` x ) MndHom ( mulGrp ` y ) ) ) ) Fn ( R X. R ) ) )
19 8 18 mpbiri 
 |-  ( ph -> H Fn ( R X. R ) )