| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ghmlin | Structured version Visualization version GIF version | ||
| Description: A homomorphism of groups is linear. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
| Ref | Expression |
|---|---|
| ghmlin.x | ⊢ 𝑋 = (Base‘𝑆) |
| ghmlin.a | ⊢ + = (+g‘𝑆) |
| ghmlin.b | ⊢ ⨣ = (+g‘𝑇) |
| Ref | Expression |
|---|---|
| ghmlin | ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋) → (𝐹‘(𝑈 + 𝑉)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑉))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ghmlin.x | . . . . . 6 ⊢ 𝑋 = (Base‘𝑆) | |
| 2 | eqid 2765 | . . . . . 6 ⊢ (Base‘𝑇) = (Base‘𝑇) | |
| 3 | ghmlin.a | . . . . . 6 ⊢ + = (+g‘𝑆) | |
| 4 | ghmlin.b | . . . . . 6 ⊢ ⨣ = (+g‘𝑇) | |
| 5 | 1, 2, 3, 4 | isghm 19274 | . . . . 5 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋⟶(Base‘𝑇) ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝐹‘(𝑎 + 𝑏)) = ((𝐹‘𝑎) ⨣ (𝐹‘𝑏))))) |
| 6 | 5 | simprbi 502 | . . . 4 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹:𝑋⟶(Base‘𝑇) ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝐹‘(𝑎 + 𝑏)) = ((𝐹‘𝑎) ⨣ (𝐹‘𝑏)))) |
| 7 | 6 | simprd 500 | . . 3 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝐹‘(𝑎 + 𝑏)) = ((𝐹‘𝑎) ⨣ (𝐹‘𝑏))) |
| 8 | fvoveq1 7423 | . . . . 5 ⊢ (𝑎 = 𝑈 → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑈 + 𝑏))) | |
| 9 | fveq2 6871 | . . . . . 6 ⊢ (𝑎 = 𝑈 → (𝐹‘𝑎) = (𝐹‘𝑈)) | |
| 10 | 9 | oveq1d 7415 | . . . . 5 ⊢ (𝑎 = 𝑈 → ((𝐹‘𝑎) ⨣ (𝐹‘𝑏)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑏))) |
| 11 | 8, 10 | eqeq12d 2781 | . . . 4 ⊢ (𝑎 = 𝑈 → ((𝐹‘(𝑎 + 𝑏)) = ((𝐹‘𝑎) ⨣ (𝐹‘𝑏)) ↔ (𝐹‘(𝑈 + 𝑏)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑏)))) |
| 12 | oveq2 7408 | . . . . . 6 ⊢ (𝑏 = 𝑉 → (𝑈 + 𝑏) = (𝑈 + 𝑉)) | |
| 13 | 12 | fveq2d 6875 | . . . . 5 ⊢ (𝑏 = 𝑉 → (𝐹‘(𝑈 + 𝑏)) = (𝐹‘(𝑈 + 𝑉))) |
| 14 | fveq2 6871 | . . . . . 6 ⊢ (𝑏 = 𝑉 → (𝐹‘𝑏) = (𝐹‘𝑉)) | |
| 15 | 14 | oveq2d 7416 | . . . . 5 ⊢ (𝑏 = 𝑉 → ((𝐹‘𝑈) ⨣ (𝐹‘𝑏)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑉))) |
| 16 | 13, 15 | eqeq12d 2781 | . . . 4 ⊢ (𝑏 = 𝑉 → ((𝐹‘(𝑈 + 𝑏)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑏)) ↔ (𝐹‘(𝑈 + 𝑉)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑉)))) |
| 17 | 11, 16 | rspc2v 3595 | . . 3 ⊢ ((𝑈 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋) → (∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝐹‘(𝑎 + 𝑏)) = ((𝐹‘𝑎) ⨣ (𝐹‘𝑏)) → (𝐹‘(𝑈 + 𝑉)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑉)))) |
| 18 | 7, 17 | mpan9 515 | . 2 ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (𝑈 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋)) → (𝐹‘(𝑈 + 𝑉)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑉))) |
| 19 | 18 | 3impb 1130 | 1 ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋) → (𝐹‘(𝑈 + 𝑉)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑉))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 400 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 ∀wral 3079 ⟶wf 6521 ‘cfv 6525 (class class class)co 7400 Basecbs 17257 +gcplusg 17298 Grpcgrp 18988 GrpHom cghm 19271 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5250 ax-nul 5260 ax-pow 5326 ax-pr 5394 ax-un 7722 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-iun 4953 df-br 5105 df-opab 5167 df-mpt 5186 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-fv 6533 df-ov 7403 df-oprab 7404 df-mpo 7405 df-1st 7974 df-2nd 7975 df-map 8814 df-ghm 19272 |
| This theorem is referenced by: ghmid 19280 ghminv 19281 ghmsub 19282 ghmmhm 19284 ghmrn 19287 resghm 19290 ghmpreima 19296 ghmnsgima 19298 ghmnsgpreima 19299 ghmf1o 19306 ghmqusnsglem1 19338 ghmqusnsg 19340 ghmquskerlem1 19341 ghmquskerlem3 19344 lactghmga 19463 invghm 19891 ghmplusg 19904 rhmopp 20580 srngadd 20920 islmhm2 21125 rhmpreimaidl 21375 cygznlem3 21676 psgnco 21690 evpmodpmf1o 21703 ipdir 21746 evlslem1 22190 evladdval 22211 mpfind 22223 evlsaddval 22237 evl1addd 22458 mdetralt 22722 cpmatacl 22830 mat2pmatghm 22844 ghmcnp 24229 ply1rem 26280 dchrptlem2 27383 abliso 33263 rhmimaidl 33651 r1pquslmic 33812 dimkerim 33929 zrhcntr 34281 qqhghm 34290 qqhrhm 34291 fldhmf1 42714 aks6d1c1p3 42734 aks6d1c5lem1 42760 aks6d1c5lem2 42762 aks5lem3a 42813 gicabl 43683 |
| Copyright terms: Public domain | W3C validator |