Detailed syntax breakdown of Definition df-rnghom
Step | Hyp | Ref
| Expression |
1 | | crh 19732 |
. 2
class
RingHom |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | vs |
. . 3
setvar 𝑠 |
4 | | crg 19562 |
. . 3
class
Ring |
5 | | vv |
. . . 4
setvar 𝑣 |
6 | 2 | cv 1542 |
. . . . 5
class 𝑟 |
7 | | cbs 16760 |
. . . . 5
class
Base |
8 | 6, 7 | cfv 6380 |
. . . 4
class
(Base‘𝑟) |
9 | | vw |
. . . . 5
setvar 𝑤 |
10 | 3 | cv 1542 |
. . . . . 6
class 𝑠 |
11 | 10, 7 | cfv 6380 |
. . . . 5
class
(Base‘𝑠) |
12 | | cur 19516 |
. . . . . . . . . 10
class
1r |
13 | 6, 12 | cfv 6380 |
. . . . . . . . 9
class
(1r‘𝑟) |
14 | | vf |
. . . . . . . . . 10
setvar 𝑓 |
15 | 14 | cv 1542 |
. . . . . . . . 9
class 𝑓 |
16 | 13, 15 | cfv 6380 |
. . . . . . . 8
class (𝑓‘(1r‘𝑟)) |
17 | 10, 12 | cfv 6380 |
. . . . . . . 8
class
(1r‘𝑠) |
18 | 16, 17 | wceq 1543 |
. . . . . . 7
wff (𝑓‘(1r‘𝑟)) = (1r‘𝑠) |
19 | | vx |
. . . . . . . . . . . . . 14
setvar 𝑥 |
20 | 19 | cv 1542 |
. . . . . . . . . . . . 13
class 𝑥 |
21 | | vy |
. . . . . . . . . . . . . 14
setvar 𝑦 |
22 | 21 | cv 1542 |
. . . . . . . . . . . . 13
class 𝑦 |
23 | | cplusg 16802 |
. . . . . . . . . . . . . 14
class
+g |
24 | 6, 23 | cfv 6380 |
. . . . . . . . . . . . 13
class
(+g‘𝑟) |
25 | 20, 22, 24 | co 7213 |
. . . . . . . . . . . 12
class (𝑥(+g‘𝑟)𝑦) |
26 | 25, 15 | cfv 6380 |
. . . . . . . . . . 11
class (𝑓‘(𝑥(+g‘𝑟)𝑦)) |
27 | 20, 15 | cfv 6380 |
. . . . . . . . . . . 12
class (𝑓‘𝑥) |
28 | 22, 15 | cfv 6380 |
. . . . . . . . . . . 12
class (𝑓‘𝑦) |
29 | 10, 23 | cfv 6380 |
. . . . . . . . . . . 12
class
(+g‘𝑠) |
30 | 27, 28, 29 | co 7213 |
. . . . . . . . . . 11
class ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) |
31 | 26, 30 | wceq 1543 |
. . . . . . . . . 10
wff (𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) |
32 | | cmulr 16803 |
. . . . . . . . . . . . . 14
class
.r |
33 | 6, 32 | cfv 6380 |
. . . . . . . . . . . . 13
class
(.r‘𝑟) |
34 | 20, 22, 33 | co 7213 |
. . . . . . . . . . . 12
class (𝑥(.r‘𝑟)𝑦) |
35 | 34, 15 | cfv 6380 |
. . . . . . . . . . 11
class (𝑓‘(𝑥(.r‘𝑟)𝑦)) |
36 | 10, 32 | cfv 6380 |
. . . . . . . . . . . 12
class
(.r‘𝑠) |
37 | 27, 28, 36 | co 7213 |
. . . . . . . . . . 11
class ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) |
38 | 35, 37 | wceq 1543 |
. . . . . . . . . 10
wff (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) |
39 | 31, 38 | wa 399 |
. . . . . . . . 9
wff ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))) |
40 | 5 | cv 1542 |
. . . . . . . . 9
class 𝑣 |
41 | 39, 21, 40 | wral 3061 |
. . . . . . . 8
wff
∀𝑦 ∈
𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))) |
42 | 41, 19, 40 | wral 3061 |
. . . . . . 7
wff
∀𝑥 ∈
𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))) |
43 | 18, 42 | wa 399 |
. . . . . 6
wff ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))) |
44 | 9 | cv 1542 |
. . . . . . 7
class 𝑤 |
45 | | cmap 8508 |
. . . . . . 7
class
↑m |
46 | 44, 40, 45 | co 7213 |
. . . . . 6
class (𝑤 ↑m 𝑣) |
47 | 43, 14, 46 | crab 3065 |
. . . . 5
class {𝑓 ∈ (𝑤 ↑m 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))} |
48 | 9, 11, 47 | csb 3811 |
. . . 4
class
⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑m 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))} |
49 | 5, 8, 48 | csb 3811 |
. . 3
class
⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑m 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))} |
50 | 2, 3, 4, 4, 49 | cmpo 7215 |
. 2
class (𝑟 ∈ Ring, 𝑠 ∈ Ring ↦
⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑m 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))}) |
51 | 1, 50 | wceq 1543 |
1
wff RingHom =
(𝑟 ∈ Ring, 𝑠 ∈ Ring ↦
⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑m 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))}) |