Theorem isghmd 19198

Description: Deduction for a group homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.)

Hypotheses

Ref	Expression
isghmd.x	⊢ 𝑋 = (Base‘𝑆)
isghmd.y	⊢ 𝑌 = (Base‘𝑇)
isghmd.a	⊢ + = (+g‘𝑆)
isghmd.b	⊢ ⨣ = (+g‘𝑇)
isghmd.s	⊢ (𝜑 → 𝑆 ∈ Grp)
isghmd.t	⊢ (𝜑 → 𝑇 ∈ Grp)
isghmd.f	⊢ (𝜑 → 𝐹:𝑋⟶𝑌)
isghmd.l	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))

Assertion

Ref	Expression
isghmd	⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇))

Distinct variable groups:   𝜑,𝑥,𝑦   𝑥,𝐹,𝑦   𝑥,𝑆,𝑦   𝑥,𝑇,𝑦   𝑥, + ,𝑦   𝑥, ⨣ ,𝑦   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦

Proof of Theorem isghmd

Step	Hyp	Ref	Expression
1		isghmd.s	. 2 ⊢ (𝜑 → 𝑆 ∈ Grp)
2		isghmd.t	. 2 ⊢ (𝜑 → 𝑇 ∈ Grp)
3		isghmd.f	. . 3 ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)
4		isghmd.l	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))
5	4	ralrimivva 3183	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))
6	3, 5	jca 516	. 2 ⊢ (𝜑 → (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))))
7		isghmd.x	. . 3 ⊢ 𝑋 = (Base‘𝑆)
8		isghmd.y	. . 3 ⊢ 𝑌 = (Base‘𝑇)
9		isghmd.a	. . 3 ⊢ + = (+g‘𝑆)
10		isghmd.b	. . 3 ⊢ ⨣ = (+g‘𝑇)
11	7, 8, 9, 10	isghm 19188	. 2 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))))
12	1, 2, 6, 11	syl21anbrc 1351	1 ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3054  ⟶wf 6488  ‘cfv 6492  (class class class)co 7363  Basecbs 17177  +_gcplusg 17218  Grpcgrp 18907   GrpHom cghm 19185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-1st 7938  df-2nd 7939  df-map 8772  df-ghm 19186

This theorem is referenced by:  ghmmhmb  19200  resghm  19205  conjghm  19222  qusghm  19228  ghmqusnsg  19255  ghmquskerlem3  19259  invoppggim  19333  galactghm  19377  pj1ghm  19676  frgpup1  19748  mulgghm  19801  ghmfghm  19803  invghm  19806  ghmplusg  19819  ringlghm  20291  ringrghm  20292  isrnghmd  20429  isrhmd  20466  lmodvsghm  20920  pwssplit2  21057  rngqiprngghm  21299  cygznlem3  21551  psgnghm  21562  frlmup1  21780  asclghm  21864  evlslem1  22065  mplmapghm  22105  mat1ghm  22473  scmatghm  22523  mat2pmatghm  22720  pm2mpghm  22806  reefgim  26440  lmodvslmhm  33138  imasghm  33445  qqhghm  34179  aks6d1c6isolem2  42667  frlmsnic  43033  imasgim  43552  amgmlemALT  50300