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 } ) )