df-rngohom

Description: Define the function which gives the set of ring homomorphisms between two given rings. (Contributed by Jeff Madsen, 19-Jun-2010)

		Ref	Expression
	Assertion	df-rngohom	⊢ RingOpsHom = ( 𝑟 ∈ RingOps , 𝑠 ∈ RingOps ↦ { 𝑓 ∈ ( ran ( 1^st ‘ 𝑠 ) ↑_m ran ( 1^st ‘ 𝑟 ) ) ∣ ( ( 𝑓 ‘ ( GId ‘ ( 2^nd ‘ 𝑟 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑠 ) ) ∧ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑟 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1^st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2^nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crngohom	⊢ RingOpsHom
1		vr	⊢ 𝑟
2		crngo	⊢ RingOps
3		vs	⊢ 𝑠
4		vf	⊢ 𝑓
5		c1st	⊢ 1^st
6	3	cv	⊢ 𝑠
7	6 5	cfv	⊢ ( 1^st ‘ 𝑠 )
8	7	crn	⊢ ran ( 1^st ‘ 𝑠 )
9		cmap	⊢ ↑_m
10	1	cv	⊢ 𝑟
11	10 5	cfv	⊢ ( 1^st ‘ 𝑟 )
12	11	crn	⊢ ran ( 1^st ‘ 𝑟 )
13	8 12 9	co	⊢ ( ran ( 1^st ‘ 𝑠 ) ↑_m ran ( 1^st ‘ 𝑟 ) )
14	4	cv	⊢ 𝑓
15		cgi	⊢ GId
16		c2nd	⊢ 2^nd
17	10 16	cfv	⊢ ( 2^nd ‘ 𝑟 )
18	17 15	cfv	⊢ ( GId ‘ ( 2^nd ‘ 𝑟 ) )
19	18 14	cfv	⊢ ( 𝑓 ‘ ( GId ‘ ( 2^nd ‘ 𝑟 ) ) )
20	6 16	cfv	⊢ ( 2^nd ‘ 𝑠 )
21	20 15	cfv	⊢ ( GId ‘ ( 2^nd ‘ 𝑠 ) )
22	19 21	wceq	⊢ ( 𝑓 ‘ ( GId ‘ ( 2^nd ‘ 𝑟 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑠 ) )
23		vx	⊢ 𝑥
24		vy	⊢ 𝑦
25	23	cv	⊢ 𝑥
26	24	cv	⊢ 𝑦
27	25 26 11	co	⊢ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 )
28	27 14	cfv	⊢ ( 𝑓 ‘ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) )
29	25 14	cfv	⊢ ( 𝑓 ‘ 𝑥 )
30	26 14	cfv	⊢ ( 𝑓 ‘ 𝑦 )
31	29 30 7	co	⊢ ( ( 𝑓 ‘ 𝑥 ) ( 1^st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) )
32	28 31	wceq	⊢ ( 𝑓 ‘ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1^st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) )
33	25 26 17	co	⊢ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑦 )
34	33 14	cfv	⊢ ( 𝑓 ‘ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑦 ) )
35	29 30 20	co	⊢ ( ( 𝑓 ‘ 𝑥 ) ( 2^nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) )
36	34 35	wceq	⊢ ( 𝑓 ‘ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2^nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) )
37	32 36	wa	⊢ ( ( 𝑓 ‘ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1^st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2^nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) )
38	37 24 12	wral	⊢ ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1^st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2^nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) )
39	38 23 12	wral	⊢ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑟 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1^st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2^nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) )
40	22 39	wa	⊢ ( ( 𝑓 ‘ ( GId ‘ ( 2^nd ‘ 𝑟 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑠 ) ) ∧ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑟 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1^st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2^nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) )
41	40 4 13	crab	⊢ { 𝑓 ∈ ( ran ( 1^st ‘ 𝑠 ) ↑_m ran ( 1^st ‘ 𝑟 ) ) ∣ ( ( 𝑓 ‘ ( GId ‘ ( 2^nd ‘ 𝑟 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑠 ) ) ∧ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑟 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1^st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2^nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) }
42	1 3 2 2 41	cmpo	⊢ ( 𝑟 ∈ RingOps , 𝑠 ∈ RingOps ↦ { 𝑓 ∈ ( ran ( 1^st ‘ 𝑠 ) ↑_m ran ( 1^st ‘ 𝑟 ) ) ∣ ( ( 𝑓 ‘ ( GId ‘ ( 2^nd ‘ 𝑟 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑠 ) ) ∧ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑟 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1^st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2^nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } )
43	0 42	wceq	⊢ RingOpsHom = ( 𝑟 ∈ RingOps , 𝑠 ∈ RingOps ↦ { 𝑓 ∈ ( ran ( 1^st ‘ 𝑠 ) ↑_m ran ( 1^st ‘ 𝑟 ) ) ∣ ( ( 𝑓 ‘ ( GId ‘ ( 2^nd ‘ 𝑟 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑠 ) ) ∧ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑟 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1^st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2^nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } )

Metamath Proof Explorer

Definition df-rngohom

Detailed syntax breakdown