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 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
15 5 lmodring ⊢ W ∈ LMod → Scalar ⁡ W ∈ Ring
16 15 3ad2ant1 ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ U → Scalar ⁡ W ∈ Ring
17 16 ringgrpd ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ U → Scalar ⁡ W ∈ Grp
18 14 7 ringidcl ⊢ Scalar ⁡ W ∈ Ring → 1 Scalar ⁡ W ∈ Base Scalar ⁡ W
19 16 18 syl ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ U → 1 Scalar ⁡ W ∈ Base Scalar ⁡ W
20 14 8 17 19 grpinvcld ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ U → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ∈ Base Scalar ⁡ W
21 simp3 ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ U → X ∈ U
22 5 6 14 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
23 12 13 20 21 22 syl22anc ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ U → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W X ∈ U
24 11 23 eqeltrrd ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ U → N ⁡ X ∈ U