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