Step | Hyp | Ref
| Expression |
1 | | df-mhm 17335 |
. . 3
⊢ MndHom =
(𝑠 ∈ Mnd, 𝑡 ∈ Mnd ↦ {𝑓 ∈ ((Base‘𝑡) ↑𝑚
(Base‘𝑠)) ∣
(∀𝑥 ∈
(Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))}) |
2 | 1 | elmpt2cl 6876 |
. 2
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → (𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd)) |
3 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → (Base‘𝑡) = (Base‘𝑇)) |
4 | | ismhm.c |
. . . . . . . 8
⊢ 𝐶 = (Base‘𝑇) |
5 | 3, 4 | syl6eqr 2674 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → (Base‘𝑡) = 𝐶) |
6 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆)) |
7 | | ismhm.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑆) |
8 | 6, 7 | syl6eqr 2674 |
. . . . . . 7
⊢ (𝑠 = 𝑆 → (Base‘𝑠) = 𝐵) |
9 | 5, 8 | oveqan12rd 6670 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ((Base‘𝑡) ↑𝑚
(Base‘𝑠)) = (𝐶 ↑𝑚
𝐵)) |
10 | 8 | adantr 481 |
. . . . . . . 8
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (Base‘𝑠) = 𝐵) |
11 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑆 → (+g‘𝑠) = (+g‘𝑆)) |
12 | | ismhm.p |
. . . . . . . . . . . . 13
⊢ + =
(+g‘𝑆) |
13 | 11, 12 | syl6eqr 2674 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑆 → (+g‘𝑠) = + ) |
14 | 13 | oveqd 6667 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑆 → (𝑥(+g‘𝑠)𝑦) = (𝑥 + 𝑦)) |
15 | 14 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑆 → (𝑓‘(𝑥(+g‘𝑠)𝑦)) = (𝑓‘(𝑥 + 𝑦))) |
16 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (+g‘𝑡) = (+g‘𝑇)) |
17 | | ismhm.q |
. . . . . . . . . . . 12
⊢ ⨣ =
(+g‘𝑇) |
18 | 16, 17 | syl6eqr 2674 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → (+g‘𝑡) = ⨣ ) |
19 | 18 | oveqd 6667 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))) |
20 | 15, 19 | eqeqan12d 2638 |
. . . . . . . . 9
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ((𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ↔ (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)))) |
21 | 10, 20 | raleqbidv 3152 |
. . . . . . . 8
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ↔ ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)))) |
22 | 10, 21 | raleqbidv 3152 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)))) |
23 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑆 → (0g‘𝑠) = (0g‘𝑆)) |
24 | | ismhm.z |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑆) |
25 | 23, 24 | syl6eqr 2674 |
. . . . . . . . 9
⊢ (𝑠 = 𝑆 → (0g‘𝑠) = 0 ) |
26 | 25 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑠 = 𝑆 → (𝑓‘(0g‘𝑠)) = (𝑓‘ 0 )) |
27 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → (0g‘𝑡) = (0g‘𝑇)) |
28 | | ismhm.y |
. . . . . . . . 9
⊢ 𝑌 = (0g‘𝑇) |
29 | 27, 28 | syl6eqr 2674 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → (0g‘𝑡) = 𝑌) |
30 | 26, 29 | eqeqan12d 2638 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ((𝑓‘(0g‘𝑠)) = (0g‘𝑡) ↔ (𝑓‘ 0 ) = 𝑌)) |
31 | 22, 30 | anbi12d 747 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ((∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡)) ↔ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌))) |
32 | 9, 31 | rabeqbidv 3195 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → {𝑓 ∈ ((Base‘𝑡) ↑𝑚
(Base‘𝑠)) ∣
(∀𝑥 ∈
(Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))} = {𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∣ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌)}) |
33 | | ovex 6678 |
. . . . . 6
⊢ (𝐶 ↑𝑚
𝐵) ∈
V |
34 | 33 | rabex 4813 |
. . . . 5
⊢ {𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∣ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌)} ∈ V |
35 | 32, 1, 34 | ovmpt2a 6791 |
. . . 4
⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → (𝑆 MndHom 𝑇) = {𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∣ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌)}) |
36 | 35 | eleq2d 2687 |
. . 3
⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ 𝐹 ∈ {𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∣ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌)})) |
37 | | fvex 6201 |
. . . . . . 7
⊢
(Base‘𝑇)
∈ V |
38 | 4, 37 | eqeltri 2697 |
. . . . . 6
⊢ 𝐶 ∈ V |
39 | | fvex 6201 |
. . . . . . 7
⊢
(Base‘𝑆)
∈ V |
40 | 7, 39 | eqeltri 2697 |
. . . . . 6
⊢ 𝐵 ∈ V |
41 | 38, 40 | elmap 7886 |
. . . . 5
⊢ (𝐹 ∈ (𝐶 ↑𝑚 𝐵) ↔ 𝐹:𝐵⟶𝐶) |
42 | 41 | anbi1i 731 |
. . . 4
⊢ ((𝐹 ∈ (𝐶 ↑𝑚 𝐵) ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌)) ↔ (𝐹:𝐵⟶𝐶 ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌))) |
43 | | fveq1 6190 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (𝑓‘(𝑥 + 𝑦)) = (𝐹‘(𝑥 + 𝑦))) |
44 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → (𝑓‘𝑥) = (𝐹‘𝑥)) |
45 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → (𝑓‘𝑦) = (𝐹‘𝑦)) |
46 | 44, 45 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) |
47 | 43, 46 | eqeq12d 2637 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → ((𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ↔ (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))) |
48 | 47 | 2ralbidv 2989 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))) |
49 | | fveq1 6190 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑓‘ 0 ) = (𝐹‘ 0 )) |
50 | 49 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑓 = 𝐹 → ((𝑓‘ 0 ) = 𝑌 ↔ (𝐹‘ 0 ) = 𝑌)) |
51 | 48, 50 | anbi12d 747 |
. . . . 5
⊢ (𝑓 = 𝐹 → ((∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌) ↔ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌))) |
52 | 51 | elrab 3363 |
. . . 4
⊢ (𝐹 ∈ {𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∣ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌)} ↔ (𝐹 ∈ (𝐶 ↑𝑚 𝐵) ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌))) |
53 | | 3anass 1042 |
. . . 4
⊢ ((𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌) ↔ (𝐹:𝐵⟶𝐶 ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌))) |
54 | 42, 52, 53 | 3bitr4i 292 |
. . 3
⊢ (𝐹 ∈ {𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∣ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌)} ↔ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌)) |
55 | 36, 54 | syl6bb 276 |
. 2
⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌))) |
56 | 2, 55 | biadan2 674 |
1
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌))) |