Theorem srhmsubclem3

Description: Lemma 3 for srhmsubc . (Contributed by AV, 19-Feb-2020)

	Ref	Expression
Hypotheses	srhmsubc.s	⊢ ∀ 𝑟 ∈ 𝑆 𝑟 ∈ Ring
	srhmsubc.c	⊢ 𝐶 = ( 𝑈 ∩ 𝑆 )
	srhmsubc.j	⊢ 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
Assertion	srhmsubclem3	⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑋 𝐽 𝑌 ) = ( 𝑋 ( Hom ‘ ( RingCat ‘ 𝑈 ) ) 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		srhmsubc.s	⊢ ∀ 𝑟 ∈ 𝑆 𝑟 ∈ Ring
2		srhmsubc.c	⊢ 𝐶 = ( 𝑈 ∩ 𝑆 )
3		srhmsubc.j	⊢ 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
4	3	a1i	⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) ) )
5		oveq12	⊢ ( ( 𝑟 = 𝑋 ∧ 𝑠 = 𝑌 ) → ( 𝑟 RingHom 𝑠 ) = ( 𝑋 RingHom 𝑌 ) )
6	5	adantl	⊢ ( ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) ∧ ( 𝑟 = 𝑋 ∧ 𝑠 = 𝑌 ) ) → ( 𝑟 RingHom 𝑠 ) = ( 𝑋 RingHom 𝑌 ) )
7		simpl	⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) → 𝑋 ∈ 𝐶 )
8	7	adantl	⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → 𝑋 ∈ 𝐶 )
9		simpr	⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) → 𝑌 ∈ 𝐶 )
10	9	adantl	⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → 𝑌 ∈ 𝐶 )
11		ovexd	⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑋 RingHom 𝑌 ) ∈ V )
12	4 6 8 10 11	ovmpod	⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑋 𝐽 𝑌 ) = ( 𝑋 RingHom 𝑌 ) )
13		eqid	⊢ ( RingCat ‘ 𝑈 ) = ( RingCat ‘ 𝑈 )
14		eqid	⊢ ( Base ‘ ( RingCat ‘ 𝑈 ) ) = ( Base ‘ ( RingCat ‘ 𝑈 ) )
15		simpl	⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → 𝑈 ∈ 𝑉 )
16		eqid	⊢ ( Hom ‘ ( RingCat ‘ 𝑈 ) ) = ( Hom ‘ ( RingCat ‘ 𝑈 ) )
17	1 2	srhmsubclem2	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ∈ ( Base ‘ ( RingCat ‘ 𝑈 ) ) )
18	7 17	sylan2	⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → 𝑋 ∈ ( Base ‘ ( RingCat ‘ 𝑈 ) ) )
19	1 2	srhmsubclem2	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝑌 ∈ 𝐶 ) → 𝑌 ∈ ( Base ‘ ( RingCat ‘ 𝑈 ) ) )
20	9 19	sylan2	⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → 𝑌 ∈ ( Base ‘ ( RingCat ‘ 𝑈 ) ) )
21	13 14 15 16 18 20	ringchom	⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑋 ( Hom ‘ ( RingCat ‘ 𝑈 ) ) 𝑌 ) = ( 𝑋 RingHom 𝑌 ) )
22	12 21	eqtr4d	⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑋 𝐽 𝑌 ) = ( 𝑋 ( Hom ‘ ( RingCat ‘ 𝑈 ) ) 𝑌 ) )