| Step | Hyp | Ref
| Expression |
| 1 | | df-ghm 19231 |
. . 3
⊢ GrpHom =
(𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑓 ∣
[(Base‘𝑠) /
𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢 ∈ 𝑤 ∀𝑣 ∈ 𝑤 (𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)))}) |
| 2 | 1 | elmpocl 7674 |
. 2
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝑆 ∈ Grp ∧ 𝑇 ∈ Grp)) |
| 3 | | fvex 6919 |
. . . . . . . 8
⊢
(Base‘𝑠)
∈ V |
| 4 | | feq2 6717 |
. . . . . . . . 9
⊢ (𝑤 = (Base‘𝑠) → (𝑓:𝑤⟶(Base‘𝑡) ↔ 𝑓:(Base‘𝑠)⟶(Base‘𝑡))) |
| 5 | | raleq 3323 |
. . . . . . . . . 10
⊢ (𝑤 = (Base‘𝑠) → (∀𝑣 ∈ 𝑤 (𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)) ↔ ∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)))) |
| 6 | 5 | raleqbi1dv 3338 |
. . . . . . . . 9
⊢ (𝑤 = (Base‘𝑠) → (∀𝑢 ∈ 𝑤 ∀𝑣 ∈ 𝑤 (𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)) ↔ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)))) |
| 7 | 4, 6 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑤 = (Base‘𝑠) → ((𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢 ∈ 𝑤 ∀𝑣 ∈ 𝑤 (𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣))) ↔ (𝑓:(Base‘𝑠)⟶(Base‘𝑡) ∧ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣))))) |
| 8 | 3, 7 | sbcie 3830 |
. . . . . . 7
⊢
([(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢 ∈ 𝑤 ∀𝑣 ∈ 𝑤 (𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣))) ↔ (𝑓:(Base‘𝑠)⟶(Base‘𝑡) ∧ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)))) |
| 9 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆)) |
| 10 | | isghm.w |
. . . . . . . . . . 11
⊢ 𝑋 = (Base‘𝑆) |
| 11 | 9, 10 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑆 → (Base‘𝑠) = 𝑋) |
| 12 | 11 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (Base‘𝑠) = 𝑋) |
| 13 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → (Base‘𝑡) = (Base‘𝑇)) |
| 14 | | isghm.x |
. . . . . . . . . . 11
⊢ 𝑌 = (Base‘𝑇) |
| 15 | 13, 14 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → (Base‘𝑡) = 𝑌) |
| 16 | 15 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (Base‘𝑡) = 𝑌) |
| 17 | 12, 16 | feq23d 6731 |
. . . . . . . 8
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (𝑓:(Base‘𝑠)⟶(Base‘𝑡) ↔ 𝑓:𝑋⟶𝑌)) |
| 18 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑆 → (+g‘𝑠) = (+g‘𝑆)) |
| 19 | | isghm.a |
. . . . . . . . . . . . . 14
⊢ + =
(+g‘𝑆) |
| 20 | 18, 19 | eqtr4di 2795 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑆 → (+g‘𝑠) = + ) |
| 21 | 20 | oveqd 7448 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑆 → (𝑢(+g‘𝑠)𝑣) = (𝑢 + 𝑣)) |
| 22 | 21 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑆 → (𝑓‘(𝑢(+g‘𝑠)𝑣)) = (𝑓‘(𝑢 + 𝑣))) |
| 23 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑇 → (+g‘𝑡) = (+g‘𝑇)) |
| 24 | | isghm.b |
. . . . . . . . . . . . 13
⊢ ⨣ =
(+g‘𝑇) |
| 25 | 23, 24 | eqtr4di 2795 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (+g‘𝑡) = ⨣ ) |
| 26 | 25 | oveqd 7448 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣))) |
| 27 | 22, 26 | eqeqan12d 2751 |
. . . . . . . . . 10
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ((𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)) ↔ (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)))) |
| 28 | 12, 27 | raleqbidv 3346 |
. . . . . . . . 9
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)) ↔ ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)))) |
| 29 | 12, 28 | raleqbidv 3346 |
. . . . . . . 8
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)) ↔ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)))) |
| 30 | 17, 29 | anbi12d 632 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ((𝑓:(Base‘𝑠)⟶(Base‘𝑡) ∧ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣))) ↔ (𝑓:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣))))) |
| 31 | 8, 30 | bitrid 283 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ([(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢 ∈ 𝑤 ∀𝑣 ∈ 𝑤 (𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣))) ↔ (𝑓:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣))))) |
| 32 | 31 | abbidv 2808 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → {𝑓 ∣ [(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢 ∈ 𝑤 ∀𝑣 ∈ 𝑤 (𝑓‘(𝑢(+g‘𝑠)𝑣)) = ((𝑓‘𝑢)(+g‘𝑡)(𝑓‘𝑣)))} = {𝑓 ∣ (𝑓:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)))}) |
| 33 | 14 | fvexi 6920 |
. . . . . . 7
⊢ 𝑌 ∈ V |
| 34 | | fsetex 8896 |
. . . . . . 7
⊢ (𝑌 ∈ V → {𝑓 ∣ 𝑓:𝑋⟶𝑌} ∈ V) |
| 35 | 33, 34 | ax-mp 5 |
. . . . . 6
⊢ {𝑓 ∣ 𝑓:𝑋⟶𝑌} ∈ V |
| 36 | | abanssl 4311 |
. . . . . 6
⊢ {𝑓 ∣ (𝑓:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)))} ⊆ {𝑓 ∣ 𝑓:𝑋⟶𝑌} |
| 37 | 35, 36 | ssexi 5322 |
. . . . 5
⊢ {𝑓 ∣ (𝑓:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)))} ∈ V |
| 38 | 32, 1, 37 | ovmpoa 7588 |
. . . 4
⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝑆 GrpHom 𝑇) = {𝑓 ∣ (𝑓:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)))}) |
| 39 | 38 | eleq2d 2827 |
. . 3
⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ 𝐹 ∈ {𝑓 ∣ (𝑓:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)))})) |
| 40 | 10 | fvexi 6920 |
. . . . . 6
⊢ 𝑋 ∈ V |
| 41 | | fex2 7958 |
. . . . . 6
⊢ ((𝐹:𝑋⟶𝑌 ∧ 𝑋 ∈ V ∧ 𝑌 ∈ V) → 𝐹 ∈ V) |
| 42 | 40, 33, 41 | mp3an23 1455 |
. . . . 5
⊢ (𝐹:𝑋⟶𝑌 → 𝐹 ∈ V) |
| 43 | 42 | adantr 480 |
. . . 4
⊢ ((𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣))) → 𝐹 ∈ V) |
| 44 | | feq1 6716 |
. . . . 5
⊢ (𝑓 = 𝐹 → (𝑓:𝑋⟶𝑌 ↔ 𝐹:𝑋⟶𝑌)) |
| 45 | | fveq1 6905 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑓‘(𝑢 + 𝑣)) = (𝐹‘(𝑢 + 𝑣))) |
| 46 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (𝑓‘𝑢) = (𝐹‘𝑢)) |
| 47 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (𝑓‘𝑣) = (𝐹‘𝑣)) |
| 48 | 46, 47 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣))) |
| 49 | 45, 48 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑓 = 𝐹 → ((𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)) ↔ (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣)))) |
| 50 | 49 | 2ralbidv 3221 |
. . . . 5
⊢ (𝑓 = 𝐹 → (∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)) ↔ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣)))) |
| 51 | 44, 50 | anbi12d 632 |
. . . 4
⊢ (𝑓 = 𝐹 → ((𝑓:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣))) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣))))) |
| 52 | 43, 51 | elab3 3686 |
. . 3
⊢ (𝐹 ∈ {𝑓 ∣ (𝑓:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓‘𝑢) ⨣ (𝑓‘𝑣)))} ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣)))) |
| 53 | 39, 52 | bitrdi 287 |
. 2
⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣))))) |
| 54 | 2, 53 | biadanii 822 |
1
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣))))) |