This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑈 ) ) 𝑌 ) )