Theorem srhmsubcALTVlem2

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

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

Proof

Step	Hyp	Ref	Expression
1		srhmsubcALTV.s	⊢ ∀ 𝑟 ∈ 𝑆 𝑟 ∈ Ring
2		srhmsubcALTV.c	⊢ 𝐶 = ( 𝑈 ∩ 𝑆 )
3		srhmsubcALTV.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	⊢ ( RingCatALTV ‘ 𝑈 ) = ( RingCatALTV ‘ 𝑈 )
14		eqid	⊢ ( Base ‘ ( RingCatALTV ‘ 𝑈 ) ) = ( Base ‘ ( RingCatALTV ‘ 𝑈 ) )
15		simpl	⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → 𝑈 ∈ 𝑉 )
16		eqid	⊢ ( Hom ‘ ( RingCatALTV ‘ 𝑈 ) ) = ( Hom ‘ ( RingCatALTV ‘ 𝑈 ) )
17	1 2	srhmsubcALTVlem1	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ∈ ( Base ‘ ( RingCatALTV ‘ 𝑈 ) ) )
18	7 17	sylan2	⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → 𝑋 ∈ ( Base ‘ ( RingCatALTV ‘ 𝑈 ) ) )
19	1 2	srhmsubcALTVlem1	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝑌 ∈ 𝐶 ) → 𝑌 ∈ ( Base ‘ ( RingCatALTV ‘ 𝑈 ) ) )
20	9 19	sylan2	⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → 𝑌 ∈ ( Base ‘ ( RingCatALTV ‘ 𝑈 ) ) )
21	13 14 15 16 18 20	ringchomALTV	⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑋 ( Hom ‘ ( RingCatALTV ‘ 𝑈 ) ) 𝑌 ) = ( 𝑋 RingHom 𝑌 ) )
22	12 21	eqtr4d	⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑋 𝐽 𝑌 ) = ( 𝑋 ( Hom ‘ ( RingCatALTV ‘ 𝑈 ) ) 𝑌 ) )