srhmsubcALTVlem2

Description: Lemma 2 for srhmsubcALTV . (Contributed by AV, 19-Feb-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	srhmsubcALTV.s	$⊢ \forall r \in S r \in Ring$
	srhmsubcALTV.c	$⊢ C = U \cap S$
	srhmsubcALTV.j	$⊢ J = (r \in C, s \in C ⟼ r RingHom s)$
Assertion	srhmsubcALTVlem2	$⊢ (U \in V \land (X \in C \land Y \in C)) \to X J Y = X Hom (RingCatALTV (U)) Y$

Proof

Step	Hyp	Ref	Expression
1		srhmsubcALTV.s	$⊢ \forall r \in S r \in Ring$
2		srhmsubcALTV.c	$⊢ C = U \cap S$
3		srhmsubcALTV.j	$⊢ J = (r \in C, s \in C ⟼ r RingHom s)$
4	3	a1i	$⊢ (U \in V \land (X \in C \land Y \in C)) \to J = (r \in C, s \in C ⟼ r RingHom s)$
5		oveq12	$⊢ (r = X \land s = Y) \to r RingHom s = X RingHom Y$
6	5	adantl	$⊢ ((U \in V \land (X \in C \land Y \in C)) \land (r = X \land s = Y)) \to r RingHom s = X RingHom Y$
7		simpl	$⊢ (X \in C \land Y \in C) \to X \in C$
8	7	adantl	$⊢ (U \in V \land (X \in C \land Y \in C)) \to X \in C$
9		simpr	$⊢ (X \in C \land Y \in C) \to Y \in C$
10	9	adantl	$⊢ (U \in V \land (X \in C \land Y \in C)) \to Y \in C$
11		ovexd	$⊢ (U \in V \land (X \in C \land Y \in C)) \to X RingHom Y \in V$
12	4 6 8 10 11	ovmpod	$⊢ (U \in V \land (X \in C \land Y \in C)) \to X J Y = X RingHom Y$
13		eqid	$⊢ RingCatALTV (U) = RingCatALTV (U)$
14		eqid	$⊢ {Base}_{RingCatALTV (U)} = {Base}_{RingCatALTV (U)}$
15		simpl	$⊢ (U \in V \land (X \in C \land Y \in C)) \to U \in V$
16		eqid	$⊢ Hom (RingCatALTV (U)) = Hom (RingCatALTV (U))$
17	1 2	srhmsubcALTVlem1	$⊢ (U \in V \land X \in C) \to X \in {Base}_{RingCatALTV (U)}$
18	7 17	sylan2	$⊢ (U \in V \land (X \in C \land Y \in C)) \to X \in {Base}_{RingCatALTV (U)}$
19	1 2	srhmsubcALTVlem1	$⊢ (U \in V \land Y \in C) \to Y \in {Base}_{RingCatALTV (U)}$
20	9 19	sylan2	$⊢ (U \in V \land (X \in C \land Y \in C)) \to Y \in {Base}_{RingCatALTV (U)}$
21	13 14 15 16 18 20	ringchomALTV	$⊢ (U \in V \land (X \in C \land Y \in C)) \to X Hom (RingCatALTV (U)) Y = X RingHom Y$
22	12 21	eqtr4d	$⊢ (U \in V \land (X \in C \land Y \in C)) \to X J Y = X Hom (RingCatALTV (U)) Y$

Metamath Proof Explorer

Theorem srhmsubcALTVlem2

Proof