Metamath Proof Explorer


Theorem lspsnneg

Description: Negation does not change the span of a singleton. (Contributed by NM, 24-Apr-2014) (Proof shortened by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lspsnneg.v V = Base W
lspsnneg.m M = inv g W
lspsnneg.n N = LSpan W
Assertion lspsnneg W LMod X V N M X = N X

Proof

Step Hyp Ref Expression
1 lspsnneg.v V = Base W
2 lspsnneg.m M = inv g W
3 lspsnneg.n N = LSpan W
4 eqid Scalar W = Scalar W
5 eqid W = W
6 eqid 1 Scalar W = 1 Scalar W
7 eqid inv g Scalar W = inv g Scalar W
8 1 2 4 5 6 7 lmodvneg1 W LMod X V inv g Scalar W 1 Scalar W W X = M X
9 8 sneqd W LMod X V inv g Scalar W 1 Scalar W W X = M X
10 9 fveq2d W LMod X V N inv g Scalar W 1 Scalar W W X = N M X
11 simpl W LMod X V W LMod
12 4 lmodfgrp W LMod Scalar W Grp
13 eqid Base Scalar W = Base Scalar W
14 4 13 6 lmod1cl W LMod 1 Scalar W Base Scalar W
15 13 7 grpinvcl Scalar W Grp 1 Scalar W Base Scalar W inv g Scalar W 1 Scalar W Base Scalar W
16 12 14 15 syl2anc W LMod inv g Scalar W 1 Scalar W Base Scalar W
17 16 adantr W LMod X V inv g Scalar W 1 Scalar W Base Scalar W
18 simpr W LMod X V X V
19 4 13 1 5 3 lspsnvsi W LMod inv g Scalar W 1 Scalar W Base Scalar W X V N inv g Scalar W 1 Scalar W W X N X
20 11 17 18 19 syl3anc W LMod X V N inv g Scalar W 1 Scalar W W X N X
21 10 20 eqsstrrd W LMod X V N M X N X
22 1 2 lmodvnegcl W LMod X V M X V
23 1 2 4 5 6 7 lmodvneg1 W LMod M X V inv g Scalar W 1 Scalar W W M X = M M X
24 22 23 syldan W LMod X V inv g Scalar W 1 Scalar W W M X = M M X
25 lmodgrp W LMod W Grp
26 1 2 grpinvinv W Grp X V M M X = X
27 25 26 sylan W LMod X V M M X = X
28 24 27 eqtrd W LMod X V inv g Scalar W 1 Scalar W W M X = X
29 28 sneqd W LMod X V inv g Scalar W 1 Scalar W W M X = X
30 29 fveq2d W LMod X V N inv g Scalar W 1 Scalar W W M X = N X
31 4 13 1 5 3 lspsnvsi W LMod inv g Scalar W 1 Scalar W Base Scalar W M X V N inv g Scalar W 1 Scalar W W M X N M X
32 11 17 22 31 syl3anc W LMod X V N inv g Scalar W 1 Scalar W W M X N M X
33 30 32 eqsstrrd W LMod X V N X N M X
34 21 33 eqssd W LMod X V N M X = N X