This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
clmvneg1.n ⊢ 𝑁 = ( invg ‘ 𝑊 )
clmvneg1.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
clmvneg1.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
Assertion clmvneg1 ( ( 𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉 ) → ( - 1 · 𝑋 ) = ( 𝑁 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 clmvneg1.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 clmvneg1.n ⊢ 𝑁 = ( invg ‘ 𝑊 )
3 clmvneg1.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 clmvneg1.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
5 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
6 3 5 clmzss ⊢ ( 𝑊 ∈ ℂMod → ℤ ⊆ ( Base ‘ 𝐹 ) )
7 1zzd ⊢ ( 𝑊 ∈ ℂMod → 1 ∈ ℤ )
8 6 7 sseldd ⊢ ( 𝑊 ∈ ℂMod → 1 ∈ ( Base ‘ 𝐹 ) )
9 3 5 clmneg ⊢ ( ( 𝑊 ∈ ℂMod ∧ 1 ∈ ( Base ‘ 𝐹 ) ) → - 1 = ( ( invg ‘ 𝐹 ) ‘ 1 ) )
10 8 9 mpdan ⊢ ( 𝑊 ∈ ℂMod → - 1 = ( ( invg ‘ 𝐹 ) ‘ 1 ) )
11 3 clm1 ⊢ ( 𝑊 ∈ ℂMod → 1 = ( 1r ‘ 𝐹 ) )
12 11 fveq2d ⊢ ( 𝑊 ∈ ℂMod → ( ( invg ‘ 𝐹 ) ‘ 1 ) = ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) )
13 10 12 eqtrd ⊢ ( 𝑊 ∈ ℂMod → - 1 = ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) )
14 13 adantr ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉 ) → - 1 = ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) )
15 14 oveq1d ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉 ) → ( - 1 · 𝑋 ) = ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · 𝑋 ) )
16 clmlmod ⊢ ( 𝑊 ∈ ℂMod → 𝑊 ∈ LMod )
17 eqid ⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
18 eqid ⊢ ( invg ‘ 𝐹 ) = ( invg ‘ 𝐹 )
19 1 2 3 4 17 18 lmodvneg1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · 𝑋 ) = ( 𝑁 ‘ 𝑋 ) )
20 16 19 sylan ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉 ) → ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · 𝑋 ) = ( 𝑁 ‘ 𝑋 ) )
21 15 20 eqtrd ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉 ) → ( - 1 · 𝑋 ) = ( 𝑁 ‘ 𝑋 ) )