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	$⊢ V = {Base}_{W}$
	lmodvneg1.n	$⊢ N = {inv}_{g} (W)$
	lmodvneg1.f	$⊢ F = Scalar (W)$
	lmodvneg1.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lmodvneg1.u	$⊢ \underset{˙}{1} = 1_{F}$
	lmodvneg1.m	$⊢ M = {inv}_{g} (F)$
Assertion	lmodvneg1	$⊢ (W \in LMod \land X \in V) \to M (\underset{˙}{1}) \underset{˙}{\cdot} X = N (X)$

Proof

Step	Hyp	Ref	Expression
1		lmodvneg1.v	$⊢ V = {Base}_{W}$
2		lmodvneg1.n	$⊢ N = {inv}_{g} (W)$
3		lmodvneg1.f	$⊢ F = Scalar (W)$
4		lmodvneg1.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
5		lmodvneg1.u	$⊢ \underset{˙}{1} = 1_{F}$
6		lmodvneg1.m	$⊢ M = {inv}_{g} (F)$
7		simpl	$⊢ (W \in LMod \land X \in V) \to W \in LMod$
8	3	lmodfgrp	$⊢ W \in LMod \to F \in Grp$
9		eqid	$⊢ {Base}_{F} = {Base}_{F}$
10	3 9 5	lmod1cl	$⊢ W \in LMod \to \underset{˙}{1} \in {Base}_{F}$
11	10	adantr	$⊢ (W \in LMod \land X \in V) \to \underset{˙}{1} \in {Base}_{F}$
12	9 6	grpinvcl	$⊢ (F \in Grp \land \underset{˙}{1} \in {Base}_{F}) \to M (\underset{˙}{1}) \in {Base}_{F}$
13	8 11 12	syl2an2r	$⊢ (W \in LMod \land X \in V) \to M (\underset{˙}{1}) \in {Base}_{F}$
14		simpr	$⊢ (W \in LMod \land X \in V) \to X \in V$
15	1 3 4 9	lmodvscl	$⊢ (W \in LMod \land M (\underset{˙}{1}) \in {Base}_{F} \land X \in V) \to M (\underset{˙}{1}) \underset{˙}{\cdot} X \in V$
16	7 13 14 15	syl3anc	$⊢ (W \in LMod \land X \in V) \to M (\underset{˙}{1}) \underset{˙}{\cdot} X \in V$
17		eqid	$⊢ +_{W} = +_{W}$
18		eqid	$⊢ 0_{W} = 0_{W}$
19	1 17 18	lmod0vrid	$⊢ (W \in LMod \land M (\underset{˙}{1}) \underset{˙}{\cdot} X \in V) \to (M (\underset{˙}{1}) \underset{˙}{\cdot} X) +_{W} 0_{W} = M (\underset{˙}{1}) \underset{˙}{\cdot} X$
20	16 19	syldan	$⊢ (W \in LMod \land X \in V) \to (M (\underset{˙}{1}) \underset{˙}{\cdot} X) +_{W} 0_{W} = M (\underset{˙}{1}) \underset{˙}{\cdot} X$
21	1 2	lmodvnegcl	$⊢ (W \in LMod \land X \in V) \to N (X) \in V$
22	1 17	lmodass	$⊢ (W \in LMod \land (M (\underset{˙}{1}) \underset{˙}{\cdot} X \in V \land X \in V \land N (X) \in V)) \to ((M (\underset{˙}{1}) \underset{˙}{\cdot} X) +_{W} X) +_{W} N (X) = (M (\underset{˙}{1}) \underset{˙}{\cdot} X) +_{W} (X +_{W} N (X))$
23	7 16 14 21 22	syl13anc	$⊢ (W \in LMod \land X \in V) \to ((M (\underset{˙}{1}) \underset{˙}{\cdot} X) +_{W} X) +_{W} N (X) = (M (\underset{˙}{1}) \underset{˙}{\cdot} X) +_{W} (X +_{W} N (X))$
24	1 3 4 5	lmodvs1	$⊢ (W \in LMod \land X \in V) \to \underset{˙}{1} \underset{˙}{\cdot} X = X$
25	24	oveq2d	$⊢ (W \in LMod \land X \in V) \to (M (\underset{˙}{1}) \underset{˙}{\cdot} X) +_{W} (\underset{˙}{1} \underset{˙}{\cdot} X) = (M (\underset{˙}{1}) \underset{˙}{\cdot} X) +_{W} X$
26		eqid	$⊢ +_{F} = +_{F}$
27		eqid	$⊢ 0_{F} = 0_{F}$
28	9 26 27 6	grplinv	$⊢ (F \in Grp \land \underset{˙}{1} \in {Base}_{F}) \to M (\underset{˙}{1}) +_{F} \underset{˙}{1} = 0_{F}$
29	8 11 28	syl2an2r	$⊢ (W \in LMod \land X \in V) \to M (\underset{˙}{1}) +_{F} \underset{˙}{1} = 0_{F}$
30	29	oveq1d	$⊢ (W \in LMod \land X \in V) \to (M (\underset{˙}{1}) +_{F} \underset{˙}{1}) \underset{˙}{\cdot} X = 0_{F} \underset{˙}{\cdot} X$
31	1 17 3 4 9 26	lmodvsdir	$⊢ (W \in LMod \land (M (\underset{˙}{1}) \in {Base}_{F} \land \underset{˙}{1} \in {Base}_{F} \land X \in V)) \to (M (\underset{˙}{1}) +_{F} \underset{˙}{1}) \underset{˙}{\cdot} X = (M (\underset{˙}{1}) \underset{˙}{\cdot} X) +_{W} (\underset{˙}{1} \underset{˙}{\cdot} X)$
32	7 13 11 14 31	syl13anc	$⊢ (W \in LMod \land X \in V) \to (M (\underset{˙}{1}) +_{F} \underset{˙}{1}) \underset{˙}{\cdot} X = (M (\underset{˙}{1}) \underset{˙}{\cdot} X) +_{W} (\underset{˙}{1} \underset{˙}{\cdot} X)$
33	1 3 4 27 18	lmod0vs	$⊢ (W \in LMod \land X \in V) \to 0_{F} \underset{˙}{\cdot} X = 0_{W}$
34	30 32 33	3eqtr3d	$⊢ (W \in LMod \land X \in V) \to (M (\underset{˙}{1}) \underset{˙}{\cdot} X) +_{W} (\underset{˙}{1} \underset{˙}{\cdot} X) = 0_{W}$
35	25 34	eqtr3d	$⊢ (W \in LMod \land X \in V) \to (M (\underset{˙}{1}) \underset{˙}{\cdot} X) +_{W} X = 0_{W}$
36	35	oveq1d	$⊢ (W \in LMod \land X \in V) \to ((M (\underset{˙}{1}) \underset{˙}{\cdot} X) +_{W} X) +_{W} N (X) = 0_{W} +_{W} N (X)$
37	23 36	eqtr3d	$⊢ (W \in LMod \land X \in V) \to (M (\underset{˙}{1}) \underset{˙}{\cdot} X) +_{W} (X +_{W} N (X)) = 0_{W} +_{W} N (X)$
38	1 17 18 2	lmodvnegid	$⊢ (W \in LMod \land X \in V) \to X +_{W} N (X) = 0_{W}$
39	38	oveq2d	$⊢ (W \in LMod \land X \in V) \to (M (\underset{˙}{1}) \underset{˙}{\cdot} X) +_{W} (X +_{W} N (X)) = (M (\underset{˙}{1}) \underset{˙}{\cdot} X) +_{W} 0_{W}$
40	1 17 18	lmod0vlid	$⊢ (W \in LMod \land N (X) \in V) \to 0_{W} +_{W} N (X) = N (X)$
41	21 40	syldan	$⊢ (W \in LMod \land X \in V) \to 0_{W} +_{W} N (X) = N (X)$
42	37 39 41	3eqtr3d	$⊢ (W \in LMod \land X \in V) \to (M (\underset{˙}{1}) \underset{˙}{\cdot} X) +_{W} 0_{W} = N (X)$
43	20 42	eqtr3d	$⊢ (W \in LMod \land X \in V) \to M (\underset{˙}{1}) \underset{˙}{\cdot} X = N (X)$

Metamath Proof Explorer

Theorem lmodvneg1

Proof