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

Theorem isghm 19008
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 19006 . . 3 GrpHom = (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑓[(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))})
21elmpocl 7595 . 2 (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝑆 ∈ Grp ∧ 𝑇 ∈ Grp))
3 fvex 6855 . . . . . . . 8 (Base‘𝑠) ∈ V
4 feq2 6650 . . . . . . . . 9 (𝑤 = (Base‘𝑠) → (𝑓:𝑤⟶(Base‘𝑡) ↔ 𝑓:(Base‘𝑠)⟶(Base‘𝑡)))
5 raleq 3309 . . . . . . . . . 10 (𝑤 = (Base‘𝑠) → (∀𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ ∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))))
65raleqbi1dv 3307 . . . . . . . . 9 (𝑤 = (Base‘𝑠) → (∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))))
74, 6anbi12d 631 . . . . . . . 8 (𝑤 = (Base‘𝑠) → ((𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))) ↔ (𝑓:(Base‘𝑠)⟶(Base‘𝑡) ∧ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))))
83, 7sbcie 3782 . . . . . . 7 ([(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))) ↔ (𝑓:(Base‘𝑠)⟶(Base‘𝑡) ∧ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))))
9 fveq2 6842 . . . . . . . . . 10 (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆))
10 isghm.w . . . . . . . . . 10 𝑋 = (Base‘𝑆)
119, 10eqtr4di 2794 . . . . . . . . 9 (𝑠 = 𝑆 → (Base‘𝑠) = 𝑋)
1211feq2d 6654 . . . . . . . 8 (𝑠 = 𝑆 → (𝑓:(Base‘𝑠)⟶(Base‘𝑡) ↔ 𝑓:𝑋⟶(Base‘𝑡)))
13 fveq2 6842 . . . . . . . . . . . . 13 (𝑠 = 𝑆 → (+g𝑠) = (+g𝑆))
14 isghm.a . . . . . . . . . . . . 13 + = (+g𝑆)
1513, 14eqtr4di 2794 . . . . . . . . . . . 12 (𝑠 = 𝑆 → (+g𝑠) = + )
1615oveqd 7374 . . . . . . . . . . 11 (𝑠 = 𝑆 → (𝑢(+g𝑠)𝑣) = (𝑢 + 𝑣))
1716fveqeq2d 6850 . . . . . . . . . 10 (𝑠 = 𝑆 → ((𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))))
1811, 17raleqbidv 3319 . . . . . . . . 9 (𝑠 = 𝑆 → (∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ ∀𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))))
1911, 18raleqbidv 3319 . . . . . . . 8 (𝑠 = 𝑆 → (∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))))
2012, 19anbi12d 631 . . . . . . 7 (𝑠 = 𝑆 → ((𝑓:(Base‘𝑠)⟶(Base‘𝑡) ∧ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))) ↔ (𝑓:𝑋⟶(Base‘𝑡) ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))))
218, 20bitrid 282 . . . . . 6 (𝑠 = 𝑆 → ([(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))) ↔ (𝑓:𝑋⟶(Base‘𝑡) ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))))
2221abbidv 2805 . . . . 5 (𝑠 = 𝑆 → {𝑓[(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))} = {𝑓 ∣ (𝑓:𝑋⟶(Base‘𝑡) ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))})
23 fveq2 6842 . . . . . . . . 9 (𝑡 = 𝑇 → (Base‘𝑡) = (Base‘𝑇))
24 isghm.x . . . . . . . . 9 𝑌 = (Base‘𝑇)
2523, 24eqtr4di 2794 . . . . . . . 8 (𝑡 = 𝑇 → (Base‘𝑡) = 𝑌)
2625feq3d 6655 . . . . . . 7 (𝑡 = 𝑇 → (𝑓:𝑋⟶(Base‘𝑡) ↔ 𝑓:𝑋𝑌))
27 fveq2 6842 . . . . . . . . . . 11 (𝑡 = 𝑇 → (+g𝑡) = (+g𝑇))
28 isghm.b . . . . . . . . . . 11 = (+g𝑇)
2927, 28eqtr4di 2794 . . . . . . . . . 10 (𝑡 = 𝑇 → (+g𝑡) = )
3029oveqd 7374 . . . . . . . . 9 (𝑡 = 𝑇 → ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) = ((𝑓𝑢) (𝑓𝑣)))
3130eqeq2d 2747 . . . . . . . 8 (𝑡 = 𝑇 → ((𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣))))
32312ralbidv 3212 . . . . . . 7 (𝑡 = 𝑇 → (∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣))))
3326, 32anbi12d 631 . . . . . 6 (𝑡 = 𝑇 → ((𝑓:𝑋⟶(Base‘𝑡) ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))))
3433abbidv 2805 . . . . 5 (𝑡 = 𝑇 → {𝑓 ∣ (𝑓:𝑋⟶(Base‘𝑡) ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))} = {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))})
3510fvexi 6856 . . . . . . 7 𝑋 ∈ V
3624fvexi 6856 . . . . . . 7 𝑌 ∈ V
37 mapex 8771 . . . . . . 7 ((𝑋 ∈ V ∧ 𝑌 ∈ V) → {𝑓𝑓:𝑋𝑌} ∈ V)
3835, 36, 37mp2an 690 . . . . . 6 {𝑓𝑓:𝑋𝑌} ∈ V
39 simpl 483 . . . . . . 7 ((𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣))) → 𝑓:𝑋𝑌)
4039ss2abi 4023 . . . . . 6 {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))} ⊆ {𝑓𝑓:𝑋𝑌}
4138, 40ssexi 5279 . . . . 5 {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))} ∈ V
4222, 34, 1, 41ovmpo 7515 . . . 4 ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝑆 GrpHom 𝑇) = {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))})
4342eleq2d 2823 . . 3 ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ 𝐹 ∈ {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))}))
44 fex 7176 . . . . . 6 ((𝐹:𝑋𝑌𝑋 ∈ V) → 𝐹 ∈ V)
4535, 44mpan2 689 . . . . 5 (𝐹:𝑋𝑌𝐹 ∈ V)
4645adantr 481 . . . 4 ((𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣))) → 𝐹 ∈ V)
47 feq1 6649 . . . . 5 (𝑓 = 𝐹 → (𝑓:𝑋𝑌𝐹:𝑋𝑌))
48 fveq1 6841 . . . . . . 7 (𝑓 = 𝐹 → (𝑓‘(𝑢 + 𝑣)) = (𝐹‘(𝑢 + 𝑣)))
49 fveq1 6841 . . . . . . . 8 (𝑓 = 𝐹 → (𝑓𝑢) = (𝐹𝑢))
50 fveq1 6841 . . . . . . . 8 (𝑓 = 𝐹 → (𝑓𝑣) = (𝐹𝑣))
5149, 50oveq12d 7375 . . . . . . 7 (𝑓 = 𝐹 → ((𝑓𝑢) (𝑓𝑣)) = ((𝐹𝑢) (𝐹𝑣)))
5248, 51eqeq12d 2752 . . . . . 6 (𝑓 = 𝐹 → ((𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)) ↔ (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣))))
53522ralbidv 3212 . . . . 5 (𝑓 = 𝐹 → (∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)) ↔ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣))))
5447, 53anbi12d 631 . . . 4 (𝑓 = 𝐹 → ((𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣))) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣)))))
5546, 54elab3 3638 . . 3 (𝐹 ∈ {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))} ↔ (𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣))))
5643, 55bitrdi 286 . 2 ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣)))))
572, 56biadanii 820 1 (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣)))))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396   = wceq 1541  wcel 2106  {cab 2713  wral 3064  Vcvv 3445  [wsbc 3739  wf 6492  cfv 6496  (class class class)co 7357  Basecbs 17083  +gcplusg 17133  Grpcgrp 18748   GrpHom cghm 19005
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-ghm 19006
This theorem is referenced by:  isghm3  19009  ghmgrp1  19010  ghmgrp2  19011  ghmf  19012  ghmlin  19013  isghmd  19017  idghm  19023  ghmf1o  19038  rhmopp  20182  islmhm2  20499  expghm  20896  mulgghm2  20897  pi1xfr  24418  pi1coghm  24424  isrnghm  46180
  Copyright terms: Public domain W3C validator