Step |
Hyp |
Ref |
Expression |
1 |
|
isrnghm.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
2 |
|
isrnghm.t |
⊢ · = ( .r ‘ 𝑅 ) |
3 |
|
isrnghm.m |
⊢ ∗ = ( .r ‘ 𝑆 ) |
4 |
|
rnghmrcl |
⊢ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) → ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) ) |
5 |
|
eqid |
⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) |
6 |
|
eqid |
⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) |
7 |
|
eqid |
⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 ) |
8 |
1 2 3 5 6 7
|
rnghmval |
⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) → ( 𝑅 RngHomo 𝑆 ) = { 𝑓 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐵 ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ∗ ( 𝑓 ‘ 𝑦 ) ) ) } ) |
9 |
8
|
eleq2d |
⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) → ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐵 ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ∗ ( 𝑓 ‘ 𝑦 ) ) ) } ) ) |
10 |
|
fveq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) ) |
11 |
|
fveq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) |
12 |
|
fveq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) |
13 |
11 12
|
oveq12d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) |
14 |
10 13
|
eqeq12d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) |
15 |
|
fveq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) ) |
16 |
11 12
|
oveq12d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑥 ) ∗ ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) |
17 |
15 16
|
eqeq12d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ∗ ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) ) |
18 |
14 17
|
anbi12d |
⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ∗ ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) ) ) |
19 |
18
|
2ralbidv |
⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ∗ ( 𝑓 ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) ) ) |
20 |
19
|
elrab |
⊢ ( 𝐹 ∈ { 𝑓 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐵 ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ∗ ( 𝑓 ‘ 𝑦 ) ) ) } ↔ ( 𝐹 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) ) ) |
21 |
|
r19.26-2 |
⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) ) |
22 |
21
|
anbi2i |
⊢ ( ( 𝐹 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) ) ↔ ( 𝐹 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) ) ) |
23 |
|
anass |
⊢ ( ( ( 𝐹 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( 𝐹 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) ) ) |
24 |
22 23
|
bitr4i |
⊢ ( ( 𝐹 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) ) ↔ ( ( 𝐹 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) ) |
25 |
1 5 6 7
|
isghm |
⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ↔ ( ( 𝑅 ∈ Grp ∧ 𝑆 ∈ Grp ) ∧ ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) ) |
26 |
|
fvex |
⊢ ( Base ‘ 𝑆 ) ∈ V |
27 |
1
|
fvexi |
⊢ 𝐵 ∈ V |
28 |
26 27
|
pm3.2i |
⊢ ( ( Base ‘ 𝑆 ) ∈ V ∧ 𝐵 ∈ V ) |
29 |
|
elmapg |
⊢ ( ( ( Base ‘ 𝑆 ) ∈ V ∧ 𝐵 ∈ V ) → ( 𝐹 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐵 ) ↔ 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ) ) |
30 |
28 29
|
mp1i |
⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) → ( 𝐹 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐵 ) ↔ 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ) ) |
31 |
30
|
anbi1d |
⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) → ( ( 𝐹 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) ) |
32 |
|
rngabl |
⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Abel ) |
33 |
|
ablgrp |
⊢ ( 𝑅 ∈ Abel → 𝑅 ∈ Grp ) |
34 |
32 33
|
syl |
⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Grp ) |
35 |
|
rngabl |
⊢ ( 𝑆 ∈ Rng → 𝑆 ∈ Abel ) |
36 |
|
ablgrp |
⊢ ( 𝑆 ∈ Abel → 𝑆 ∈ Grp ) |
37 |
35 36
|
syl |
⊢ ( 𝑆 ∈ Rng → 𝑆 ∈ Grp ) |
38 |
|
ibar |
⊢ ( ( 𝑅 ∈ Grp ∧ 𝑆 ∈ Grp ) → ( ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( ( 𝑅 ∈ Grp ∧ 𝑆 ∈ Grp ) ∧ ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) ) ) |
39 |
34 37 38
|
syl2an |
⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) → ( ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( ( 𝑅 ∈ Grp ∧ 𝑆 ∈ Grp ) ∧ ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) ) ) |
40 |
31 39
|
bitr2d |
⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) → ( ( ( 𝑅 ∈ Grp ∧ 𝑆 ∈ Grp ) ∧ ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) ↔ ( 𝐹 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) ) |
41 |
25 40
|
bitr2id |
⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) → ( ( 𝐹 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ↔ 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ) ) |
42 |
41
|
anbi1d |
⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) → ( ( ( 𝐹 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) ) ) |
43 |
24 42
|
syl5bb |
⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) → ( ( 𝐹 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) ) ↔ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) ) ) |
44 |
20 43
|
syl5bb |
⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) → ( 𝐹 ∈ { 𝑓 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐵 ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ∗ ( 𝑓 ‘ 𝑦 ) ) ) } ↔ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) ) ) |
45 |
9 44
|
bitrd |
⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) → ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) ) ) |
46 |
4 45
|
biadanii |
⊢ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ↔ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) ) ) |