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

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