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 ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lssvnegcl.n ⊢ 𝑁 = ( invg ‘ 𝑊 )
Assertion lssvnegcl ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 lssvnegcl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2 lssvnegcl.n ⊢ 𝑁 = ( invg ‘ 𝑊 )
3 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
4 3 1 lssel ⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
5 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
6 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
7 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) )
8 eqid ⊢ ( invg ‘ ( Scalar ‘ 𝑊 ) ) = ( invg ‘ ( Scalar ‘ 𝑊 ) )
9 3 2 5 6 7 8 lmodvneg1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = ( 𝑁 ‘ 𝑋 ) )
10 4 9 sylan2 ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) ) → ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = ( 𝑁 ‘ 𝑋 ) )
11 10 3impb ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = ( 𝑁 ‘ 𝑋 ) )
12 simp1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → 𝑊 ∈ LMod )
13 simp2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → 𝑈 ∈ 𝑆 )
14 5 lmodring ⊢ ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) ∈ Ring )
15 14 3ad2ant1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → ( Scalar ‘ 𝑊 ) ∈ Ring )
16 ringgrp ⊢ ( ( Scalar ‘ 𝑊 ) ∈ Ring → ( Scalar ‘ 𝑊 ) ∈ Grp )
17 15 16 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → ( Scalar ‘ 𝑊 ) ∈ Grp )
18 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
19 18 7 ringidcl ⊢ ( ( Scalar ‘ 𝑊 ) ∈ Ring → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
20 15 19 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
21 18 8 grpinvcl ⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ Grp ∧ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
22 17 20 21 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
23 simp3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑈 )
24 5 6 18 1 lssvscl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑋 ∈ 𝑈 ) ) → ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ 𝑈 )
25 12 13 22 23 24 syl22anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ 𝑈 )
26 11 25 eqeltrrd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝑈 )