This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-rhm

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

Ref Expression
Assertion df-rhm 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 ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } )