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

Theorem ghmlin 18301
Description: A homomorphism of groups is linear. (Contributed by Stefan O'Rear, 31-Dec-2014.)
Hypotheses
Ref Expression
ghmlin.x 𝑋 = (Base‘𝑆)
ghmlin.a + = (+g𝑆)
ghmlin.b = (+g𝑇)
Assertion
Ref Expression
ghmlin ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈𝑋𝑉𝑋) → (𝐹‘(𝑈 + 𝑉)) = ((𝐹𝑈) (𝐹𝑉)))

Proof of Theorem ghmlin
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ghmlin.x . . . . . 6 𝑋 = (Base‘𝑆)
2 eqid 2818 . . . . . 6 (Base‘𝑇) = (Base‘𝑇)
3 ghmlin.a . . . . . 6 + = (+g𝑆)
4 ghmlin.b . . . . . 6 = (+g𝑇)
51, 2, 3, 4isghm 18296 . . . . 5 (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋⟶(Base‘𝑇) ∧ ∀𝑎𝑋𝑏𝑋 (𝐹‘(𝑎 + 𝑏)) = ((𝐹𝑎) (𝐹𝑏)))))
65simprbi 497 . . . 4 (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹:𝑋⟶(Base‘𝑇) ∧ ∀𝑎𝑋𝑏𝑋 (𝐹‘(𝑎 + 𝑏)) = ((𝐹𝑎) (𝐹𝑏))))
76simprd 496 . . 3 (𝐹 ∈ (𝑆 GrpHom 𝑇) → ∀𝑎𝑋𝑏𝑋 (𝐹‘(𝑎 + 𝑏)) = ((𝐹𝑎) (𝐹𝑏)))
8 fvoveq1 7168 . . . . 5 (𝑎 = 𝑈 → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑈 + 𝑏)))
9 fveq2 6663 . . . . . 6 (𝑎 = 𝑈 → (𝐹𝑎) = (𝐹𝑈))
109oveq1d 7160 . . . . 5 (𝑎 = 𝑈 → ((𝐹𝑎) (𝐹𝑏)) = ((𝐹𝑈) (𝐹𝑏)))
118, 10eqeq12d 2834 . . . 4 (𝑎 = 𝑈 → ((𝐹‘(𝑎 + 𝑏)) = ((𝐹𝑎) (𝐹𝑏)) ↔ (𝐹‘(𝑈 + 𝑏)) = ((𝐹𝑈) (𝐹𝑏))))
12 oveq2 7153 . . . . . 6 (𝑏 = 𝑉 → (𝑈 + 𝑏) = (𝑈 + 𝑉))
1312fveq2d 6667 . . . . 5 (𝑏 = 𝑉 → (𝐹‘(𝑈 + 𝑏)) = (𝐹‘(𝑈 + 𝑉)))
14 fveq2 6663 . . . . . 6 (𝑏 = 𝑉 → (𝐹𝑏) = (𝐹𝑉))
1514oveq2d 7161 . . . . 5 (𝑏 = 𝑉 → ((𝐹𝑈) (𝐹𝑏)) = ((𝐹𝑈) (𝐹𝑉)))
1613, 15eqeq12d 2834 . . . 4 (𝑏 = 𝑉 → ((𝐹‘(𝑈 + 𝑏)) = ((𝐹𝑈) (𝐹𝑏)) ↔ (𝐹‘(𝑈 + 𝑉)) = ((𝐹𝑈) (𝐹𝑉))))
1711, 16rspc2v 3630 . . 3 ((𝑈𝑋𝑉𝑋) → (∀𝑎𝑋𝑏𝑋 (𝐹‘(𝑎 + 𝑏)) = ((𝐹𝑎) (𝐹𝑏)) → (𝐹‘(𝑈 + 𝑉)) = ((𝐹𝑈) (𝐹𝑉))))
187, 17mpan9 507 . 2 ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (𝑈𝑋𝑉𝑋)) → (𝐹‘(𝑈 + 𝑉)) = ((𝐹𝑈) (𝐹𝑉)))
19183impb 1107 1 ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈𝑋𝑉𝑋) → (𝐹‘(𝑈 + 𝑉)) = ((𝐹𝑈) (𝐹𝑉)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079   = wceq 1528  wcel 2105  wral 3135  wf 6344  cfv 6348  (class class class)co 7145  Basecbs 16471  +gcplusg 16553  Grpcgrp 18041   GrpHom cghm 18293
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7148  df-oprab 7149  df-mpo 7150  df-ghm 18294
This theorem is referenced by:  ghmid  18302  ghminv  18303  ghmsub  18304  ghmmhm  18306  ghmrn  18309  resghm  18312  ghmpreima  18318  ghmnsgima  18320  ghmnsgpreima  18321  ghmf1o  18326  lactghmga  18462  invghm  18883  ghmplusg  18895  srngadd  19557  islmhm2  19739  evlslem1  20223  mpfind  20248  evl1addd  20432  cygznlem3  20644  psgnco  20655  evpmodpmf1o  20668  ipdir  20711  mdetralt  21145  cpmatacl  21252  mat2pmatghm  21266  ghmcnp  22650  ply1rem  24684  dchrptlem2  25768  abliso  30610  rhmopp  30819  dimkerim  30922  qqhghm  31128  qqhrhm  31129  gicabl  39577
  Copyright terms: Public domain W3C validator