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

Theorem isghmOLD 19234
Description: Obsolete version of isghm 19233 as of 5-Jun-2025. (Contributed by Stefan O'Rear, 31-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
isghm.w 𝑋 = (Base‘𝑆)
isghm.x 𝑌 = (Base‘𝑇)
isghm.a + = (+g𝑆)
isghm.b = (+g𝑇)
Assertion
Ref Expression
isghmOLD (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣)))))
Distinct variable groups:   𝑣,𝑢,𝑆   𝑢,𝑇,𝑣   𝑢,𝑋,𝑣   𝑢, + ,𝑣   𝑢,𝑌,𝑣   𝑢, ,𝑣   𝑢,𝐹,𝑣

Proof of Theorem isghmOLD
Dummy variables 𝑡 𝑠 𝑤 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ghm 19231 . . 3 GrpHom = (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑓[(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))})
21elmpocl 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𝑡)(𝑓𝑣))))
65raleqbi1dv 3338 . . . . . . . . 9 (𝑤 = (Base‘𝑠) → (∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))))
74, 6anbi12d 632 . . . . . . . 8 (𝑤 = (Base‘𝑠) → ((𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))) ↔ (𝑓:(Base‘𝑠)⟶(Base‘𝑡) ∧ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))))
83, 7sbcie 3830 . . . . . . 7 ([(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))) ↔ (𝑓:(Base‘𝑠)⟶(Base‘𝑡) ∧ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))))
9 fveq2 6906 . . . . . . . . . 10 (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆))
10 isghm.w . . . . . . . . . 10 𝑋 = (Base‘𝑆)
119, 10eqtr4di 2795 . . . . . . . . 9 (𝑠 = 𝑆 → (Base‘𝑠) = 𝑋)
1211feq2d 6722 . . . . . . . 8 (𝑠 = 𝑆 → (𝑓:(Base‘𝑠)⟶(Base‘𝑡) ↔ 𝑓:𝑋⟶(Base‘𝑡)))
13 fveq2 6906 . . . . . . . . . . . . 13 (𝑠 = 𝑆 → (+g𝑠) = (+g𝑆))
14 isghm.a . . . . . . . . . . . . 13 + = (+g𝑆)
1513, 14eqtr4di 2795 . . . . . . . . . . . 12 (𝑠 = 𝑆 → (+g𝑠) = + )
1615oveqd 7448 . . . . . . . . . . 11 (𝑠 = 𝑆 → (𝑢(+g𝑠)𝑣) = (𝑢 + 𝑣))
1716fveqeq2d 6914 . . . . . . . . . 10 (𝑠 = 𝑆 → ((𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))))
1811, 17raleqbidv 3346 . . . . . . . . 9 (𝑠 = 𝑆 → (∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ ∀𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))))
1911, 18raleqbidv 3346 . . . . . . . 8 (𝑠 = 𝑆 → (∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))))
2012, 19anbi12d 632 . . . . . . 7 (𝑠 = 𝑆 → ((𝑓:(Base‘𝑠)⟶(Base‘𝑡) ∧ ∀𝑢 ∈ (Base‘𝑠)∀𝑣 ∈ (Base‘𝑠)(𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))) ↔ (𝑓:𝑋⟶(Base‘𝑡) ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))))
218, 20bitrid 283 . . . . . 6 (𝑠 = 𝑆 → ([(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))) ↔ (𝑓:𝑋⟶(Base‘𝑡) ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))))
2221abbidv 2808 . . . . 5 (𝑠 = 𝑆 → {𝑓[(Base‘𝑠) / 𝑤](𝑓:𝑤⟶(Base‘𝑡) ∧ ∀𝑢𝑤𝑣𝑤 (𝑓‘(𝑢(+g𝑠)𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))} = {𝑓 ∣ (𝑓:𝑋⟶(Base‘𝑡) ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))})
23 fveq2 6906 . . . . . . . . 9 (𝑡 = 𝑇 → (Base‘𝑡) = (Base‘𝑇))
24 isghm.x . . . . . . . . 9 𝑌 = (Base‘𝑇)
2523, 24eqtr4di 2795 . . . . . . . 8 (𝑡 = 𝑇 → (Base‘𝑡) = 𝑌)
2625feq3d 6723 . . . . . . 7 (𝑡 = 𝑇 → (𝑓:𝑋⟶(Base‘𝑡) ↔ 𝑓:𝑋𝑌))
27 fveq2 6906 . . . . . . . . . . 11 (𝑡 = 𝑇 → (+g𝑡) = (+g𝑇))
28 isghm.b . . . . . . . . . . 11 = (+g𝑇)
2927, 28eqtr4di 2795 . . . . . . . . . 10 (𝑡 = 𝑇 → (+g𝑡) = )
3029oveqd 7448 . . . . . . . . 9 (𝑡 = 𝑇 → ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) = ((𝑓𝑢) (𝑓𝑣)))
3130eqeq2d 2748 . . . . . . . 8 (𝑡 = 𝑇 → ((𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣))))
32312ralbidv 3221 . . . . . . 7 (𝑡 = 𝑇 → (∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)) ↔ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣))))
3326, 32anbi12d 632 . . . . . 6 (𝑡 = 𝑇 → ((𝑓:𝑋⟶(Base‘𝑡) ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣))) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))))
3433abbidv 2808 . . . . 5 (𝑡 = 𝑇 → {𝑓 ∣ (𝑓:𝑋⟶(Base‘𝑡) ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢)(+g𝑡)(𝑓𝑣)))} = {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))})
3510fvexi 6920 . . . . . . 7 𝑋 ∈ V
3624fvexi 6920 . . . . . . 7 𝑌 ∈ V
37 mapex 7963 . . . . . . 7 ((𝑋 ∈ V ∧ 𝑌 ∈ V) → {𝑓𝑓:𝑋𝑌} ∈ V)
3835, 36, 37mp2an 692 . . . . . 6 {𝑓𝑓:𝑋𝑌} ∈ V
39 simpl 482 . . . . . . 7 ((𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣))) → 𝑓:𝑋𝑌)
4039ss2abi 4067 . . . . . 6 {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))} ⊆ {𝑓𝑓:𝑋𝑌}
4138, 40ssexi 5322 . . . . 5 {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))} ∈ V
4222, 34, 1, 41ovmpo 7593 . . . 4 ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝑆 GrpHom 𝑇) = {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))})
4342eleq2d 2827 . . 3 ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ 𝐹 ∈ {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))}))
44 fex 7246 . . . . . 6 ((𝐹:𝑋𝑌𝑋 ∈ V) → 𝐹 ∈ V)
4535, 44mpan2 691 . . . . 5 (𝐹:𝑋𝑌𝐹 ∈ V)
4645adantr 480 . . . 4 ((𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣))) → 𝐹 ∈ V)
47 feq1 6716 . . . . 5 (𝑓 = 𝐹 → (𝑓:𝑋𝑌𝐹:𝑋𝑌))
48 fveq1 6905 . . . . . . 7 (𝑓 = 𝐹 → (𝑓‘(𝑢 + 𝑣)) = (𝐹‘(𝑢 + 𝑣)))
49 fveq1 6905 . . . . . . . 8 (𝑓 = 𝐹 → (𝑓𝑢) = (𝐹𝑢))
50 fveq1 6905 . . . . . . . 8 (𝑓 = 𝐹 → (𝑓𝑣) = (𝐹𝑣))
5149, 50oveq12d 7449 . . . . . . 7 (𝑓 = 𝐹 → ((𝑓𝑢) (𝑓𝑣)) = ((𝐹𝑢) (𝐹𝑣)))
5248, 51eqeq12d 2753 . . . . . 6 (𝑓 = 𝐹 → ((𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)) ↔ (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣))))
53522ralbidv 3221 . . . . 5 (𝑓 = 𝐹 → (∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)) ↔ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣))))
5447, 53anbi12d 632 . . . 4 (𝑓 = 𝐹 → ((𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣))) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣)))))
5546, 54elab3 3686 . . 3 (𝐹 ∈ {𝑓 ∣ (𝑓:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝑓‘(𝑢 + 𝑣)) = ((𝑓𝑢) (𝑓𝑣)))} ↔ (𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣))))
5643, 55bitrdi 287 . 2 ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣)))))
572, 56biadanii 822 1 (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑢𝑋𝑣𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹𝑢) (𝐹𝑣)))))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1540  wcel 2108  {cab 2714  wral 3061  Vcvv 3480  [wsbc 3788  wf 6557  cfv 6561  (class class class)co 7431  Basecbs 17247  +gcplusg 17297  Grpcgrp 18951   GrpHom cghm 19230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-ghm 19231
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator