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=BaseW
lspsnneg.m M=invgW
lspsnneg.n N=LSpanW
Assertion lspsnneg WLModXVNMX=NX

Proof

Step Hyp Ref Expression
1 lspsnneg.v V=BaseW
2 lspsnneg.m M=invgW
3 lspsnneg.n N=LSpanW
4 eqid ScalarW=ScalarW
5 eqid W=W
6 eqid 1ScalarW=1ScalarW
7 eqid invgScalarW=invgScalarW
8 1 2 4 5 6 7 lmodvneg1 WLModXVinvgScalarW1ScalarWWX=MX
9 8 sneqd WLModXVinvgScalarW1ScalarWWX=MX
10 9 fveq2d WLModXVNinvgScalarW1ScalarWWX=NMX
11 simpl WLModXVWLMod
12 4 lmodfgrp WLModScalarWGrp
13 eqid BaseScalarW=BaseScalarW
14 4 13 6 lmod1cl WLMod1ScalarWBaseScalarW
15 13 7 grpinvcl ScalarWGrp1ScalarWBaseScalarWinvgScalarW1ScalarWBaseScalarW
16 12 14 15 syl2anc WLModinvgScalarW1ScalarWBaseScalarW
17 16 adantr WLModXVinvgScalarW1ScalarWBaseScalarW
18 simpr WLModXVXV
19 4 13 1 5 3 lspsnvsi WLModinvgScalarW1ScalarWBaseScalarWXVNinvgScalarW1ScalarWWXNX
20 11 17 18 19 syl3anc WLModXVNinvgScalarW1ScalarWWXNX
21 10 20 eqsstrrd WLModXVNMXNX
22 1 2 lmodvnegcl WLModXVMXV
23 1 2 4 5 6 7 lmodvneg1 WLModMXVinvgScalarW1ScalarWWMX=MMX
24 22 23 syldan WLModXVinvgScalarW1ScalarWWMX=MMX
25 lmodgrp WLModWGrp
26 1 2 grpinvinv WGrpXVMMX=X
27 25 26 sylan WLModXVMMX=X
28 24 27 eqtrd WLModXVinvgScalarW1ScalarWWMX=X
29 28 sneqd WLModXVinvgScalarW1ScalarWWMX=X
30 29 fveq2d WLModXVNinvgScalarW1ScalarWWMX=NX
31 4 13 1 5 3 lspsnvsi WLModinvgScalarW1ScalarWBaseScalarWMXVNinvgScalarW1ScalarWWMXNMX
32 11 17 22 31 syl3anc WLModXVNinvgScalarW1ScalarWWMXNMX
33 30 32 eqsstrrd WLModXVNXNMX
34 21 33 eqssd WLModXVNMX=NX