Metamath Proof Explorer

Theorem lmodvneg1

Description: Minus 1 times a vector is the negative of the vector. Equation 2 of Kreyszig p. 51. (Contributed by NM, 18-Apr-2014) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lmodvneg1.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lmodvneg1.n ⊢ 𝑁 = ( invg ‘ 𝑊 )
lmodvneg1.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lmodvneg1.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
lmodvneg1.u ⊢ 1 = ( 1r ‘ 𝐹 )
lmodvneg1.m ⊢ 𝑀 = ( invg ‘ 𝐹 )
Assertion lmodvneg1 ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑀 ‘ 1 ) · 𝑋 ) = ( 𝑁 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 lmodvneg1.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lmodvneg1.n ⊢ 𝑁 = ( invg ‘ 𝑊 )
3 lmodvneg1.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 lmodvneg1.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
5 lmodvneg1.u ⊢ 1 = ( 1r ‘ 𝐹 )
6 lmodvneg1.m ⊢ 𝑀 = ( invg ‘ 𝐹 )
7 simpl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → 𝑊 ∈ LMod )
8 3 lmodfgrp ⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Grp )
9 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
10 3 9 5 lmod1cl ⊢ ( 𝑊 ∈ LMod → 1 ∈ ( Base ‘ 𝐹 ) )
11 10 adantr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → 1 ∈ ( Base ‘ 𝐹 ) )
12 9 6 grpinvcl ⊢ ( ( 𝐹 ∈ Grp ∧ 1 ∈ ( Base ‘ 𝐹 ) ) → ( 𝑀 ‘ 1 ) ∈ ( Base ‘ 𝐹 ) )
13 8 11 12 syl2an2r ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 ‘ 1 ) ∈ ( Base ‘ 𝐹 ) )
14 simpr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
15 1 3 4 9 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑀 ‘ 1 ) ∈ ( Base ‘ 𝐹 ) ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑀 ‘ 1 ) · 𝑋 ) ∈ 𝑉 )
16 7 13 14 15 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑀 ‘ 1 ) · 𝑋 ) ∈ 𝑉 )
17 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
18 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
19 1 17 18 lmod0vrid ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑀 ‘ 1 ) · 𝑋 ) ∈ 𝑉 ) → ( ( ( 𝑀 ‘ 1 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = ( ( 𝑀 ‘ 1 ) · 𝑋 ) )
20 16 19 syldan ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝑀 ‘ 1 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = ( ( 𝑀 ‘ 1 ) · 𝑋 ) )
21 1 2 lmodvnegcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝑉 )
22 1 17 lmodass ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( ( 𝑀 ‘ 1 ) · 𝑋 ) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝑉 ) ) → ( ( ( ( 𝑀 ‘ 1 ) · 𝑋 ) ( +g ‘ 𝑊 ) 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) = ( ( ( 𝑀 ‘ 1 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) ) )
23 7 16 14 21 22 syl13anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( ( ( 𝑀 ‘ 1 ) · 𝑋 ) ( +g ‘ 𝑊 ) 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) = ( ( ( 𝑀 ‘ 1 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) ) )
24 1 3 4 5 lmodvs1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 1 · 𝑋 ) = 𝑋 )
25 24 oveq2d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝑀 ‘ 1 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 1 · 𝑋 ) ) = ( ( ( 𝑀 ‘ 1 ) · 𝑋 ) ( +g ‘ 𝑊 ) 𝑋 ) )
26 eqid ⊢ ( +g ‘ 𝐹 ) = ( +g ‘ 𝐹 )
27 eqid ⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
28 9 26 27 6 grplinv ⊢ ( ( 𝐹 ∈ Grp ∧ 1 ∈ ( Base ‘ 𝐹 ) ) → ( ( 𝑀 ‘ 1 ) ( +g ‘ 𝐹 ) 1 ) = ( 0g ‘ 𝐹 ) )
29 8 11 28 syl2an2r ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑀 ‘ 1 ) ( +g ‘ 𝐹 ) 1 ) = ( 0g ‘ 𝐹 ) )
30 29 oveq1d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝑀 ‘ 1 ) ( +g ‘ 𝐹 ) 1 ) · 𝑋 ) = ( ( 0g ‘ 𝐹 ) · 𝑋 ) )
31 1 17 3 4 9 26 lmodvsdir ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑀 ‘ 1 ) ∈ ( Base ‘ 𝐹 ) ∧ 1 ∈ ( Base ‘ 𝐹 ) ∧ 𝑋 ∈ 𝑉 ) ) → ( ( ( 𝑀 ‘ 1 ) ( +g ‘ 𝐹 ) 1 ) · 𝑋 ) = ( ( ( 𝑀 ‘ 1 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 1 · 𝑋 ) ) )
32 7 13 11 14 31 syl13anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝑀 ‘ 1 ) ( +g ‘ 𝐹 ) 1 ) · 𝑋 ) = ( ( ( 𝑀 ‘ 1 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 1 · 𝑋 ) ) )
33 1 3 4 27 18 lmod0vs ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 0g ‘ 𝐹 ) · 𝑋 ) = ( 0g ‘ 𝑊 ) )
34 30 32 33 3eqtr3d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝑀 ‘ 1 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 1 · 𝑋 ) ) = ( 0g ‘ 𝑊 ) )
35 25 34 eqtr3d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝑀 ‘ 1 ) · 𝑋 ) ( +g ‘ 𝑊 ) 𝑋 ) = ( 0g ‘ 𝑊 ) )
36 35 oveq1d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( ( ( 𝑀 ‘ 1 ) · 𝑋 ) ( +g ‘ 𝑊 ) 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) = ( ( 0g ‘ 𝑊 ) ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) )
37 23 36 eqtr3d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝑀 ‘ 1 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) ) = ( ( 0g ‘ 𝑊 ) ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) )
38 1 17 18 2 lmodvnegid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) = ( 0g ‘ 𝑊 ) )
39 38 oveq2d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝑀 ‘ 1 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) ) = ( ( ( 𝑀 ‘ 1 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) )
40 1 17 18 lmod0vlid ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝑉 ) → ( ( 0g ‘ 𝑊 ) ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) = ( 𝑁 ‘ 𝑋 ) )
41 21 40 syldan ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 0g ‘ 𝑊 ) ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) = ( 𝑁 ‘ 𝑋 ) )
42 37 39 41 3eqtr3d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝑀 ‘ 1 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = ( 𝑁 ‘ 𝑋 ) )
43 20 42 eqtr3d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑀 ‘ 1 ) · 𝑋 ) = ( 𝑁 ‘ 𝑋 ) )