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 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑀 ‘ 𝑋 ) } ) = ( 𝑁 ‘ { 𝑋 } ) )