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	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
Assertion	clmvneg1	$⊢ (W \in CMod \land X \in V) \to -1 \underset{˙}{\cdot} 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	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
5		eqid	$⊢ {Base}_{F} = {Base}_{F}$
6	3 5	clmzss	$⊢ W \in CMod \to ℤ \subseteq {Base}_{F}$
7		1zzd	$⊢ W \in CMod \to 1 \in ℤ$
8	6 7	sseldd	$⊢ W \in CMod \to 1 \in {Base}_{F}$
9	3 5	clmneg	$⊢ (W \in CMod \land 1 \in {Base}_{F}) \to - 1 = {inv}_{g} (F) (1)$
10	8 9	mpdan	$⊢ W \in CMod \to - 1 = {inv}_{g} (F) (1)$
11	3	clm1	$⊢ W \in CMod \to 1 = 1_{F}$
12	11	fveq2d	$⊢ W \in CMod \to {inv}_{g} (F) (1) = {inv}_{g} (F) (1_{F})$
13	10 12	eqtrd	$⊢ W \in CMod \to - 1 = {inv}_{g} (F) (1_{F})$
14	13	adantr	$⊢ (W \in CMod \land X \in V) \to - 1 = {inv}_{g} (F) (1_{F})$
15	14	oveq1d	$⊢ (W \in CMod \land X \in V) \to -1 \underset{˙}{\cdot} X = {inv}_{g} (F) (1_{F}) \underset{˙}{\cdot} X$
16		clmlmod	$⊢ W \in CMod \to W \in LMod$
17		eqid	$⊢ 1_{F} = 1_{F}$
18		eqid	$⊢ {inv}_{g} (F) = {inv}_{g} (F)$
19	1 2 3 4 17 18	lmodvneg1	$⊢ (W \in LMod \land X \in V) \to {inv}_{g} (F) (1_{F}) \underset{˙}{\cdot} X = N (X)$
20	16 19	sylan	$⊢ (W \in CMod \land X \in V) \to {inv}_{g} (F) (1_{F}) \underset{˙}{\cdot} X = N (X)$
21	15 20	eqtrd	$⊢ (W \in CMod \land X \in V) \to -1 \underset{˙}{\cdot} X = N (X)$

Metamath Proof Explorer

Theorem clmvneg1

Proof