funcringcsetclem6ALTV

Description: Lemma 6 for funcringcsetcALTV . (Contributed by AV, 15-Feb-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	funcringcsetcALTV.r	$⊢ R = RingCatALTV (U)$
	funcringcsetcALTV.s	$⊢ S = SetCat (U)$
	funcringcsetcALTV.b	$⊢ B = {Base}_{R}$
	funcringcsetcALTV.c	$⊢ C = {Base}_{S}$
	funcringcsetcALTV.u	$⊢ φ \to U \in WUni$
	funcringcsetcALTV.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
	funcringcsetcALTV.g	$⊢ φ \to G = (x \in B, y \in B ⟼ {I ↾}_{(x RingHom y)})$
Assertion	funcringcsetclem6ALTV	$⊢ (φ \land (X \in B \land Y \in B) \land H \in (X RingHom Y)) \to (X G Y) (H) = H$

Step	Hyp	Ref	Expression
1		funcringcsetcALTV.r	$⊢ R = RingCatALTV (U)$
2		funcringcsetcALTV.s	$⊢ S = SetCat (U)$
3		funcringcsetcALTV.b	$⊢ B = {Base}_{R}$
4		funcringcsetcALTV.c	$⊢ C = {Base}_{S}$
5		funcringcsetcALTV.u	$⊢ φ \to U \in WUni$
6		funcringcsetcALTV.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
7		funcringcsetcALTV.g	$⊢ φ \to G = (x \in B, y \in B ⟼ {I ↾}_{(x RingHom y)})$
8	1 2 3 4 5 6 7	funcringcsetclem5ALTV	$⊢ (φ \land (X \in B \land Y \in B)) \to X G Y = {I ↾}_{(X RingHom Y)}$
9	8	3adant3	$⊢ (φ \land (X \in B \land Y \in B) \land H \in (X RingHom Y)) \to X G Y = {I ↾}_{(X RingHom Y)}$
10	9	fveq1d	$⊢ (φ \land (X \in B \land Y \in B) \land H \in (X RingHom Y)) \to (X G Y) (H) = ({I ↾}_{(X RingHom Y)}) (H)$
11		fvresi	$⊢ H \in (X RingHom Y) \to ({I ↾}_{(X RingHom Y)}) (H) = H$
12	11	3ad2ant3	$⊢ (φ \land (X \in B \land Y \in B) \land H \in (X RingHom Y)) \to ({I ↾}_{(X RingHom Y)}) (H) = H$
13	10 12	eqtrd	$⊢ (φ \land (X \in B \land Y \in B) \land H \in (X RingHom Y)) \to (X G Y) (H) = H$

Metamath Proof Explorer