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 = ( invg ` W )
lspsnneg.n
|- N = ( LSpan ` W )
Assertion lspsnneg
|- ( ( W e. LMod /\ X e. V ) -> ( N ` { ( M ` X ) } ) = ( N ` { X } ) )

Proof

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