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 · 𝑋 ) = ( 𝑁 ‘ 𝑋 ) )