MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isghm Structured version   Visualization version   GIF version

Theorem isghm 19245
Description: Property of being a homomorphism of groups. (Contributed by Stefan O'Rear, 31-Dec-2014.) (Proof shortened by SN, 5-Jun-2025.)
Hypotheses
Ref Expression
isghm.w 𝑋 = (Base‘𝑆)
isghm.x 𝑌 = (Base‘𝑇)
isghm.a + = (+g𝑆)
isghm.b = (+g𝑇)
Assertion
Ref Expression
isghm (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣)))))
Distinct variable groups:   𝑣,𝑢,𝑆   𝑢,𝑇,𝑣   𝑢,𝑋,𝑣   𝑢, + ,𝑣   𝑢,𝑌,𝑣   𝑢, ,𝑣   𝑢,𝐹,𝑣

Proof of Theorem isghm
Dummy variables 𝑡 𝑠 𝑤 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ghm 19243 . . 3 GrpHom = (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑓[(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))})
21elmpocl 7673 . 2 (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝑆 ∈ Grp ∧ 𝑇 ∈ Grp))
3 fvex 6919 . . . . . . . 8 (Base‘𝑠) ∈ V
4 feq2 6717 . . . . . . . . 9 (𝑤 = (Base‘𝑠) → (𝑓:𝑤⟶(Base‘𝑡) ↔ 𝑓:(Base‘𝑠)⟶(Base‘𝑡)))
5 raleq 3320 . . . . . . . . . 10 (𝑤 = (Base‘𝑠) → (∀𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ ∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))))
65raleqbi1dv 3335 . . . . . . . . 9 (𝑤 = (Base‘𝑠) → (∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))))
74, 6anbi12d 632 . . . . . . . 8 (𝑤 = (Base‘𝑠) → ((𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))) ↔ (𝑓:(Base‘𝑠)⟶(Base‘𝑡) ∧ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))))
83, 7sbcie 3834 . . . . . . 7 ([(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))) ↔ (𝑓:(Base‘𝑠)⟶(Base‘𝑡) ∧ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))))
9 fveq2 6906 . . . . . . . . . . 11 (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆))
10 isghm.w . . . . . . . . . . 11 𝑋 = (Base‘𝑆)
119, 10eqtr4di 2792 . . . . . . . . . 10 (𝑠 = 𝑆 → (Base‘𝑠) = 𝑋)
1211adantr 480 . . . . . . . . 9 ((𝑠 = 𝑆𝑡 = 𝑇) → (Base‘𝑠) = 𝑋)
13 fveq2 6906 . . . . . . . . . . 11 (𝑡 = 𝑇 → (Base‘𝑡) = (Base‘𝑇))
14 isghm.x . . . . . . . . . . 11 𝑌 = (Base‘𝑇)
1513, 14eqtr4di 2792 . . . . . . . . . 10 (𝑡 = 𝑇 → (Base‘𝑡) = 𝑌)
1615adantl 481 . . . . . . . . 9 ((𝑠 = 𝑆𝑡 = 𝑇) → (Base‘𝑡) = 𝑌)
1712, 16feq23d 6731 . . . . . . . 8 ((𝑠 = 𝑆𝑡 = 𝑇) → (𝑓:(Base‘𝑠)⟶(Base‘𝑡) ↔ 𝑓:𝑋𝑌))
18 fveq2 6906 . . . . . . . . . . . . . 14 (𝑠 = 𝑆 → (+g𝑠) = (+g𝑆))
19 isghm.a . . . . . . . . . . . . . 14 + = (+g𝑆)
2018, 19eqtr4di 2792 . . . . . . . . . . . . 13 (𝑠 = 𝑆 → (+g𝑠) = + )
2120oveqd 7447 . . . . . . . . . . . 12 (𝑠 = 𝑆 → (𝑢(+g𝑠)𝑣) = (𝑢 + 𝑣))
2221fveq2d 6910 . . . . . . . . . . 11 (𝑠 = 𝑆 → (𝑓‘(𝑢(+g𝑠)𝑣)) = (𝑓‘(𝑢 + 𝑣)))
23 fveq2 6906 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → (+g𝑡) = (+g𝑇))
24 isghm.b . . . . . . . . . . . . 13 = (+g𝑇)
2523, 24eqtr4di 2792 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (+g𝑡) = )
2625oveqd 7447 . . . . . . . . . . 11 (𝑡 = 𝑇 → ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) = ((𝑓𝑢) (𝑓𝑣)))
2722, 26eqeqan12d 2748 . . . . . . . . . 10 ((𝑠 = 𝑆𝑡 = 𝑇) → ((𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣))))
2812, 27raleqbidv 3343 . . . . . . . . 9 ((𝑠 = 𝑆𝑡 = 𝑇) → (∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ ∀𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣))))
2912, 28raleqbidv 3343 . . . . . . . 8 ((𝑠 = 𝑆𝑡 = 𝑇) → (∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣))))
3017, 29anbi12d 632 . . . . . . 7 ((𝑠 = 𝑆𝑡 = 𝑇) → ((𝑓:(Base‘𝑠)⟶(Base‘𝑡) ∧ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))))
318, 30bitrid 283 . . . . . 6 ((𝑠 = 𝑆𝑡 = 𝑇) → ([(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))))
3231abbidv 2805 . . . . 5 ((𝑠 = 𝑆𝑡 = 𝑇) → {𝑓[(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))} = {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))})
3314fvexi 6920 . . . . . . 7 𝑌 ∈ V
34 fsetex 8894 . . . . . . 7 (𝑌 ∈ V → {𝑓𝑓:𝑋𝑌} ∈ V)
3533, 34ax-mp 5 . . . . . 6 {𝑓𝑓:𝑋𝑌} ∈ V
36 abanssl 4316 . . . . . 6 {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))} ⊆ {𝑓𝑓:𝑋𝑌}
3735, 36ssexi 5327 . . . . 5 {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))} ∈ V
3832, 1, 37ovmpoa 7587 . . . 4 ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝑆 GrpHom 𝑇) = {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))})
3938eleq2d 2824 . . 3 ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ 𝐹 ∈ {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))}))
4010fvexi 6920 . . . . . 6 𝑋 ∈ V
41 fex2 7956 . . . . . 6 ((𝐹:𝑋𝑌𝑋 ∈ V ∧ 𝑌 ∈ V) → 𝐹 ∈ V)
4240, 33, 41mp3an23 1452 . . . . 5 (𝐹:𝑋𝑌𝐹 ∈ V)
4342adantr 480 . . . 4 ((𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣))) → 𝐹 ∈ V)
44 feq1 6716 . . . . 5 (𝑓 = 𝐹 → (𝑓:𝑋𝑌𝐹:𝑋𝑌))
45 fveq1 6905 . . . . . . 7 (𝑓 = 𝐹 → (𝑓‘(𝑢 + 𝑣)) = (𝐹‘(𝑢 + 𝑣)))
46 fveq1 6905 . . . . . . . 8 (𝑓 = 𝐹 → (𝑓𝑢) = (𝐹𝑢))
47 fveq1 6905 . . . . . . . 8 (𝑓 = 𝐹 → (𝑓𝑣) = (𝐹𝑣))
4846, 47oveq12d 7448 . . . . . . 7 (𝑓 = 𝐹 → ((𝑓𝑢) (𝑓𝑣)) = ((𝐹𝑢) (𝐹𝑣)))
4945, 48eqeq12d 2750 . . . . . 6 (𝑓 = 𝐹 → ((𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)) ↔ (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣))))
50492ralbidv 3218 . . . . 5 (𝑓 = 𝐹 → (∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)) ↔ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣))))
5144, 50anbi12d 632 . . . 4 (𝑓 = 𝐹 → ((𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣))) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣)))))
5243, 51elab3 3688 . . 3 (𝐹 ∈ {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))} ↔ (𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣))))
5339, 52bitrdi 287 . 2 ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣)))))
542, 53biadanii 822 1 (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣)))))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1536  wcel 2105  {cab 2711  wral 3058  Vcvv 3477  [wsbc 3790  wf 6558  cfv 6562  (class class class)co 7430  Basecbs 17244  +gcplusg 17297  Grpcgrp 18963   GrpHom cghm 19242
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-1st 8012  df-2nd 8013  df-map 8866  df-ghm 19243
This theorem is referenced by:  isghm3  19247  ghmgrp1  19248  ghmgrp2  19249  ghmf  19250  ghmlin  19251  isghmd  19255  idghm  19261  ghmf1o  19278  isrnghm  20457  rhmopp  20525  islmhm2  21054  expghm  21503  mulgghm2  21504  pi1xfr  25101  pi1coghm  25107  zringfrac  33561
  Copyright terms: Public domain W3C validator