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

Theorem ghmid 18050
Description: A homomorphism of groups preserves the identity. (Contributed by Stefan O'Rear, 31-Dec-2014.)
Hypotheses
Ref Expression
ghmid.y 𝑌 = (0g𝑆)
ghmid.z 0 = (0g𝑇)
Assertion
Ref Expression
ghmid (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹𝑌) = 0 )

Proof of Theorem ghmid
StepHypRef Expression
1 ghmgrp1 18046 . . . . . 6 (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Grp)
2 eqid 2778 . . . . . . 7 (Base‘𝑆) = (Base‘𝑆)
3 ghmid.y . . . . . . 7 𝑌 = (0g𝑆)
42, 3grpidcl 17837 . . . . . 6 (𝑆 ∈ Grp → 𝑌 ∈ (Base‘𝑆))
51, 4syl 17 . . . . 5 (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑌 ∈ (Base‘𝑆))
6 eqid 2778 . . . . . 6 (+g𝑆) = (+g𝑆)
7 eqid 2778 . . . . . 6 (+g𝑇) = (+g𝑇)
82, 6, 7ghmlin 18049 . . . . 5 ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑌 ∈ (Base‘𝑆) ∧ 𝑌 ∈ (Base‘𝑆)) → (𝐹‘(𝑌(+g𝑆)𝑌)) = ((𝐹𝑌)(+g𝑇)(𝐹𝑌)))
95, 5, 8mpd3an23 1536 . . . 4 (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹‘(𝑌(+g𝑆)𝑌)) = ((𝐹𝑌)(+g𝑇)(𝐹𝑌)))
102, 6, 3grplid 17839 . . . . . 6 ((𝑆 ∈ Grp ∧ 𝑌 ∈ (Base‘𝑆)) → (𝑌(+g𝑆)𝑌) = 𝑌)
111, 5, 10syl2anc 579 . . . . 5 (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝑌(+g𝑆)𝑌) = 𝑌)
1211fveq2d 6450 . . . 4 (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹‘(𝑌(+g𝑆)𝑌)) = (𝐹𝑌))
139, 12eqtr3d 2816 . . 3 (𝐹 ∈ (𝑆 GrpHom 𝑇) → ((𝐹𝑌)(+g𝑇)(𝐹𝑌)) = (𝐹𝑌))
14 ghmgrp2 18047 . . . 4 (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑇 ∈ Grp)
15 eqid 2778 . . . . . 6 (Base‘𝑇) = (Base‘𝑇)
162, 15ghmf 18048 . . . . 5 (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇))
1716, 5ffvelrnd 6624 . . . 4 (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹𝑌) ∈ (Base‘𝑇))
18 ghmid.z . . . . 5 0 = (0g𝑇)
1915, 7, 18grpid 17844 . . . 4 ((𝑇 ∈ Grp ∧ (𝐹𝑌) ∈ (Base‘𝑇)) → (((𝐹𝑌)(+g𝑇)(𝐹𝑌)) = (𝐹𝑌) ↔ 0 = (𝐹𝑌)))
2014, 17, 19syl2anc 579 . . 3 (𝐹 ∈ (𝑆 GrpHom 𝑇) → (((𝐹𝑌)(+g𝑇)(𝐹𝑌)) = (𝐹𝑌) ↔ 0 = (𝐹𝑌)))
2113, 20mpbid 224 . 2 (𝐹 ∈ (𝑆 GrpHom 𝑇) → 0 = (𝐹𝑌))
2221eqcomd 2784 1 (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹𝑌) = 0 )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198   = wceq 1601  wcel 2107  cfv 6135  (class class class)co 6922  Basecbs 16255  +gcplusg 16338  0gc0g 16486  Grpcgrp 17809   GrpHom cghm 18041
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-0g 16488  df-mgm 17628  df-sgrp 17670  df-mnd 17681  df-grp 17812  df-ghm 18042
This theorem is referenced by:  ghminv  18051  ghmmhm  18054  ghmpreima  18066  ghmf1  18073  lactghmga  18207  f1ghm0to0  19129  f1rhm0to0OLD  19130  f1rhm0to0ALT  19131  kerf1ghm  19134  kerf1hrmOLD  19135  srng0  19252  islmhm2  19433  evlslem2  19908  evlslem6  19909  evlslem3  19910  zrh0  20258  chrrhm  20275  zndvds0  20294  ip0l  20379  0mat2pmat  20948  nmolb2d  22930  nmoi  22940  nmoix  22941  nmoleub  22943  nmoleub2lem2  23323  nmhmcn  23327  dchrptlem2  25442  dimkerim  30441  psgnid  30445  nrhmzr  42892  zrinitorngc  43019
  Copyright terms: Public domain W3C validator