Theorem rngchomffvalALTV

Description: The value of the functionalized Hom-set operation in the category of non-unital rings (in a universe) in maps-to notation for an operation. (Contributed by AV, 1-Mar-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rngchomffvalALTV.c	⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
	rngchomffvalALTV.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	rngchomffvalALTV.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	rngchomffvalALTV.h	⊢ 𝐹 = ( Homf ‘ 𝐶 )
Assertion	rngchomffvalALTV	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHom 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rngchomffvalALTV.c	⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
2		rngchomffvalALTV.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		rngchomffvalALTV.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
4		rngchomffvalALTV.h	⊢ 𝐹 = ( Homf ‘ 𝐶 )
5		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
6	1 2 3 5	rngchomfvalALTV	⊢ ( 𝜑 → ( Hom ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHom 𝑦 ) ) )
7		eqid	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHom 𝑦 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHom 𝑦 ) )
8		ovex	⊢ ( 𝑥 RngHom 𝑦 ) ∈ V
9	7 8	fnmpoi	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHom 𝑦 ) ) Fn ( 𝐵 × 𝐵 )
10		fneq1	⊢ ( ( Hom ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHom 𝑦 ) ) → ( ( Hom ‘ 𝐶 ) Fn ( 𝐵 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHom 𝑦 ) ) Fn ( 𝐵 × 𝐵 ) ) )
11	9 10	mpbiri	⊢ ( ( Hom ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHom 𝑦 ) ) → ( Hom ‘ 𝐶 ) Fn ( 𝐵 × 𝐵 ) )
12	4 2 5	fnhomeqhomf	⊢ ( ( Hom ‘ 𝐶 ) Fn ( 𝐵 × 𝐵 ) → 𝐹 = ( Hom ‘ 𝐶 ) )
13	6 11 12	3syl	⊢ ( 𝜑 → 𝐹 = ( Hom ‘ 𝐶 ) )
14	13 6	eqtrd	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 RngHom 𝑦 ) ) )