Step | Hyp | Ref
| Expression |
1 | | df-ghm 19181 |
. . 3
⊢ GrpHom =
(𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑓 ∣
[(Base‘𝑠) /
𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢 ∈ 𝑤 ∀𝑣 ∈ 𝑤 (𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)))}) |
2 | 1 | elmpocl 7662 |
. 2
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝑆 ∈ Grp ∧ 𝑇 ∈ Grp)) |
3 | | fvex 6909 |
. . . . . . . 8
⊢
(Base‘𝑠)
∈ V |
4 | | feq2 6705 |
. . . . . . . . 9
⊢ (𝑤 = (Base‘𝑠) → (𝑓:𝑤⟶(Base‘𝑡) ↔ 𝑓:(Base‘𝑠)⟶(Base‘𝑡))) |
5 | | raleq 3311 |
. . . . . . . . . 10
⊢ (𝑤 = (Base‘𝑠) → (∀𝑣 ∈ 𝑤 (𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)) ↔ ∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)))) |
6 | 5 | raleqbi1dv 3322 |
. . . . . . . . 9
⊢ (𝑤 = (Base‘𝑠) → (∀𝑢 ∈ 𝑤 ∀𝑣 ∈ 𝑤 (𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)) ↔ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)))) |
7 | 4, 6 | anbi12d 630 |
. . . . . . . 8
⊢ (𝑤 = (Base‘𝑠) → ((𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢 ∈ 𝑤 ∀𝑣 ∈ 𝑤 (𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣))) ↔ (𝑓:(Base‘𝑠)⟶(Base‘𝑡) ∧ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣))))) |
8 | 3, 7 | sbcie 3817 |
. . . . . . 7
⊢
([(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢 ∈ 𝑤 ∀𝑣 ∈ 𝑤 (𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣))) ↔ (𝑓:(Base‘𝑠)⟶(Base‘𝑡) ∧ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)))) |
9 | | fveq2 6896 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆)) |
10 | | isghm.w |
. . . . . . . . . . 11
⊢ 𝑋 = (Base‘𝑆) |
11 | 9, 10 | eqtr4di 2783 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑆 → (Base‘𝑠) = 𝑋) |
12 | 11 | adantr 479 |
. . . . . . . . 9
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (Base‘𝑠) = 𝑋) |
13 | | fveq2 6896 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → (Base‘𝑡) = (Base‘𝑇)) |
14 | | isghm.x |
. . . . . . . . . . 11
⊢ 𝑌 = (Base‘𝑇) |
15 | 13, 14 | eqtr4di 2783 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → (Base‘𝑡) = 𝑌) |
16 | 15 | adantl 480 |
. . . . . . . . 9
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (Base‘𝑡) = 𝑌) |
17 | 12, 16 | feq23d 6718 |
. . . . . . . 8
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (𝑓:(Base‘𝑠)⟶(Base‘𝑡) ↔ 𝑓:𝑋⟶𝑌)) |
18 | | fveq2 6896 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑆 → (+g‘𝑠) = (+g‘𝑆)) |
19 | | isghm.a |
. . . . . . . . . . . . . 14
⊢ + =
(+g‘𝑆) |
20 | 18, 19 | eqtr4di 2783 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑆 → (+g‘𝑠) = + ) |
21 | 20 | oveqd 7436 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑆 → (𝑢(+g‘𝑠)𝑣) = (𝑢 + 𝑣)) |
22 | 21 | fveq2d 6900 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑆 → (𝑓‘(𝑢(+g‘𝑠)𝑣)) = (𝑓‘(𝑢 + 𝑣))) |
23 | | fveq2 6896 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑇 → (+g‘𝑡) = (+g‘𝑇)) |
24 | | isghm.b |
. . . . . . . . . . . . 13
⊢ ⨣ =
(+g‘𝑇) |
25 | 23, 24 | eqtr4di 2783 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (+g‘𝑡) = ⨣ ) |
26 | 25 | oveqd 7436 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣))) |
27 | 22, 26 | eqeqan12d 2739 |
. . . . . . . . . 10
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ((𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)) ↔ (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)))) |
28 | 12, 27 | raleqbidv 3329 |
. . . . . . . . 9
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)) ↔ ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)))) |
29 | 12, 28 | raleqbidv 3329 |
. . . . . . . 8
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)) ↔ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)))) |
30 | 17, 29 | anbi12d 630 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ((𝑓:(Base‘𝑠)⟶(Base‘𝑡) ∧ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣))) ↔ (𝑓:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣))))) |
31 | 8, 30 | bitrid 282 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ([(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢 ∈ 𝑤 ∀𝑣 ∈ 𝑤 (𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣))) ↔ (𝑓:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣))))) |
32 | 31 | abbidv 2794 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → {𝑓 ∣ [(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢 ∈ 𝑤 ∀𝑣 ∈ 𝑤 (𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)))} = {𝑓 ∣ (𝑓:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)))}) |
33 | 14 | fvexi 6910 |
. . . . . . 7
⊢ 𝑌 ∈ V |
34 | | fsetex 8875 |
. . . . . . 7
⊢ (𝑌 ∈ V → {𝑓 ∣ 𝑓:𝑋⟶𝑌} ∈ V) |
35 | 33, 34 | ax-mp 5 |
. . . . . 6
⊢ {𝑓 ∣ 𝑓:𝑋⟶𝑌} ∈ V |
36 | | abanssl 4300 |
. . . . . 6
⊢ {𝑓 ∣ (𝑓:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)))} ⊆ {𝑓 ∣ 𝑓:𝑋⟶𝑌} |
37 | 35, 36 | ssexi 5323 |
. . . . 5
⊢ {𝑓 ∣ (𝑓:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)))} ∈ V |
38 | 32, 1, 37 | ovmpoa 7576 |
. . . 4
⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝑆 GrpHom 𝑇) = {𝑓 ∣ (𝑓:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)))}) |
39 | 38 | eleq2d 2811 |
. . 3
⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ 𝐹 ∈ {𝑓 ∣ (𝑓:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)))})) |
40 | 10 | fvexi 6910 |
. . . . . 6
⊢ 𝑋 ∈ V |
41 | | fex2 7942 |
. . . . . 6
⊢ ((𝐹:𝑋⟶𝑌 ∧ 𝑋 ∈ V ∧ 𝑌 ∈ V) → 𝐹 ∈ V) |
42 | 40, 33, 41 | mp3an23 1449 |
. . . . 5
⊢ (𝐹:𝑋⟶𝑌 → 𝐹 ∈ V) |
43 | 42 | adantr 479 |
. . . 4
⊢ ((𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣))) → 𝐹 ∈ V) |
44 | | feq1 6704 |
. . . . 5
⊢ (𝑓 = 𝐹 → (𝑓:𝑋⟶𝑌 ↔ 𝐹:𝑋⟶𝑌)) |
45 | | fveq1 6895 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑓‘(𝑢 + 𝑣)) = (𝐹‘(𝑢 + 𝑣))) |
46 | | fveq1 6895 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (𝑓‘𝑢) = (𝐹‘𝑢)) |
47 | | fveq1 6895 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (𝑓‘𝑣) = (𝐹‘𝑣)) |
48 | 46, 47 | oveq12d 7437 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣))) |
49 | 45, 48 | eqeq12d 2741 |
. . . . . 6
⊢ (𝑓 = 𝐹 → ((𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)) ↔ (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣)))) |
50 | 49 | 2ralbidv 3208 |
. . . . 5
⊢ (𝑓 = 𝐹 → (∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)) ↔ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣)))) |
51 | 44, 50 | anbi12d 630 |
. . . 4
⊢ (𝑓 = 𝐹 → ((𝑓:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣))) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣))))) |
52 | 43, 51 | elab3 3672 |
. . 3
⊢ (𝐹 ∈ {𝑓 ∣ (𝑓:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)))} ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣)))) |
53 | 39, 52 | bitrdi 286 |
. 2
⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣))))) |
54 | 2, 53 | biadanii 820 |
1
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣))))) |