Metamath Proof Explorer

Theorem rhmval0

Description: The set of ring homomorphisms. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 22-Sep-2015) (Revised by AV, 24-Jul-2026)

Ref Expression
Hypotheses rhmval0.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
rhmval0.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
rhmval0.1 ⊢ 1 = ( 1r ‘ 𝑅 )
rhmval0.i ⊢ 𝑁 = ( 1r ‘ 𝑆 )
rhmval0.m ⊢ · = ( .r ‘ 𝑅 )
rhmval0.n ⊢ × = ( .r ‘ 𝑆 )
rhmval0.p ⊢ + = ( +g ‘ 𝑅 )
rhmval0.q ⊢ ⨣ = ( +g ‘ 𝑆 )
Assertion rhmval0 ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) → ( 𝑅 RingHom 𝑆 ) = { 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∣ ( ( 𝑓 ‘ 1 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 rhmval0.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 rhmval0.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
3 rhmval0.1 ⊢ 1 = ( 1r ‘ 𝑅 )
4 rhmval0.i ⊢ 𝑁 = ( 1r ‘ 𝑆 )
5 rhmval0.m ⊢ · = ( .r ‘ 𝑅 )
6 rhmval0.n ⊢ × = ( .r ‘ 𝑆 )
7 rhmval0.p ⊢ + = ( +g ‘ 𝑅 )
8 rhmval0.q ⊢ ⨣ = ( +g ‘ 𝑆 )
9 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
10 9 1 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐵 )
11 10 adantr ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( Base ‘ 𝑟 ) = 𝐵 )
12 fveq2 ⊢ ( 𝑟 = 𝑅 → ( 1r ‘ 𝑟 ) = ( 1r ‘ 𝑅 ) )
13 12 3 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( 1r ‘ 𝑟 ) = 1 )
14 13 fveq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 𝑓 ‘ 1 ) )
15 fveq2 ⊢ ( 𝑠 = 𝑆 → ( 1r ‘ 𝑠 ) = ( 1r ‘ 𝑆 ) )
16 15 4 eqtr4di ⊢ ( 𝑠 = 𝑆 → ( 1r ‘ 𝑠 ) = 𝑁 )
17 14 16 eqeqan12d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ↔ ( 𝑓 ‘ 1 ) = 𝑁 ) )
18 fveq2 ⊢ ( 𝑟 = 𝑅 → ( +g ‘ 𝑟 ) = ( +g ‘ 𝑅 ) )
19 18 7 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( +g ‘ 𝑟 ) = + )
20 19 oveqd ⊢ ( 𝑟 = 𝑅 → ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) = ( 𝑥 + 𝑦 ) )
21 20 fveq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) )
22 fveq2 ⊢ ( 𝑠 = 𝑆 → ( +g ‘ 𝑠 ) = ( +g ‘ 𝑆 ) )
23 22 8 eqtr4di ⊢ ( 𝑠 = 𝑆 → ( +g ‘ 𝑠 ) = ⨣ )
24 23 oveqd ⊢ ( 𝑠 = 𝑆 → ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) )
25 21 24 eqeqan12d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ) )
26 fveq2 ⊢ ( 𝑟 = 𝑅 → ( .r ‘ 𝑟 ) = ( .r ‘ 𝑅 ) )
27 26 5 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( .r ‘ 𝑟 ) = · )
28 27 oveqd ⊢ ( 𝑟 = 𝑅 → ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = ( 𝑥 · 𝑦 ) )
29 28 fveq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) )
30 fveq2 ⊢ ( 𝑠 = 𝑆 → ( .r ‘ 𝑠 ) = ( .r ‘ 𝑆 ) )
31 30 6 eqtr4di ⊢ ( 𝑠 = 𝑆 → ( .r ‘ 𝑠 ) = × )
32 31 oveqd ⊢ ( 𝑠 = 𝑆 → ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) )
33 29 32 eqeqan12d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) )
34 25 33 anbi12d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) )
35 34 2ralbidv ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) )
36 17 35 anbi12d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) ↔ ( ( 𝑓 ‘ 1 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
37 36 rabbidv ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } = { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ 1 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) } )
38 37 csbeq2dv ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } = ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ 1 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) } )
39 11 38 csbeq12dv ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } = ⦋ 𝐵 / 𝑣 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ 1 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) } )
40 fveq2 ⊢ ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
41 40 2 eqtr4di ⊢ ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = 𝐶 )
42 41 adantl ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( Base ‘ 𝑠 ) = 𝐶 )
43 42 csbeq1d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ 1 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) } = ⦋ 𝐶 / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ 1 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) } )
44 43 csbeq2dv ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ⦋ 𝐵 / 𝑣 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ 1 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) } = ⦋ 𝐵 / 𝑣 ⦌ ⦋ 𝐶 / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ 1 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) } )
45 1 fvexi ⊢ 𝐵 ∈ V
46 2 fvexi ⊢ 𝐶 ∈ V
47 oveq12 ⊢ ( ( 𝑤 = 𝐶 ∧ 𝑣 = 𝐵 ) → ( 𝑤 ↑m 𝑣 ) = ( 𝐶 ↑m 𝐵 ) )
48 47 ancoms ⊢ ( ( 𝑣 = 𝐵 ∧ 𝑤 = 𝐶 ) → ( 𝑤 ↑m 𝑣 ) = ( 𝐶 ↑m 𝐵 ) )
49 raleq ⊢ ( 𝑣 = 𝐵 → ( ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) )
50 raleq ⊢ ( 𝑣 = 𝐵 → ( ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) )
51 50 ralbidv ⊢ ( 𝑣 = 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) )
52 49 51 bitrd ⊢ ( 𝑣 = 𝐵 → ( ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) )
53 52 adantr ⊢ ( ( 𝑣 = 𝐵 ∧ 𝑤 = 𝐶 ) → ( ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) )
54 53 anbi2d ⊢ ( ( 𝑣 = 𝐵 ∧ 𝑤 = 𝐶 ) → ( ( ( 𝑓 ‘ 1 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) ↔ ( ( 𝑓 ‘ 1 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
55 48 54 rabeqbidv ⊢ ( ( 𝑣 = 𝐵 ∧ 𝑤 = 𝐶 ) → { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ 1 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) } = { 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∣ ( ( 𝑓 ‘ 1 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) } )
56 45 46 55 csbie2 ⊢ ⦋ 𝐵 / 𝑣 ⦌ ⦋ 𝐶 / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ 1 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) } = { 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∣ ( ( 𝑓 ‘ 1 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) }
57 56 a1i ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ⦋ 𝐵 / 𝑣 ⦌ ⦋ 𝐶 / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ 1 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) } = { 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∣ ( ( 𝑓 ‘ 1 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) } )
58 39 44 57 3eqtrd ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } = { 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∣ ( ( 𝑓 ‘ 1 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) } )
59 df-rhm ⊢ RingHom = ( 𝑟 ∈ Ring , 𝑠 ∈ Ring ↦ ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } )
60 ovex ⊢ ( 𝐶 ↑m 𝐵 ) ∈ V
61 60 rabex ⊢ { 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∣ ( ( 𝑓 ‘ 1 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) } ∈ V
62 58 59 61 ovmpoa ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) → ( 𝑅 RingHom 𝑆 ) = { 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∣ ( ( 𝑓 ‘ 1 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) × ( 𝑓 ‘ 𝑦 ) ) ) ) } )