Proof of Theorem lmodvneg1
Step | Hyp | Ref
| Expression |
1 | | simpl 476 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑊 ∈ LMod) |
2 | | lmodvneg1.f |
. . . . . . 7
⊢ 𝐹 = (Scalar‘𝑊) |
3 | 2 | lmodfgrp 19235 |
. . . . . 6
⊢ (𝑊 ∈ LMod → 𝐹 ∈ Grp) |
4 | 3 | adantr 474 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝐹 ∈ Grp) |
5 | | eqid 2825 |
. . . . . . 7
⊢
(Base‘𝐹) =
(Base‘𝐹) |
6 | | lmodvneg1.u |
. . . . . . 7
⊢ 1 =
(1r‘𝐹) |
7 | 2, 5, 6 | lmod1cl 19253 |
. . . . . 6
⊢ (𝑊 ∈ LMod → 1 ∈
(Base‘𝐹)) |
8 | 7 | adantr 474 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 1 ∈ (Base‘𝐹)) |
9 | | lmodvneg1.m |
. . . . . 6
⊢ 𝑀 = (invg‘𝐹) |
10 | 5, 9 | grpinvcl 17828 |
. . . . 5
⊢ ((𝐹 ∈ Grp ∧ 1 ∈
(Base‘𝐹)) →
(𝑀‘ 1 ) ∈
(Base‘𝐹)) |
11 | 4, 8, 10 | syl2anc 579 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑀‘ 1 ) ∈ (Base‘𝐹)) |
12 | | simpr 479 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉) |
13 | | lmodvneg1.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑊) |
14 | | lmodvneg1.s |
. . . . 5
⊢ · = (
·𝑠 ‘𝑊) |
15 | 13, 2, 14, 5 | lmodvscl 19243 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ (𝑀‘ 1 ) ∈ (Base‘𝐹) ∧ 𝑋 ∈ 𝑉) → ((𝑀‘ 1 ) · 𝑋) ∈ 𝑉) |
16 | 1, 11, 12, 15 | syl3anc 1494 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑀‘ 1 ) · 𝑋) ∈ 𝑉) |
17 | | eqid 2825 |
. . . 4
⊢
(+g‘𝑊) = (+g‘𝑊) |
18 | | eqid 2825 |
. . . 4
⊢
(0g‘𝑊) = (0g‘𝑊) |
19 | 13, 17, 18 | lmod0vrid 19257 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ ((𝑀‘ 1 ) · 𝑋) ∈ 𝑉) → (((𝑀‘ 1 ) · 𝑋)(+g‘𝑊)(0g‘𝑊)) = ((𝑀‘ 1 ) · 𝑋)) |
20 | 16, 19 | syldan 585 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (((𝑀‘ 1 ) · 𝑋)(+g‘𝑊)(0g‘𝑊)) = ((𝑀‘ 1 ) · 𝑋)) |
21 | | lmodvneg1.n |
. . . . . 6
⊢ 𝑁 = (invg‘𝑊) |
22 | 13, 21 | lmodvnegcl 19267 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘𝑋) ∈ 𝑉) |
23 | 13, 17 | lmodass 19241 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ (((𝑀‘ 1 ) · 𝑋) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ (𝑁‘𝑋) ∈ 𝑉)) → ((((𝑀‘ 1 ) · 𝑋)(+g‘𝑊)𝑋)(+g‘𝑊)(𝑁‘𝑋)) = (((𝑀‘ 1 ) · 𝑋)(+g‘𝑊)(𝑋(+g‘𝑊)(𝑁‘𝑋)))) |
24 | 1, 16, 12, 22, 23 | syl13anc 1495 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((((𝑀‘ 1 ) · 𝑋)(+g‘𝑊)𝑋)(+g‘𝑊)(𝑁‘𝑋)) = (((𝑀‘ 1 ) · 𝑋)(+g‘𝑊)(𝑋(+g‘𝑊)(𝑁‘𝑋)))) |
25 | 13, 2, 14, 6 | lmodvs1 19254 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ( 1 · 𝑋) = 𝑋) |
26 | 25 | oveq2d 6926 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (((𝑀‘ 1 ) · 𝑋)(+g‘𝑊)( 1 · 𝑋)) = (((𝑀‘ 1 ) · 𝑋)(+g‘𝑊)𝑋)) |
27 | | eqid 2825 |
. . . . . . . . . 10
⊢
(+g‘𝐹) = (+g‘𝐹) |
28 | | eqid 2825 |
. . . . . . . . . 10
⊢
(0g‘𝐹) = (0g‘𝐹) |
29 | 5, 27, 28, 9 | grplinv 17829 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Grp ∧ 1 ∈
(Base‘𝐹)) →
((𝑀‘ 1
)(+g‘𝐹)
1 ) =
(0g‘𝐹)) |
30 | 4, 8, 29 | syl2anc 579 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑀‘ 1
)(+g‘𝐹)
1 ) =
(0g‘𝐹)) |
31 | 30 | oveq1d 6925 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (((𝑀‘ 1
)(+g‘𝐹)
1 ) · 𝑋) = ((0g‘𝐹) · 𝑋)) |
32 | 13, 17, 2, 14, 5, 27 | lmodvsdir 19250 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ ((𝑀‘ 1 ) ∈ (Base‘𝐹) ∧ 1 ∈ (Base‘𝐹) ∧ 𝑋 ∈ 𝑉)) → (((𝑀‘ 1
)(+g‘𝐹)
1 ) · 𝑋) = (((𝑀‘ 1 ) · 𝑋)(+g‘𝑊)( 1 · 𝑋))) |
33 | 1, 11, 8, 12, 32 | syl13anc 1495 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (((𝑀‘ 1
)(+g‘𝐹)
1 ) · 𝑋) = (((𝑀‘ 1 ) · 𝑋)(+g‘𝑊)( 1 · 𝑋))) |
34 | 13, 2, 14, 28, 18 | lmod0vs 19259 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((0g‘𝐹) · 𝑋) = (0g‘𝑊)) |
35 | 31, 33, 34 | 3eqtr3d 2869 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (((𝑀‘ 1 ) · 𝑋)(+g‘𝑊)( 1 · 𝑋)) = (0g‘𝑊)) |
36 | 26, 35 | eqtr3d 2863 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (((𝑀‘ 1 ) · 𝑋)(+g‘𝑊)𝑋) = (0g‘𝑊)) |
37 | 36 | oveq1d 6925 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((((𝑀‘ 1 ) · 𝑋)(+g‘𝑊)𝑋)(+g‘𝑊)(𝑁‘𝑋)) = ((0g‘𝑊)(+g‘𝑊)(𝑁‘𝑋))) |
38 | 24, 37 | eqtr3d 2863 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (((𝑀‘ 1 ) · 𝑋)(+g‘𝑊)(𝑋(+g‘𝑊)(𝑁‘𝑋))) = ((0g‘𝑊)(+g‘𝑊)(𝑁‘𝑋))) |
39 | 13, 17, 18, 21 | lmodvnegid 19268 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑋(+g‘𝑊)(𝑁‘𝑋)) = (0g‘𝑊)) |
40 | 39 | oveq2d 6926 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (((𝑀‘ 1 ) · 𝑋)(+g‘𝑊)(𝑋(+g‘𝑊)(𝑁‘𝑋))) = (((𝑀‘ 1 ) · 𝑋)(+g‘𝑊)(0g‘𝑊))) |
41 | 13, 17, 18 | lmod0vlid 19256 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘𝑋) ∈ 𝑉) → ((0g‘𝑊)(+g‘𝑊)(𝑁‘𝑋)) = (𝑁‘𝑋)) |
42 | 22, 41 | syldan 585 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((0g‘𝑊)(+g‘𝑊)(𝑁‘𝑋)) = (𝑁‘𝑋)) |
43 | 38, 40, 42 | 3eqtr3d 2869 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (((𝑀‘ 1 ) · 𝑋)(+g‘𝑊)(0g‘𝑊)) = (𝑁‘𝑋)) |
44 | 20, 43 | eqtr3d 2863 |
1
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑀‘ 1 ) · 𝑋) = (𝑁‘𝑋)) |