Step | Hyp | Ref
| Expression |
1 | | crnghom 35885 |
. 2
class
RngHom |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | vs |
. . 3
setvar 𝑠 |
4 | | crngo 35819 |
. . 3
class
RingOps |
5 | 2 | cv 1542 |
. . . . . . . . 9
class 𝑟 |
6 | | c2nd 7779 |
. . . . . . . . 9
class
2^{nd} |
7 | 5, 6 | cfv 6398 |
. . . . . . . 8
class
(2^{nd} ‘𝑟) |
8 | | cgi 28598 |
. . . . . . . 8
class
GId |
9 | 7, 8 | cfv 6398 |
. . . . . . 7
class
(GId‘(2^{nd} ‘𝑟)) |
10 | | vf |
. . . . . . . 8
setvar 𝑓 |
11 | 10 | cv 1542 |
. . . . . . 7
class 𝑓 |
12 | 9, 11 | cfv 6398 |
. . . . . 6
class (𝑓‘(GId‘(2^{nd}
‘𝑟))) |
13 | 3 | cv 1542 |
. . . . . . . 8
class 𝑠 |
14 | 13, 6 | cfv 6398 |
. . . . . . 7
class
(2^{nd} ‘𝑠) |
15 | 14, 8 | cfv 6398 |
. . . . . 6
class
(GId‘(2^{nd} ‘𝑠)) |
16 | 12, 15 | wceq 1543 |
. . . . 5
wff (𝑓‘(GId‘(2^{nd}
‘𝑟))) =
(GId‘(2^{nd} ‘𝑠)) |
17 | | vx |
. . . . . . . . . . . 12
setvar 𝑥 |
18 | 17 | cv 1542 |
. . . . . . . . . . 11
class 𝑥 |
19 | | vy |
. . . . . . . . . . . 12
setvar 𝑦 |
20 | 19 | cv 1542 |
. . . . . . . . . . 11
class 𝑦 |
21 | | c1st 7778 |
. . . . . . . . . . . 12
class
1^{st} |
22 | 5, 21 | cfv 6398 |
. . . . . . . . . . 11
class
(1^{st} ‘𝑟) |
23 | 18, 20, 22 | co 7232 |
. . . . . . . . . 10
class (𝑥(1^{st} ‘𝑟)𝑦) |
24 | 23, 11 | cfv 6398 |
. . . . . . . . 9
class (𝑓‘(𝑥(1^{st} ‘𝑟)𝑦)) |
25 | 18, 11 | cfv 6398 |
. . . . . . . . . 10
class (𝑓‘𝑥) |
26 | 20, 11 | cfv 6398 |
. . . . . . . . . 10
class (𝑓‘𝑦) |
27 | 13, 21 | cfv 6398 |
. . . . . . . . . 10
class
(1^{st} ‘𝑠) |
28 | 25, 26, 27 | co 7232 |
. . . . . . . . 9
class ((𝑓‘𝑥)(1^{st} ‘𝑠)(𝑓‘𝑦)) |
29 | 24, 28 | wceq 1543 |
. . . . . . . 8
wff (𝑓‘(𝑥(1^{st} ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1^{st} ‘𝑠)(𝑓‘𝑦)) |
30 | 18, 20, 7 | co 7232 |
. . . . . . . . . 10
class (𝑥(2^{nd} ‘𝑟)𝑦) |
31 | 30, 11 | cfv 6398 |
. . . . . . . . 9
class (𝑓‘(𝑥(2^{nd} ‘𝑟)𝑦)) |
32 | 25, 26, 14 | co 7232 |
. . . . . . . . 9
class ((𝑓‘𝑥)(2^{nd} ‘𝑠)(𝑓‘𝑦)) |
33 | 31, 32 | wceq 1543 |
. . . . . . . 8
wff (𝑓‘(𝑥(2^{nd} ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2^{nd} ‘𝑠)(𝑓‘𝑦)) |
34 | 29, 33 | wa 399 |
. . . . . . 7
wff ((𝑓‘(𝑥(1^{st} ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1^{st} ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2^{nd} ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2^{nd} ‘𝑠)(𝑓‘𝑦))) |
35 | 22 | crn 5567 |
. . . . . . 7
class ran
(1^{st} ‘𝑟) |
36 | 34, 19, 35 | wral 3062 |
. . . . . 6
wff
∀𝑦 ∈ ran
(1^{st} ‘𝑟)((𝑓‘(𝑥(1^{st} ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1^{st} ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2^{nd} ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2^{nd} ‘𝑠)(𝑓‘𝑦))) |
37 | 36, 17, 35 | wral 3062 |
. . . . 5
wff
∀𝑥 ∈ ran
(1^{st} ‘𝑟)∀𝑦 ∈ ran (1^{st} ‘𝑟)((𝑓‘(𝑥(1^{st} ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1^{st} ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2^{nd} ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2^{nd} ‘𝑠)(𝑓‘𝑦))) |
38 | 16, 37 | wa 399 |
. . . 4
wff ((𝑓‘(GId‘(2^{nd}
‘𝑟))) =
(GId‘(2^{nd} ‘𝑠)) ∧ ∀𝑥 ∈ ran (1^{st} ‘𝑟)∀𝑦 ∈ ran (1^{st} ‘𝑟)((𝑓‘(𝑥(1^{st} ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1^{st} ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2^{nd} ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2^{nd} ‘𝑠)(𝑓‘𝑦)))) |
39 | 27 | crn 5567 |
. . . . 5
class ran
(1^{st} ‘𝑠) |
40 | | cmap 8529 |
. . . . 5
class
↑_{m} |
41 | 39, 35, 40 | co 7232 |
. . . 4
class (ran
(1^{st} ‘𝑠)
↑_{m} ran (1^{st} ‘𝑟)) |
42 | 38, 10, 41 | crab 3066 |
. . 3
class {𝑓 ∈ (ran (1^{st}
‘𝑠)
↑_{m} ran (1^{st} ‘𝑟)) ∣ ((𝑓‘(GId‘(2^{nd}
‘𝑟))) =
(GId‘(2^{nd} ‘𝑠)) ∧ ∀𝑥 ∈ ran (1^{st} ‘𝑟)∀𝑦 ∈ ran (1^{st} ‘𝑟)((𝑓‘(𝑥(1^{st} ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1^{st} ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2^{nd} ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2^{nd} ‘𝑠)(𝑓‘𝑦))))} |
43 | 2, 3, 4, 4, 42 | cmpo 7234 |
. 2
class (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (ran (1^{st}
‘𝑠)
↑_{m} ran (1^{st} ‘𝑟)) ∣ ((𝑓‘(GId‘(2^{nd}
‘𝑟))) =
(GId‘(2^{nd} ‘𝑠)) ∧ ∀𝑥 ∈ ran (1^{st} ‘𝑟)∀𝑦 ∈ ran (1^{st} ‘𝑟)((𝑓‘(𝑥(1^{st} ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1^{st} ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2^{nd} ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2^{nd} ‘𝑠)(𝑓‘𝑦))))}) |
44 | 1, 43 | wceq 1543 |
1
wff RngHom =
(𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (ran (1^{st}
‘𝑠)
↑_{m} ran (1^{st} ‘𝑟)) ∣ ((𝑓‘(GId‘(2^{nd}
‘𝑟))) =
(GId‘(2^{nd} ‘𝑠)) ∧ ∀𝑥 ∈ ran (1^{st} ‘𝑟)∀𝑦 ∈ ran (1^{st} ‘𝑟)((𝑓‘(𝑥(1^{st} ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1^{st} ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2^{nd} ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2^{nd} ‘𝑠)(𝑓‘𝑦))))}) |