Theorem rngchomrnghmresALTV

Description: The value of the functionalized Hom-set operation in the category of non-unital rings (in a universe) as restriction of the non-unital ring homomorphisms. (Contributed by AV, 2-Mar-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rngchomrnghmresALTV.c	⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
	rngchomrnghmresALTV.b	⊢ 𝐵 = ( Rng ∩ 𝑈 )
	rngchomrnghmresALTV.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	rngchomrnghmresALTV.f	⊢ 𝐹 = ( Homf ‘ 𝐶 )
Assertion	rngchomrnghmresALTV	⊢ ( 𝜑 → 𝐹 = ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rngchomrnghmresALTV.c	⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
2		rngchomrnghmresALTV.b	⊢ 𝐵 = ( Rng ∩ 𝑈 )
3		rngchomrnghmresALTV.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
4		rngchomrnghmresALTV.f	⊢ 𝐹 = ( Homf ‘ 𝐶 )
5		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6	1 5 3	rngcbasALTV	⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( 𝑈 ∩ Rng ) )
7		inss2	⊢ ( 𝑈 ∩ Rng ) ⊆ Rng
8	6 7	eqsstrdi	⊢ ( 𝜑 → ( Base ‘ 𝐶 ) ⊆ Rng )
9		resmpo	⊢ ( ( ( Base ‘ 𝐶 ) ⊆ Rng ∧ ( Base ‘ 𝐶 ) ⊆ Rng ) → ( ( 𝑥 ∈ Rng , 𝑦 ∈ Rng ↦ ( 𝑥 RngHomo 𝑦 ) ) ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 RngHomo 𝑦 ) ) )
10	8 8 9	syl2anc	⊢ ( 𝜑 → ( ( 𝑥 ∈ Rng , 𝑦 ∈ Rng ↦ ( 𝑥 RngHomo 𝑦 ) ) ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 RngHomo 𝑦 ) ) )
11		df-rnghomo	⊢ RngHomo = ( 𝑟 ∈ Rng , 𝑠 ∈ Rng ↦ ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) } )
12		ovex	⊢ ( 𝑤 ↑m 𝑣 ) ∈ V
13	12	rabex	⊢ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) } ∈ V
14	13	csbex	⊢ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) } ∈ V
15	14	csbex	⊢ ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) } ∈ V
16	11 15	fnmpoi	⊢ RngHomo Fn ( Rng × Rng )
17	16	a1i	⊢ ( 𝜑 → RngHomo Fn ( Rng × Rng ) )
18		fnov	⊢ ( RngHomo Fn ( Rng × Rng ) ↔ RngHomo = ( 𝑥 ∈ Rng , 𝑦 ∈ Rng ↦ ( 𝑥 RngHomo 𝑦 ) ) )
19	17 18	sylib	⊢ ( 𝜑 → RngHomo = ( 𝑥 ∈ Rng , 𝑦 ∈ Rng ↦ ( 𝑥 RngHomo 𝑦 ) ) )
20		incom	⊢ ( 𝑈 ∩ Rng ) = ( Rng ∩ 𝑈 )
21	20	a1i	⊢ ( 𝜑 → ( 𝑈 ∩ Rng ) = ( Rng ∩ 𝑈 ) )
22	2	a1i	⊢ ( 𝜑 → 𝐵 = ( Rng ∩ 𝑈 ) )
23	21 6 22	3eqtr4rd	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
24	23	sqxpeqd	⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
25	19 24	reseq12d	⊢ ( 𝜑 → ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) = ( ( 𝑥 ∈ Rng , 𝑦 ∈ Rng ↦ ( 𝑥 RngHomo 𝑦 ) ) ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) )
26	1 5 3 4	rngchomffvalALTV	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 RngHomo 𝑦 ) ) )
27	10 25 26	3eqtr4rd	⊢ ( 𝜑 → 𝐹 = ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) )