Metamath Proof Explorer

Theorem clmvneg1

Description: Minus 1 times a vector is the negative of the vector. Equation 2 of Kreyszig p. 51. ( lmodvneg1 analog.) (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses clmvneg1.v ⊢ V = Base W
clmvneg1.n ⊢ N = inv g ⁡ W
clmvneg1.f ⊢ F = Scalar ⁡ W
clmvneg1.s ⊢ · ˙ = ⋅ W
Assertion clmvneg1 ⊢ W ∈ CMod ∧ X ∈ V → -1 · ˙ X = N ⁡ X

Proof

Step Hyp Ref Expression
1 clmvneg1.v ⊢ V = Base W
2 clmvneg1.n ⊢ N = inv g ⁡ W
3 clmvneg1.f ⊢ F = Scalar ⁡ W
4 clmvneg1.s ⊢ · ˙ = ⋅ W
5 eqid ⊢ Base F = Base F
6 3 5 clmzss ⊢ W ∈ CMod → ℤ ⊆ Base F
7 1zzd ⊢ W ∈ CMod → 1 ∈ ℤ
8 6 7 sseldd ⊢ W ∈ CMod → 1 ∈ Base F
9 3 5 clmneg ⊢ W ∈ CMod ∧ 1 ∈ Base F → − 1 = inv g ⁡ F ⁡ 1
10 8 9 mpdan ⊢ W ∈ CMod → − 1 = inv g ⁡ F ⁡ 1
11 3 clm1 ⊢ W ∈ CMod → 1 = 1 F
12 11 fveq2d ⊢ W ∈ CMod → inv g ⁡ F ⁡ 1 = inv g ⁡ F ⁡ 1 F
13 10 12 eqtrd ⊢ W ∈ CMod → − 1 = inv g ⁡ F ⁡ 1 F
14 13 adantr ⊢ W ∈ CMod ∧ X ∈ V → − 1 = inv g ⁡ F ⁡ 1 F
15 14 oveq1d ⊢ W ∈ CMod ∧ X ∈ V → -1 · ˙ X = inv g ⁡ F ⁡ 1 F · ˙ X
16 clmlmod ⊢ W ∈ CMod → W ∈ LMod
17 eqid ⊢ 1 F = 1 F
18 eqid ⊢ inv g ⁡ F = inv g ⁡ F
19 1 2 3 4 17 18 lmodvneg1 ⊢ W ∈ LMod ∧ X ∈ V → inv g ⁡ F ⁡ 1 F · ˙ X = N ⁡ X
20 16 19 sylan ⊢ W ∈ CMod ∧ X ∈ V → inv g ⁡ F ⁡ 1 F · ˙ X = N ⁡ X
21 15 20 eqtrd ⊢ W ∈ CMod ∧ X ∈ V → -1 · ˙ X = N ⁡ X