Metamath Proof Explorer

Theorem lssvnegcl

Description: Closure of negative vectors in a subspace. (Contributed by Stefan O'Rear, 11-Dec-2014)

Ref Expression
Hypotheses lssvnegcl.s ⊢ S = LSubSp ⁡ W
lssvnegcl.n ⊢ N = inv g ⁡ W
Assertion lssvnegcl ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ U → N ⁡ X ∈ U

Proof

Step Hyp Ref Expression
1 lssvnegcl.s ⊢ S = LSubSp ⁡ W
2 lssvnegcl.n ⊢ N = inv g ⁡ W
3 eqid ⊢ Base W = Base W
4 3 1 lssel ⊢ U ∈ S ∧ X ∈ U → X ∈ Base W
5 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
6 eqid ⊢ ⋅ W = ⋅ W
7 eqid ⊢ 1 Scalar ⁡ W = 1 Scalar ⁡ W
8 eqid ⊢ inv g ⁡ Scalar ⁡ W = inv g ⁡ Scalar ⁡ W
9 3 2 5 6 7 8 lmodvneg1 ⊢ W ∈ LMod ∧ X ∈ Base W → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W X = N ⁡ X
10 4 9 sylan2 ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ U → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W X = N ⁡ X
11 10 3impb ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ U → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W X = N ⁡ X
12 simp1 ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ U → W ∈ LMod
13 simp2 ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ U → U ∈ S
14 5 lmodring ⊢ W ∈ LMod → Scalar ⁡ W ∈ Ring
15 14 3ad2ant1 ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ U → Scalar ⁡ W ∈ Ring
16 ringgrp ⊢ Scalar ⁡ W ∈ Ring → Scalar ⁡ W ∈ Grp
17 15 16 syl ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ U → Scalar ⁡ W ∈ Grp
18 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
19 18 7 ringidcl ⊢ Scalar ⁡ W ∈ Ring → 1 Scalar ⁡ W ∈ Base Scalar ⁡ W
20 15 19 syl ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ U → 1 Scalar ⁡ W ∈ Base Scalar ⁡ W
21 18 8 grpinvcl ⊢ Scalar ⁡ W ∈ Grp ∧ 1 Scalar ⁡ W ∈ Base Scalar ⁡ W → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ∈ Base Scalar ⁡ W
22 17 20 21 syl2anc ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ U → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ∈ Base Scalar ⁡ W
23 simp3 ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ U → X ∈ U
24 5 6 18 1 lssvscl ⊢ W ∈ LMod ∧ U ∈ S ∧ inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ∈ Base Scalar ⁡ W ∧ X ∈ U → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W X ∈ U
25 12 13 22 23 24 syl22anc ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ U → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W X ∈ U
26 11 25 eqeltrrd ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ U → N ⁡ X ∈ U