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

Theorem isghm 17868
Description: Property of being a homomorphism of groups. (Contributed by Stefan O'Rear, 31-Dec-2014.)
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 17866 . . 3 GrpHom = (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑓[(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))})
21elmpt2cl 7023 . 2 (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝑆 ∈ Grp ∧ 𝑇 ∈ Grp))
3 fvex 6342 . . . . . . . 8 (Base‘𝑠) ∈ V
4 feq2 6167 . . . . . . . . 9 (𝑤 = (Base‘𝑠) → (𝑓:𝑤⟶(Base‘𝑡) ↔ 𝑓:(Base‘𝑠)⟶(Base‘𝑡)))
5 raleq 3287 . . . . . . . . . 10 (𝑤 = (Base‘𝑠) → (∀𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ ∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))))
65raleqbi1dv 3295 . . . . . . . . 9 (𝑤 = (Base‘𝑠) → (∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))))
74, 6anbi12d 608 . . . . . . . 8 (𝑤 = (Base‘𝑠) → ((𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))) ↔ (𝑓:(Base‘𝑠)⟶(Base‘𝑡) ∧ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))))
83, 7sbcie 3622 . . . . . . 7 ([(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))) ↔ (𝑓:(Base‘𝑠)⟶(Base‘𝑡) ∧ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))))
9 fveq2 6332 . . . . . . . . . 10 (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆))
10 isghm.w . . . . . . . . . 10 𝑋 = (Base‘𝑆)
119, 10syl6eqr 2823 . . . . . . . . 9 (𝑠 = 𝑆 → (Base‘𝑠) = 𝑋)
1211feq2d 6171 . . . . . . . 8 (𝑠 = 𝑆 → (𝑓:(Base‘𝑠)⟶(Base‘𝑡) ↔ 𝑓:𝑋⟶(Base‘𝑡)))
13 fveq2 6332 . . . . . . . . . . . . . 14 (𝑠 = 𝑆 → (+g𝑠) = (+g𝑆))
14 isghm.a . . . . . . . . . . . . . 14 + = (+g𝑆)
1513, 14syl6eqr 2823 . . . . . . . . . . . . 13 (𝑠 = 𝑆 → (+g𝑠) = + )
1615oveqd 6810 . . . . . . . . . . . 12 (𝑠 = 𝑆 → (𝑢(+g𝑠)𝑣) = (𝑢 + 𝑣))
1716fveq2d 6336 . . . . . . . . . . 11 (𝑠 = 𝑆 → (𝑓‘(𝑢(+g𝑠)𝑣)) = (𝑓‘(𝑢 + 𝑣)))
1817eqeq1d 2773 . . . . . . . . . 10 (𝑠 = 𝑆 → ((𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))))
1911, 18raleqbidv 3301 . . . . . . . . 9 (𝑠 = 𝑆 → (∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ ∀𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))))
2011, 19raleqbidv 3301 . . . . . . . 8 (𝑠 = 𝑆 → (∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))))
2112, 20anbi12d 608 . . . . . . 7 (𝑠 = 𝑆 → ((𝑓:(Base‘𝑠)⟶(Base‘𝑡) ∧ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))) ↔ (𝑓:𝑋⟶(Base‘𝑡) ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))))
228, 21syl5bb 272 . . . . . 6 (𝑠 = 𝑆 → ([(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))) ↔ (𝑓:𝑋⟶(Base‘𝑡) ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))))
2322abbidv 2890 . . . . 5 (𝑠 = 𝑆 → {𝑓[(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))} = {𝑓 ∣ (𝑓:𝑋⟶(Base‘𝑡) ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))})
24 fveq2 6332 . . . . . . . . 9 (𝑡 = 𝑇 → (Base‘𝑡) = (Base‘𝑇))
25 isghm.x . . . . . . . . 9 𝑌 = (Base‘𝑇)
2624, 25syl6eqr 2823 . . . . . . . 8 (𝑡 = 𝑇 → (Base‘𝑡) = 𝑌)
2726feq3d 6172 . . . . . . 7 (𝑡 = 𝑇 → (𝑓:𝑋⟶(Base‘𝑡) ↔ 𝑓:𝑋𝑌))
28 fveq2 6332 . . . . . . . . . . 11 (𝑡 = 𝑇 → (+g𝑡) = (+g𝑇))
29 isghm.b . . . . . . . . . . 11 = (+g𝑇)
3028, 29syl6eqr 2823 . . . . . . . . . 10 (𝑡 = 𝑇 → (+g𝑡) = )
3130oveqd 6810 . . . . . . . . 9 (𝑡 = 𝑇 → ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) = ((𝑓𝑢) (𝑓𝑣)))
3231eqeq2d 2781 . . . . . . . 8 (𝑡 = 𝑇 → ((𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣))))
33322ralbidv 3138 . . . . . . 7 (𝑡 = 𝑇 → (∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣))))
3427, 33anbi12d 608 . . . . . 6 (𝑡 = 𝑇 → ((𝑓:𝑋⟶(Base‘𝑡) ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))))
3534abbidv 2890 . . . . 5 (𝑡 = 𝑇 → {𝑓 ∣ (𝑓:𝑋⟶(Base‘𝑡) ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))} = {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))})
36 fvex 6342 . . . . . . . 8 (Base‘𝑆) ∈ V
3710, 36eqeltri 2846 . . . . . . 7 𝑋 ∈ V
38 fvex 6342 . . . . . . . 8 (Base‘𝑇) ∈ V
3925, 38eqeltri 2846 . . . . . . 7 𝑌 ∈ V
40 mapex 8015 . . . . . . 7 ((𝑋 ∈ V ∧ 𝑌 ∈ V) → {𝑓𝑓:𝑋𝑌} ∈ V)
4137, 39, 40mp2an 664 . . . . . 6 {𝑓𝑓:𝑋𝑌} ∈ V
42 simpl 468 . . . . . . 7 ((𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣))) → 𝑓:𝑋𝑌)
4342ss2abi 3823 . . . . . 6 {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))} ⊆ {𝑓𝑓:𝑋𝑌}
4441, 43ssexi 4937 . . . . 5 {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))} ∈ V
4523, 35, 1, 44ovmpt2 6943 . . . 4 ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝑆 GrpHom 𝑇) = {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))})
4645eleq2d 2836 . . 3 ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ 𝐹 ∈ {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))}))
47 fex 6633 . . . . . 6 ((𝐹:𝑋𝑌𝑋 ∈ V) → 𝐹 ∈ V)
4837, 47mpan2 663 . . . . 5 (𝐹:𝑋𝑌𝐹 ∈ V)
4948adantr 466 . . . 4 ((𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣))) → 𝐹 ∈ V)
50 feq1 6166 . . . . 5 (𝑓 = 𝐹 → (𝑓:𝑋𝑌𝐹:𝑋𝑌))
51 fveq1 6331 . . . . . . 7 (𝑓 = 𝐹 → (𝑓‘(𝑢 + 𝑣)) = (𝐹‘(𝑢 + 𝑣)))
52 fveq1 6331 . . . . . . . 8 (𝑓 = 𝐹 → (𝑓𝑢) = (𝐹𝑢))
53 fveq1 6331 . . . . . . . 8 (𝑓 = 𝐹 → (𝑓𝑣) = (𝐹𝑣))
5452, 53oveq12d 6811 . . . . . . 7 (𝑓 = 𝐹 → ((𝑓𝑢) (𝑓𝑣)) = ((𝐹𝑢) (𝐹𝑣)))
5551, 54eqeq12d 2786 . . . . . 6 (𝑓 = 𝐹 → ((𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)) ↔ (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣))))
56552ralbidv 3138 . . . . 5 (𝑓 = 𝐹 → (∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)) ↔ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣))))
5750, 56anbi12d 608 . . . 4 (𝑓 = 𝐹 → ((𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣))) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣)))))
5849, 57elab3 3509 . . 3 (𝐹 ∈ {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))} ↔ (𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣))))
5946, 58syl6bb 276 . 2 ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣)))))
602, 59biadan2 802 1 (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣)))))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 382   = wceq 1631  wcel 2145  {cab 2757  wral 3061  Vcvv 3351  [wsbc 3587  wf 6027  cfv 6031  (class class class)co 6793  Basecbs 16064  +gcplusg 16149  Grpcgrp 17630   GrpHom cghm 17865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-ghm 17866
This theorem is referenced by:  isghm3  17869  ghmgrp1  17870  ghmgrp2  17871  ghmf  17872  ghmlin  17873  isghmd  17877  idghm  17883  ghmf1o  17898  islmhm2  19251  expghm  20059  mulgghm2  20060  pi1xfr  23074  pi1coghm  23080  rhmopp  30159  isrnghm  42420
  Copyright terms: Public domain W3C validator