Theorem rhmsubcALTVlem2

Description: Lemma 2 for rhmsubcALTV . (Contributed by AV, 2-Mar-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rngcrescrhmALTV.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	rngcrescrhmALTV.c	⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
	rngcrescrhmALTV.r	⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
	rngcrescrhmALTV.h	⊢ 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
Assertion	rhmsubcALTVlem2	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) → ( 𝑋 𝐻 𝑌 ) = ( 𝑋 RingHom 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		rngcrescrhmALTV.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
2		rngcrescrhmALTV.c	⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
3		rngcrescrhmALTV.r	⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
4		rngcrescrhmALTV.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 𝑌 ) )