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 𝑉 = ( Base ‘ 𝑊 )
lspsnneg.m 𝑀 = ( invg𝑊 )
lspsnneg.n 𝑁 = ( LSpan ‘ 𝑊 )
Assertion lspsnneg ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( 𝑁 ‘ { ( 𝑀𝑋 ) } ) = ( 𝑁 ‘ { 𝑋 } ) )

Proof

Step Hyp Ref Expression
1 lspsnneg.v 𝑉 = ( Base ‘ 𝑊 )
2 lspsnneg.m 𝑀 = ( invg𝑊 )
3 lspsnneg.n 𝑁 = ( LSpan ‘ 𝑊 )
4 eqid ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
5 eqid ( ·𝑠𝑊 ) = ( ·𝑠𝑊 )
6 eqid ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) )
7 eqid ( invg ‘ ( Scalar ‘ 𝑊 ) ) = ( invg ‘ ( Scalar ‘ 𝑊 ) )
8 1 2 4 5 6 7 lmodvneg1 ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) = ( 𝑀𝑋 ) )
9 8 sneqd ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → { ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) } = { ( 𝑀𝑋 ) } )
10 9 fveq2d ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( 𝑁 ‘ { ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) } ) = ( 𝑁 ‘ { ( 𝑀𝑋 ) } ) )
11 simpl ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → 𝑊 ∈ LMod )
12 4 lmodfgrp ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) ∈ Grp )
13 eqid ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
14 4 13 6 lmod1cl ( 𝑊 ∈ LMod → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
15 13 7 grpinvcl ( ( ( Scalar ‘ 𝑊 ) ∈ Grp ∧ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
16 12 14 15 syl2anc ( 𝑊 ∈ LMod → ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
17 16 adantr ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
18 simpr ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → 𝑋𝑉 )
19 4 13 1 5 3 lspsnvsi ( ( 𝑊 ∈ LMod ∧ ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑋𝑉 ) → ( 𝑁 ‘ { ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) } ) ⊆ ( 𝑁 ‘ { 𝑋 } ) )
20 11 17 18 19 syl3anc ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( 𝑁 ‘ { ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) } ) ⊆ ( 𝑁 ‘ { 𝑋 } ) )
21 10 20 eqsstrrd ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( 𝑁 ‘ { ( 𝑀𝑋 ) } ) ⊆ ( 𝑁 ‘ { 𝑋 } ) )
22 1 2 lmodvnegcl ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( 𝑀𝑋 ) ∈ 𝑉 )
23 1 2 4 5 6 7 lmodvneg1 ( ( 𝑊 ∈ LMod ∧ ( 𝑀𝑋 ) ∈ 𝑉 ) → ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠𝑊 ) ( 𝑀𝑋 ) ) = ( 𝑀 ‘ ( 𝑀𝑋 ) ) )
24 22 23 syldan ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠𝑊 ) ( 𝑀𝑋 ) ) = ( 𝑀 ‘ ( 𝑀𝑋 ) ) )
25 lmodgrp ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
26 1 2 grpinvinv ( ( 𝑊 ∈ Grp ∧ 𝑋𝑉 ) → ( 𝑀 ‘ ( 𝑀𝑋 ) ) = 𝑋 )
27 25 26 sylan ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( 𝑀 ‘ ( 𝑀𝑋 ) ) = 𝑋 )
28 24 27 eqtrd ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠𝑊 ) ( 𝑀𝑋 ) ) = 𝑋 )
29 28 sneqd ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → { ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠𝑊 ) ( 𝑀𝑋 ) ) } = { 𝑋 } )
30 29 fveq2d ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( 𝑁 ‘ { ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠𝑊 ) ( 𝑀𝑋 ) ) } ) = ( 𝑁 ‘ { 𝑋 } ) )
31 4 13 1 5 3 lspsnvsi ( ( 𝑊 ∈ LMod ∧ ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑀𝑋 ) ∈ 𝑉 ) → ( 𝑁 ‘ { ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠𝑊 ) ( 𝑀𝑋 ) ) } ) ⊆ ( 𝑁 ‘ { ( 𝑀𝑋 ) } ) )
32 11 17 22 31 syl3anc ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( 𝑁 ‘ { ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠𝑊 ) ( 𝑀𝑋 ) ) } ) ⊆ ( 𝑁 ‘ { ( 𝑀𝑋 ) } ) )
33 30 32 eqsstrrd ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { ( 𝑀𝑋 ) } ) )
34 21 33 eqssd ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( 𝑁 ‘ { ( 𝑀𝑋 ) } ) = ( 𝑁 ‘ { 𝑋 } ) )