srhmsubclem3

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

Proof

Step	Hyp	Ref	Expression
1		srhmsubc.s	$⊢ \forall r \in S r \in Ring$
2		srhmsubc.c	$⊢ C = U \cap S$
3		srhmsubc.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	$⊢ RingCat (U) = RingCat (U)$
14		eqid	$⊢ {Base}_{RingCat (U)} = {Base}_{RingCat (U)}$
15		simpl	$⊢ (U \in V \land (X \in C \land Y \in C)) \to U \in V$
16		eqid	$⊢ Hom (RingCat (U)) = Hom (RingCat (U))$
17	1 2	srhmsubclem2	$⊢ (U \in V \land X \in C) \to X \in {Base}_{RingCat (U)}$
18	7 17	sylan2	$⊢ (U \in V \land (X \in C \land Y \in C)) \to X \in {Base}_{RingCat (U)}$
19	1 2	srhmsubclem2	$⊢ (U \in V \land Y \in C) \to Y \in {Base}_{RingCat (U)}$
20	9 19	sylan2	$⊢ (U \in V \land (X \in C \land Y \in C)) \to Y \in {Base}_{RingCat (U)}$
21	13 14 15 16 18 20	ringchom	$⊢ (U \in V \land (X \in C \land Y \in C)) \to X Hom (RingCat (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 (RingCat (U)) Y$

Metamath Proof Explorer

Theorem srhmsubclem3

Proof