Step | Hyp | Ref
| Expression |
1 | | df-mhm 18430 |
. . 3
⊢ MndHom =
(𝑠 ∈ Mnd, 𝑡 ∈ Mnd ↦ {𝑓 ∈ ((Base‘𝑡) ↑m
(Base‘𝑠)) ∣
(∀𝑥 ∈
(Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))}) |
2 | 1 | elmpocl 7511 |
. 2
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → (𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd)) |
3 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → (Base‘𝑡) = (Base‘𝑇)) |
4 | | ismhm.c |
. . . . . . . 8
⊢ 𝐶 = (Base‘𝑇) |
5 | 3, 4 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → (Base‘𝑡) = 𝐶) |
6 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆)) |
7 | | ismhm.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑆) |
8 | 6, 7 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑠 = 𝑆 → (Base‘𝑠) = 𝐵) |
9 | 5, 8 | oveqan12rd 7295 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ((Base‘𝑡) ↑m (Base‘𝑠)) = (𝐶 ↑m 𝐵)) |
10 | 8 | adantr 481 |
. . . . . . . 8
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (Base‘𝑠) = 𝐵) |
11 | | fveq2 6774 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑆 → (+g‘𝑠) = (+g‘𝑆)) |
12 | | ismhm.p |
. . . . . . . . . . . . 13
⊢ + =
(+g‘𝑆) |
13 | 11, 12 | eqtr4di 2796 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑆 → (+g‘𝑠) = + ) |
14 | 13 | oveqd 7292 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑆 → (𝑥(+g‘𝑠)𝑦) = (𝑥 + 𝑦)) |
15 | 14 | fveq2d 6778 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑆 → (𝑓‘(𝑥(+g‘𝑠)𝑦)) = (𝑓‘(𝑥 + 𝑦))) |
16 | | fveq2 6774 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (+g‘𝑡) = (+g‘𝑇)) |
17 | | ismhm.q |
. . . . . . . . . . . 12
⊢ ⨣ =
(+g‘𝑇) |
18 | 16, 17 | eqtr4di 2796 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → (+g‘𝑡) = ⨣ ) |
19 | 18 | oveqd 7292 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))) |
20 | 15, 19 | eqeqan12d 2752 |
. . . . . . . . 9
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ((𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ↔ (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)))) |
21 | 10, 20 | raleqbidv 3336 |
. . . . . . . 8
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ↔ ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)))) |
22 | 10, 21 | raleqbidv 3336 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)))) |
23 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑆 → (0g‘𝑠) = (0g‘𝑆)) |
24 | | ismhm.z |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑆) |
25 | 23, 24 | eqtr4di 2796 |
. . . . . . . . 9
⊢ (𝑠 = 𝑆 → (0g‘𝑠) = 0 ) |
26 | 25 | fveq2d 6778 |
. . . . . . . 8
⊢ (𝑠 = 𝑆 → (𝑓‘(0g‘𝑠)) = (𝑓‘ 0 )) |
27 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → (0g‘𝑡) = (0g‘𝑇)) |
28 | | ismhm.y |
. . . . . . . . 9
⊢ 𝑌 = (0g‘𝑇) |
29 | 27, 28 | eqtr4di 2796 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → (0g‘𝑡) = 𝑌) |
30 | 26, 29 | eqeqan12d 2752 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ((𝑓‘(0g‘𝑠)) = (0g‘𝑡) ↔ (𝑓‘ 0 ) = 𝑌)) |
31 | 22, 30 | anbi12d 631 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ((∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡)) ↔ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌))) |
32 | 9, 31 | rabeqbidv 3420 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → {𝑓 ∈ ((Base‘𝑡) ↑m (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))} = {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌)}) |
33 | | ovex 7308 |
. . . . . 6
⊢ (𝐶 ↑m 𝐵) ∈ V |
34 | 33 | rabex 5256 |
. . . . 5
⊢ {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌)} ∈ V |
35 | 32, 1, 34 | ovmpoa 7428 |
. . . 4
⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → (𝑆 MndHom 𝑇) = {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌)}) |
36 | 35 | eleq2d 2824 |
. . 3
⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ 𝐹 ∈ {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌)})) |
37 | 4 | fvexi 6788 |
. . . . . 6
⊢ 𝐶 ∈ V |
38 | 7 | fvexi 6788 |
. . . . . 6
⊢ 𝐵 ∈ V |
39 | 37, 38 | elmap 8659 |
. . . . 5
⊢ (𝐹 ∈ (𝐶 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐶) |
40 | 39 | anbi1i 624 |
. . . 4
⊢ ((𝐹 ∈ (𝐶 ↑m 𝐵) ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌)) ↔ (𝐹:𝐵⟶𝐶 ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌))) |
41 | | fveq1 6773 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (𝑓‘(𝑥 + 𝑦)) = (𝐹‘(𝑥 + 𝑦))) |
42 | | fveq1 6773 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → (𝑓‘𝑥) = (𝐹‘𝑥)) |
43 | | fveq1 6773 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → (𝑓‘𝑦) = (𝐹‘𝑦)) |
44 | 42, 43 | oveq12d 7293 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) |
45 | 41, 44 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → ((𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ↔ (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))) |
46 | 45 | 2ralbidv 3129 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))) |
47 | | fveq1 6773 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑓‘ 0 ) = (𝐹‘ 0 )) |
48 | 47 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑓 = 𝐹 → ((𝑓‘ 0 ) = 𝑌 ↔ (𝐹‘ 0 ) = 𝑌)) |
49 | 46, 48 | anbi12d 631 |
. . . . 5
⊢ (𝑓 = 𝐹 → ((∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌) ↔ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌))) |
50 | 49 | elrab 3624 |
. . . 4
⊢ (𝐹 ∈ {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌)} ↔ (𝐹 ∈ (𝐶 ↑m 𝐵) ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌))) |
51 | | 3anass 1094 |
. . . 4
⊢ ((𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌) ↔ (𝐹:𝐵⟶𝐶 ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌))) |
52 | 40, 50, 51 | 3bitr4i 303 |
. . 3
⊢ (𝐹 ∈ {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌)} ↔ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌)) |
53 | 36, 52 | bitrdi 287 |
. 2
⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌))) |
54 | 2, 53 | biadanii 819 |
1
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌))) |