Step |
Hyp |
Ref |
Expression |
0 |
|
crnghom |
⊢ RngHom |
1 |
|
vr |
⊢ 𝑟 |
2 |
|
crngo |
⊢ RingOps |
3 |
|
vs |
⊢ 𝑠 |
4 |
|
vf |
⊢ 𝑓 |
5 |
|
c1st |
⊢ 1st |
6 |
3
|
cv |
⊢ 𝑠 |
7 |
6 5
|
cfv |
⊢ ( 1st ‘ 𝑠 ) |
8 |
7
|
crn |
⊢ ran ( 1st ‘ 𝑠 ) |
9 |
|
cmap |
⊢ ↑m |
10 |
1
|
cv |
⊢ 𝑟 |
11 |
10 5
|
cfv |
⊢ ( 1st ‘ 𝑟 ) |
12 |
11
|
crn |
⊢ ran ( 1st ‘ 𝑟 ) |
13 |
8 12 9
|
co |
⊢ ( ran ( 1st ‘ 𝑠 ) ↑m ran ( 1st ‘ 𝑟 ) ) |
14 |
4
|
cv |
⊢ 𝑓 |
15 |
|
cgi |
⊢ GId |
16 |
|
c2nd |
⊢ 2nd |
17 |
10 16
|
cfv |
⊢ ( 2nd ‘ 𝑟 ) |
18 |
17 15
|
cfv |
⊢ ( GId ‘ ( 2nd ‘ 𝑟 ) ) |
19 |
18 14
|
cfv |
⊢ ( 𝑓 ‘ ( GId ‘ ( 2nd ‘ 𝑟 ) ) ) |
20 |
6 16
|
cfv |
⊢ ( 2nd ‘ 𝑠 ) |
21 |
20 15
|
cfv |
⊢ ( GId ‘ ( 2nd ‘ 𝑠 ) ) |
22 |
19 21
|
wceq |
⊢ ( 𝑓 ‘ ( GId ‘ ( 2nd ‘ 𝑟 ) ) ) = ( GId ‘ ( 2nd ‘ 𝑠 ) ) |
23 |
|
vx |
⊢ 𝑥 |
24 |
|
vy |
⊢ 𝑦 |
25 |
23
|
cv |
⊢ 𝑥 |
26 |
24
|
cv |
⊢ 𝑦 |
27 |
25 26 11
|
co |
⊢ ( 𝑥 ( 1st ‘ 𝑟 ) 𝑦 ) |
28 |
27 14
|
cfv |
⊢ ( 𝑓 ‘ ( 𝑥 ( 1st ‘ 𝑟 ) 𝑦 ) ) |
29 |
25 14
|
cfv |
⊢ ( 𝑓 ‘ 𝑥 ) |
30 |
26 14
|
cfv |
⊢ ( 𝑓 ‘ 𝑦 ) |
31 |
29 30 7
|
co |
⊢ ( ( 𝑓 ‘ 𝑥 ) ( 1st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) |
32 |
28 31
|
wceq |
⊢ ( 𝑓 ‘ ( 𝑥 ( 1st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) |
33 |
25 26 17
|
co |
⊢ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) |
34 |
33 14
|
cfv |
⊢ ( 𝑓 ‘ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ) |
35 |
29 30 20
|
co |
⊢ ( ( 𝑓 ‘ 𝑥 ) ( 2nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) |
36 |
34 35
|
wceq |
⊢ ( 𝑓 ‘ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) |
37 |
32 36
|
wa |
⊢ ( ( 𝑓 ‘ ( 𝑥 ( 1st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) |
38 |
37 24 12
|
wral |
⊢ ∀ 𝑦 ∈ ran ( 1st ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( 1st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) |
39 |
38 23 12
|
wral |
⊢ ∀ 𝑥 ∈ ran ( 1st ‘ 𝑟 ) ∀ 𝑦 ∈ ran ( 1st ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( 1st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) |
40 |
22 39
|
wa |
⊢ ( ( 𝑓 ‘ ( GId ‘ ( 2nd ‘ 𝑟 ) ) ) = ( GId ‘ ( 2nd ‘ 𝑠 ) ) ∧ ∀ 𝑥 ∈ ran ( 1st ‘ 𝑟 ) ∀ 𝑦 ∈ ran ( 1st ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( 1st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) |
41 |
40 4 13
|
crab |
⊢ { 𝑓 ∈ ( ran ( 1st ‘ 𝑠 ) ↑m ran ( 1st ‘ 𝑟 ) ) ∣ ( ( 𝑓 ‘ ( GId ‘ ( 2nd ‘ 𝑟 ) ) ) = ( GId ‘ ( 2nd ‘ 𝑠 ) ) ∧ ∀ 𝑥 ∈ ran ( 1st ‘ 𝑟 ) ∀ 𝑦 ∈ ran ( 1st ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( 1st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } |
42 |
1 3 2 2 41
|
cmpo |
⊢ ( 𝑟 ∈ RingOps , 𝑠 ∈ RingOps ↦ { 𝑓 ∈ ( ran ( 1st ‘ 𝑠 ) ↑m ran ( 1st ‘ 𝑟 ) ) ∣ ( ( 𝑓 ‘ ( GId ‘ ( 2nd ‘ 𝑟 ) ) ) = ( GId ‘ ( 2nd ‘ 𝑠 ) ) ∧ ∀ 𝑥 ∈ ran ( 1st ‘ 𝑟 ) ∀ 𝑦 ∈ ran ( 1st ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( 1st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } ) |
43 |
0 42
|
wceq |
⊢ RngHom = ( 𝑟 ∈ RingOps , 𝑠 ∈ RingOps ↦ { 𝑓 ∈ ( ran ( 1st ‘ 𝑠 ) ↑m ran ( 1st ‘ 𝑟 ) ) ∣ ( ( 𝑓 ‘ ( GId ‘ ( 2nd ‘ 𝑟 ) ) ) = ( GId ‘ ( 2nd ‘ 𝑠 ) ) ∧ ∀ 𝑥 ∈ ran ( 1st ‘ 𝑟 ) ∀ 𝑦 ∈ ran ( 1st ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( 1st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } ) |