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

Metamath Proof Explorer

Definition df-rnghm

Description: Define the set of non-unital ring homomorphisms from r to s . (Contributed by AV, 20-Feb-2020)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 crnghm ⊢ RngHom
1 vr ⊢ 𝑟
2 crng ⊢ Rng
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 vx ⊢ 𝑥
17 vy ⊢ 𝑦
18 11 cv ⊢ 𝑓
19 16 cv ⊢ 𝑥
20 cplusg ⊢ +g
21 5 20 cfv ⊢ ( +g ‘ 𝑟 )
22 17 cv ⊢ 𝑦
23 19 22 21 co ⊢ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 )
24 23 18 cfv ⊢ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) )
25 19 18 cfv ⊢ ( 𝑓 ‘ 𝑥 )
26 8 20 cfv ⊢ ( +g ‘ 𝑠 )
27 22 18 cfv ⊢ ( 𝑓 ‘ 𝑦 )
28 25 27 26 co ⊢ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) )
29 24 28 wceq ⊢ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) )
30 cmulr ⊢ .r
31 5 30 cfv ⊢ ( .r ‘ 𝑟 )
32 19 22 31 co ⊢ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 )
33 32 18 cfv ⊢ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) )
34 8 30 cfv ⊢ ( .r ‘ 𝑠 )
35 25 27 34 co ⊢ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) )
36 33 35 wceq ⊢ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) )
37 29 36 wa ⊢ ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) )
38 37 17 14 wral ⊢ ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) )
39 38 16 14 wral ⊢ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) )
40 39 11 15 crab ⊢ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) }
41 10 9 40 csb ⊢ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) }
42 7 6 41 csb ⊢ ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) }
43 1 3 2 2 42 cmpo ⊢ ( 𝑟 ∈ Rng , 𝑠 ∈ Rng ↦ ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) } )
44 0 43 wceq ⊢ RngHom = ( 𝑟 ∈ Rng , 𝑠 ∈ Rng ↦ ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) } )