Metamath Proof Explorer


Theorem rhmsubclem1

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

Ref Expression
Hypotheses rngcrescrhm.u φUV
rngcrescrhm.c C=RngCatU
rngcrescrhm.r φR=RingU
rngcrescrhm.h H=RingHomR×R
Assertion rhmsubclem1 φHFnR×R

Proof

Step Hyp Ref Expression
1 rngcrescrhm.u φUV
2 rngcrescrhm.c C=RngCatU
3 rngcrescrhm.r φR=RingU
4 rngcrescrhm.h H=RingHomR×R
5 eqid xR,yRxGrpHomymulGrpxMndHommulGrpy=xR,yRxGrpHomymulGrpxMndHommulGrpy
6 ovex xGrpHomyV
7 6 inex1 xGrpHomymulGrpxMndHommulGrpyV
8 5 7 fnmpoi xR,yRxGrpHomymulGrpxMndHommulGrpyFnR×R
9 4 a1i φH=RingHomR×R
10 dfrhm2 RingHom=xRing,yRingxGrpHomymulGrpxMndHommulGrpy
11 10 a1i φRingHom=xRing,yRingxGrpHomymulGrpxMndHommulGrpy
12 11 reseq1d φRingHomR×R=xRing,yRingxGrpHomymulGrpxMndHommulGrpyR×R
13 inss1 RingURing
14 3 13 eqsstrdi φRRing
15 resmpo RRingRRingxRing,yRingxGrpHomymulGrpxMndHommulGrpyR×R=xR,yRxGrpHomymulGrpxMndHommulGrpy
16 14 14 15 syl2anc φxRing,yRingxGrpHomymulGrpxMndHommulGrpyR×R=xR,yRxGrpHomymulGrpxMndHommulGrpy
17 9 12 16 3eqtrd φH=xR,yRxGrpHomymulGrpxMndHommulGrpy
18 17 fneq1d φHFnR×RxR,yRxGrpHomymulGrpxMndHommulGrpyFnR×R
19 8 18 mpbiri φHFnR×R