Definition df-rnghom

Description: Define the set of ring homomorphisms from r to s . (Contributed by Stefan O'Rear, 7-Mar-2015)

	Ref	Expression
Assertion	df-rnghom	⊢ RingHom = ( 𝑟 ∈ Ring , 𝑠 ∈ Ring ↦ ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crh	⊢ RingHom
1		vr	⊢ 𝑟
2		crg	⊢ Ring
3		vs	⊢ 𝑠
4		cbs	⊢ Base
5	1	cv	⊢ 𝑟
6	5 4	cfv	⊢ ( Base ‘ 𝑟 )
7		vv	⊢ 𝑣
8	3	cv	⊢ 𝑠
9	8 4	cfv	⊢ ( Base ‘ 𝑠 )
10		vw	⊢ 𝑤
11		vf	⊢ 𝑓
12	10	cv	⊢ 𝑤
13		cmap	⊢ ↑m
14	7	cv	⊢ 𝑣
15	12 14 13	co	⊢ ( 𝑤 ↑m 𝑣 )
16	11	cv	⊢ 𝑓
17		cur	⊢ 1r
18	5 17	cfv	⊢ ( 1r ‘ 𝑟 )
19	18 16	cfv	⊢ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) )
20	8 17	cfv	⊢ ( 1r ‘ 𝑠 )
21	19 20	wceq	⊢ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 )
22		vx	⊢ 𝑥
23		vy	⊢ 𝑦
24	22	cv	⊢ 𝑥
25		cplusg	⊢ +g
26	5 25	cfv	⊢ ( +g ‘ 𝑟 )
27	23	cv	⊢ 𝑦
28	24 27 26	co	⊢ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 )
29	28 16	cfv	⊢ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) )
30	24 16	cfv	⊢ ( 𝑓 ‘ 𝑥 )
31	8 25	cfv	⊢ ( +g ‘ 𝑠 )
32	27 16	cfv	⊢ ( 𝑓 ‘ 𝑦 )
33	30 32 31	co	⊢ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) )
34	29 33	wceq	⊢ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) )
35		cmulr	⊢ .r
36	5 35	cfv	⊢ ( .r ‘ 𝑟 )
37	24 27 36	co	⊢ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 )
38	37 16	cfv	⊢ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) )
39	8 35	cfv	⊢ ( .r ‘ 𝑠 )
40	30 32 39	co	⊢ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) )
41	38 40	wceq	⊢ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) )
42	34 41	wa	⊢ ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) )
43	42 23 14	wral	⊢ ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) )
44	43 22 14	wral	⊢ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) )
45	21 44	wa	⊢ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) )
46	45 11 15	crab	⊢ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) }
47	10 9 46	csb	⊢ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) }
48	7 6 47	csb	⊢ ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) }
49	1 3 2 2 48	cmpo	⊢ ( 𝑟 ∈ Ring , 𝑠 ∈ Ring ↦ ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } )
50	0 49	wceq	⊢ RingHom = ( 𝑟 ∈ Ring , 𝑠 ∈ Ring ↦ ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } )