Metamath Proof Explorer


Definition 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 RngHom = ( 𝑟 ∈ RingOps , 𝑠 ∈ RingOps ↦ { 𝑓 ∈ ( ran ( 1st𝑠 ) ↑m ran ( 1st𝑟 ) ) ∣ ( ( 𝑓 ‘ ( GId ‘ ( 2nd𝑟 ) ) ) = ( GId ‘ ( 2nd𝑠 ) ) ∧ ∀ 𝑥 ∈ ran ( 1st𝑟 ) ∀ 𝑦 ∈ ran ( 1st𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( 1st𝑟 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( 1st𝑠 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2nd𝑟 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( 2nd𝑠 ) ( 𝑓𝑦 ) ) ) ) } )

Detailed syntax breakdown

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