![]() |
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 2795 | . . . . . 6 ⊢ (Base‘𝑇) = (Base‘𝑇) | |
3 | ghmlin.a | . . . . . 6 ⊢ + = (+g‘𝑆) | |
4 | ghmlin.b | . . . . . 6 ⊢ ⨣ = (+g‘𝑇) | |
5 | 1, 2, 3, 4 | isghm 18099 | . . . . 5 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋⟶(Base‘𝑇) ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝐹‘(𝑎 + 𝑏)) = ((𝐹‘𝑎) ⨣ (𝐹‘𝑏))))) |
6 | 5 | simprbi 497 | . . . 4 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹:𝑋⟶(Base‘𝑇) ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝐹‘(𝑎 + 𝑏)) = ((𝐹‘𝑎) ⨣ (𝐹‘𝑏)))) |
7 | 6 | simprd 496 | . . 3 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝐹‘(𝑎 + 𝑏)) = ((𝐹‘𝑎) ⨣ (𝐹‘𝑏))) |
8 | fvoveq1 7039 | . . . . 5 ⊢ (𝑎 = 𝑈 → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑈 + 𝑏))) | |
9 | fveq2 6538 | . . . . . 6 ⊢ (𝑎 = 𝑈 → (𝐹‘𝑎) = (𝐹‘𝑈)) | |
10 | 9 | oveq1d 7031 | . . . . 5 ⊢ (𝑎 = 𝑈 → ((𝐹‘𝑎) ⨣ (𝐹‘𝑏)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑏))) |
11 | 8, 10 | eqeq12d 2810 | . . . 4 ⊢ (𝑎 = 𝑈 → ((𝐹‘(𝑎 + 𝑏)) = ((𝐹‘𝑎) ⨣ (𝐹‘𝑏)) ↔ (𝐹‘(𝑈 + 𝑏)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑏)))) |
12 | oveq2 7024 | . . . . . 6 ⊢ (𝑏 = 𝑉 → (𝑈 + 𝑏) = (𝑈 + 𝑉)) | |
13 | 12 | fveq2d 6542 | . . . . 5 ⊢ (𝑏 = 𝑉 → (𝐹‘(𝑈 + 𝑏)) = (𝐹‘(𝑈 + 𝑉))) |
14 | fveq2 6538 | . . . . . 6 ⊢ (𝑏 = 𝑉 → (𝐹‘𝑏) = (𝐹‘𝑉)) | |
15 | 14 | oveq2d 7032 | . . . . 5 ⊢ (𝑏 = 𝑉 → ((𝐹‘𝑈) ⨣ (𝐹‘𝑏)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑉))) |
16 | 13, 15 | eqeq12d 2810 | . . . 4 ⊢ (𝑏 = 𝑉 → ((𝐹‘(𝑈 + 𝑏)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑏)) ↔ (𝐹‘(𝑈 + 𝑉)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑉)))) |
17 | 11, 16 | rspc2v 3572 | . . 3 ⊢ ((𝑈 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋) → (∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝐹‘(𝑎 + 𝑏)) = ((𝐹‘𝑎) ⨣ (𝐹‘𝑏)) → (𝐹‘(𝑈 + 𝑉)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑉)))) |
18 | 7, 17 | mpan9 507 | . 2 ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (𝑈 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋)) → (𝐹‘(𝑈 + 𝑉)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑉))) |
19 | 18 | 3impb 1108 | 1 ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋) → (𝐹‘(𝑈 + 𝑉)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑉))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1080 = wceq 1522 ∈ wcel 2081 ∀wral 3105 ⟶wf 6221 ‘cfv 6225 (class class class)co 7016 Basecbs 16312 +gcplusg 16394 Grpcgrp 17861 GrpHom cghm 18096 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-rep 5081 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rex 3111 df-reu 3112 df-rab 3114 df-v 3439 df-sbc 3707 df-csb 3812 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-iun 4827 df-br 4963 df-opab 5025 df-mpt 5042 df-id 5348 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-f1 6230 df-fo 6231 df-f1o 6232 df-fv 6233 df-ov 7019 df-oprab 7020 df-mpo 7021 df-ghm 18097 |
This theorem is referenced by: ghmid 18105 ghminv 18106 ghmsub 18107 ghmmhm 18109 ghmrn 18112 resghm 18115 ghmpreima 18121 ghmnsgima 18123 ghmnsgpreima 18124 ghmf1o 18129 lactghmga 18263 invghm 18679 ghmplusg 18689 srngadd 19318 islmhm2 19500 evlslem1 19982 mpfind 20003 evl1addd 20186 cygznlem3 20398 psgnco 20409 evpmodpmf1o 20422 ipdir 20465 mdetralt 20901 cpmatacl 21008 mat2pmatghm 21022 ghmcnp 22406 ply1rem 24440 dchrptlem2 25523 abliso 30357 rhmopp 30546 dimkerim 30627 qqhghm 30846 qqhrhm 30847 gicabl 39184 |
Copyright terms: Public domain | W3C validator |