Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > lmhmlin | Structured version Visualization version GIF version |
Description: A homomorphism of left modules is 𝐾-linear. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
Ref | Expression |
---|---|
lmhmlin.k | ⊢ 𝐾 = (Scalar‘𝑆) |
lmhmlin.b | ⊢ 𝐵 = (Base‘𝐾) |
lmhmlin.e | ⊢ 𝐸 = (Base‘𝑆) |
lmhmlin.m | ⊢ · = ( ·𝑠 ‘𝑆) |
lmhmlin.n | ⊢ × = ( ·𝑠 ‘𝑇) |
Ref | Expression |
---|---|
lmhmlin | ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐸) → (𝐹‘(𝑋 · 𝑌)) = (𝑋 × (𝐹‘𝑌))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lmhmlin.k | . . . . . 6 ⊢ 𝐾 = (Scalar‘𝑆) | |
2 | eqid 2738 | . . . . . 6 ⊢ (Scalar‘𝑇) = (Scalar‘𝑇) | |
3 | lmhmlin.b | . . . . . 6 ⊢ 𝐵 = (Base‘𝐾) | |
4 | lmhmlin.e | . . . . . 6 ⊢ 𝐸 = (Base‘𝑆) | |
5 | lmhmlin.m | . . . . . 6 ⊢ · = ( ·𝑠 ‘𝑆) | |
6 | lmhmlin.n | . . . . . 6 ⊢ × = ( ·𝑠 ‘𝑇) | |
7 | 1, 2, 3, 4, 5, 6 | islmhm 19911 | . . . . 5 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) ↔ ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (Scalar‘𝑇) = 𝐾 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐸 (𝐹‘(𝑎 · 𝑏)) = (𝑎 × (𝐹‘𝑏))))) |
8 | 7 | simprbi 500 | . . . 4 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (Scalar‘𝑇) = 𝐾 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐸 (𝐹‘(𝑎 · 𝑏)) = (𝑎 × (𝐹‘𝑏)))) |
9 | 8 | simp3d 1145 | . . 3 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐸 (𝐹‘(𝑎 · 𝑏)) = (𝑎 × (𝐹‘𝑏))) |
10 | fvoveq1 7187 | . . . . 5 ⊢ (𝑎 = 𝑋 → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑋 · 𝑏))) | |
11 | oveq1 7171 | . . . . 5 ⊢ (𝑎 = 𝑋 → (𝑎 × (𝐹‘𝑏)) = (𝑋 × (𝐹‘𝑏))) | |
12 | 10, 11 | eqeq12d 2754 | . . . 4 ⊢ (𝑎 = 𝑋 → ((𝐹‘(𝑎 · 𝑏)) = (𝑎 × (𝐹‘𝑏)) ↔ (𝐹‘(𝑋 · 𝑏)) = (𝑋 × (𝐹‘𝑏)))) |
13 | oveq2 7172 | . . . . . 6 ⊢ (𝑏 = 𝑌 → (𝑋 · 𝑏) = (𝑋 · 𝑌)) | |
14 | 13 | fveq2d 6672 | . . . . 5 ⊢ (𝑏 = 𝑌 → (𝐹‘(𝑋 · 𝑏)) = (𝐹‘(𝑋 · 𝑌))) |
15 | fveq2 6668 | . . . . . 6 ⊢ (𝑏 = 𝑌 → (𝐹‘𝑏) = (𝐹‘𝑌)) | |
16 | 15 | oveq2d 7180 | . . . . 5 ⊢ (𝑏 = 𝑌 → (𝑋 × (𝐹‘𝑏)) = (𝑋 × (𝐹‘𝑌))) |
17 | 14, 16 | eqeq12d 2754 | . . . 4 ⊢ (𝑏 = 𝑌 → ((𝐹‘(𝑋 · 𝑏)) = (𝑋 × (𝐹‘𝑏)) ↔ (𝐹‘(𝑋 · 𝑌)) = (𝑋 × (𝐹‘𝑌)))) |
18 | 12, 17 | rspc2v 3534 | . . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐸) → (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐸 (𝐹‘(𝑎 · 𝑏)) = (𝑎 × (𝐹‘𝑏)) → (𝐹‘(𝑋 · 𝑌)) = (𝑋 × (𝐹‘𝑌)))) |
19 | 9, 18 | syl5com 31 | . 2 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐸) → (𝐹‘(𝑋 · 𝑌)) = (𝑋 × (𝐹‘𝑌)))) |
20 | 19 | 3impib 1117 | 1 ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐸) → (𝐹‘(𝑋 · 𝑌)) = (𝑋 × (𝐹‘𝑌))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1088 = wceq 1542 ∈ wcel 2113 ∀wral 3053 ‘cfv 6333 (class class class)co 7164 Basecbs 16579 Scalarcsca 16664 ·𝑠 cvsca 16665 GrpHom cghm 18466 LModclmod 19746 LMHom clmhm 19903 |
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 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-sep 5164 ax-nul 5171 ax-pr 5293 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3399 df-sbc 3680 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-nul 4210 df-if 4412 df-sn 4514 df-pr 4516 df-op 4520 df-uni 4794 df-br 5028 df-opab 5090 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-iota 6291 df-fun 6335 df-fv 6341 df-ov 7167 df-oprab 7168 df-mpo 7169 df-lmhm 19906 |
This theorem is referenced by: islmhm2 19922 lmhmco 19927 lmhmplusg 19928 lmhmvsca 19929 lmhmf1o 19930 lmhmima 19931 lmhmpreima 19932 reslmhm 19936 reslmhm2 19937 reslmhm2b 19938 lmhmeql 19939 ipass 20454 lindfmm 20636 nmoleub2lem3 23860 nmoleub3 23864 mendassa 40575 |
Copyright terms: Public domain | W3C validator |