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 = inv g ⁡ W
lspsnneg.n ⊢ N = LSpan ⁡ W
Assertion lspsnneg ⊢ W ∈ LMod ∧ X ∈ V → N ⁡ M ⁡ X = N ⁡ X

Proof

Step Hyp Ref Expression
1 lspsnneg.v ⊢ V = Base W
2 lspsnneg.m ⊢ M = inv g ⁡ W
3 lspsnneg.n ⊢ N = LSpan ⁡ W
4 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
5 eqid ⊢ ⋅ W = ⋅ W
6 eqid ⊢ 1 Scalar ⁡ W = 1 Scalar ⁡ W
7 eqid ⊢ inv g ⁡ Scalar ⁡ W = inv g ⁡ Scalar ⁡ W
8 1 2 4 5 6 7 lmodvneg1 ⊢ W ∈ LMod ∧ X ∈ V → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W X = M ⁡ X
9 8 sneqd ⊢ W ∈ LMod ∧ X ∈ V → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W X = M ⁡ X
10 9 fveq2d ⊢ W ∈ LMod ∧ X ∈ V → N ⁡ inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W X = N ⁡ M ⁡ X
11 simpl ⊢ W ∈ LMod ∧ X ∈ V → W ∈ LMod
12 4 lmodfgrp ⊢ W ∈ LMod → Scalar ⁡ W ∈ Grp
13 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
14 4 13 6 lmod1cl ⊢ W ∈ LMod → 1 Scalar ⁡ W ∈ Base Scalar ⁡ W
15 13 7 grpinvcl ⊢ Scalar ⁡ W ∈ Grp ∧ 1 Scalar ⁡ W ∈ Base Scalar ⁡ W → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ∈ Base Scalar ⁡ W
16 12 14 15 syl2anc ⊢ W ∈ LMod → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ∈ Base Scalar ⁡ W
17 16 adantr ⊢ W ∈ LMod ∧ X ∈ V → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ∈ Base Scalar ⁡ W
18 simpr ⊢ W ∈ LMod ∧ X ∈ V → X ∈ V
19 4 13 1 5 3 lspsnvsi ⊢ W ∈ LMod ∧ inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ∈ Base Scalar ⁡ W ∧ X ∈ V → N ⁡ inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W X ⊆ N ⁡ X
20 11 17 18 19 syl3anc ⊢ W ∈ LMod ∧ X ∈ V → N ⁡ inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W X ⊆ N ⁡ X
21 10 20 eqsstrrd ⊢ W ∈ LMod ∧ X ∈ V → N ⁡ M ⁡ X ⊆ N ⁡ X
22 1 2 lmodvnegcl ⊢ W ∈ LMod ∧ X ∈ V → M ⁡ X ∈ V
23 1 2 4 5 6 7 lmodvneg1 ⊢ W ∈ LMod ∧ M ⁡ X ∈ V → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W M ⁡ X = M ⁡ M ⁡ X
24 22 23 syldan ⊢ W ∈ LMod ∧ X ∈ V → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W M ⁡ X = M ⁡ M ⁡ X
25 lmodgrp ⊢ W ∈ LMod → W ∈ Grp
26 1 2 grpinvinv ⊢ W ∈ Grp ∧ X ∈ V → M ⁡ M ⁡ X = X
27 25 26 sylan ⊢ W ∈ LMod ∧ X ∈ V → M ⁡ M ⁡ X = X
28 24 27 eqtrd ⊢ W ∈ LMod ∧ X ∈ V → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W M ⁡ X = X
29 28 sneqd ⊢ W ∈ LMod ∧ X ∈ V → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W M ⁡ X = X
30 29 fveq2d ⊢ W ∈ LMod ∧ X ∈ V → N ⁡ inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W M ⁡ X = N ⁡ X
31 4 13 1 5 3 lspsnvsi ⊢ W ∈ LMod ∧ inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ∈ Base Scalar ⁡ W ∧ M ⁡ X ∈ V → N ⁡ inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W M ⁡ X ⊆ N ⁡ M ⁡ X
32 11 17 22 31 syl3anc ⊢ W ∈ LMod ∧ X ∈ V → N ⁡ inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W M ⁡ X ⊆ N ⁡ M ⁡ X
33 30 32 eqsstrrd ⊢ W ∈ LMod ∧ X ∈ V → N ⁡ X ⊆ N ⁡ M ⁡ X
34 21 33 eqssd ⊢ W ∈ LMod ∧ X ∈ V → N ⁡ M ⁡ X = N ⁡ X