Metamath Proof Explorer

Theorem rhmsubcALTVlem1

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

		Ref	Expression
	Hypotheses	rngcrescrhmALTV.u	$⊢ φ \to U \in V$
		rngcrescrhmALTV.c	$⊢ C = RngCatALTV (U)$
		rngcrescrhmALTV.r	$⊢ φ \to R = Ring \cap U$
		rngcrescrhmALTV.h	$⊢ H = {RingHom ↾}_{(R \times R)}$
	Assertion	rhmsubcALTVlem1	$⊢ φ \to H Fn (R \times R)$

Proof

Step	Hyp	Ref	Expression
1		rngcrescrhmALTV.u	$⊢ φ \to U \in V$
2		rngcrescrhmALTV.c	$⊢ C = RngCatALTV (U)$
3		rngcrescrhmALTV.r	$⊢ φ \to R = Ring \cap U$
4		rngcrescrhmALTV.h	$⊢ H = {RingHom ↾}_{(R \times R)}$
5		eqid	$⊢ (x \in R, y \in R ⟼ (x GrpHom y) \cap ({mulGrp}_{x} MndHom {mulGrp}_{y})) = (x \in R, y \in R ⟼ (x GrpHom y) \cap ({mulGrp}_{x} MndHom {mulGrp}_{y}))$
6		ovex	$⊢ x GrpHom y \in V$
7	6	inex1	$⊢ (x GrpHom y) \cap ({mulGrp}_{x} MndHom {mulGrp}_{y}) \in V$
8	5 7	fnmpoi	$⊢ (x \in R, y \in R ⟼ (x GrpHom y) \cap ({mulGrp}_{x} MndHom {mulGrp}_{y})) Fn (R \times R)$
9	4	a1i	$⊢ φ \to H = {RingHom ↾}_{(R \times R)}$
10		dfrhm2	$⊢ RingHom = (x \in Ring, y \in Ring ⟼ (x GrpHom y) \cap ({mulGrp}_{x} MndHom {mulGrp}_{y}))$
11	10	a1i	$⊢ φ \to RingHom = (x \in Ring, y \in Ring ⟼ (x GrpHom y) \cap ({mulGrp}_{x} MndHom {mulGrp}_{y}))$
12	11	reseq1d	$⊢ φ \to {RingHom ↾}_{(R \times R)} = {(x \in Ring, y \in Ring ⟼ (x GrpHom y) \cap ({mulGrp}_{x} MndHom {mulGrp}_{y})) ↾}_{(R \times R)}$
13		inss1	$⊢ Ring \cap U \subseteq Ring$
14	3 13	eqsstrdi	$⊢ φ \to R \subseteq Ring$
15		resmpo	$⊢ (R \subseteq Ring \land R \subseteq Ring) \to {(x \in Ring, y \in Ring ⟼ (x GrpHom y) \cap ({mulGrp}_{x} MndHom {mulGrp}_{y})) ↾}_{(R \times R)} = (x \in R, y \in R ⟼ (x GrpHom y) \cap ({mulGrp}_{x} MndHom {mulGrp}_{y}))$
16	14 14 15	syl2anc	$⊢ φ \to {(x \in Ring, y \in Ring ⟼ (x GrpHom y) \cap ({mulGrp}_{x} MndHom {mulGrp}_{y})) ↾}_{(R \times R)} = (x \in R, y \in R ⟼ (x GrpHom y) \cap ({mulGrp}_{x} MndHom {mulGrp}_{y}))$
17	9 12 16	3eqtrd	$⊢ φ \to H = (x \in R, y \in R ⟼ (x GrpHom y) \cap ({mulGrp}_{x} MndHom {mulGrp}_{y}))$
18	17	fneq1d	$⊢ φ \to (H Fn (R \times R) \leftrightarrow (x \in R, y \in R ⟼ (x GrpHom y) \cap ({mulGrp}_{x} MndHom {mulGrp}_{y})) Fn (R \times R))$
19	8 18	mpbiri	$⊢ φ \to H Fn (R \times R)$