Metamath Proof Explorer


Theorem rhmsubclem2

Description: Lemma 2 for rhmsubc . (Contributed by AV, 2-Mar-2020)

Ref Expression
Hypotheses rngcrescrhm.u ( 𝜑𝑈𝑉 )
rngcrescrhm.c 𝐶 = ( RngCat ‘ 𝑈 )
rngcrescrhm.r ( 𝜑𝑅 = ( Ring ∩ 𝑈 ) )
rngcrescrhm.h 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
Assertion rhmsubclem2 ( ( 𝜑𝑋𝑅𝑌𝑅 ) → ( 𝑋 𝐻 𝑌 ) = ( 𝑋 RingHom 𝑌 ) )

Proof

Step Hyp Ref Expression
1 rngcrescrhm.u ( 𝜑𝑈𝑉 )
2 rngcrescrhm.c 𝐶 = ( RngCat ‘ 𝑈 )
3 rngcrescrhm.r ( 𝜑𝑅 = ( Ring ∩ 𝑈 ) )
4 rngcrescrhm.h 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
5 opelxpi ( ( 𝑋𝑅𝑌𝑅 ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝑅 × 𝑅 ) )
6 5 3adant1 ( ( 𝜑𝑋𝑅𝑌𝑅 ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝑅 × 𝑅 ) )
7 6 fvresd ( ( 𝜑𝑋𝑅𝑌𝑅 ) → ( ( RingHom ↾ ( 𝑅 × 𝑅 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( RingHom ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
8 df-ov ( 𝑋 𝐻 𝑌 ) = ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
9 4 fveq1i ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( RingHom ↾ ( 𝑅 × 𝑅 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ )
10 8 9 eqtri ( 𝑋 𝐻 𝑌 ) = ( ( RingHom ↾ ( 𝑅 × 𝑅 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ )
11 df-ov ( 𝑋 RingHom 𝑌 ) = ( RingHom ‘ ⟨ 𝑋 , 𝑌 ⟩ )
12 7 10 11 3eqtr4g ( ( 𝜑𝑋𝑅𝑌𝑅 ) → ( 𝑋 𝐻 𝑌 ) = ( 𝑋 RingHom 𝑌 ) )