Description: Closure of negative vectors in a subspace. (Contributed by Stefan O'Rear, 11-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lssvnegcl.s | |
|
lssvnegcl.n | |
||
Assertion | lssvnegcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lssvnegcl.s | |
|
2 | lssvnegcl.n | |
|
3 | eqid | |
|
4 | 3 1 | lssel | |
5 | eqid | |
|
6 | eqid | |
|
7 | eqid | |
|
8 | eqid | |
|
9 | 3 2 5 6 7 8 | lmodvneg1 | |
10 | 4 9 | sylan2 | |
11 | 10 | 3impb | |
12 | simp1 | |
|
13 | simp2 | |
|
14 | 5 | lmodring | |
15 | 14 | 3ad2ant1 | |
16 | ringgrp | |
|
17 | 15 16 | syl | |
18 | eqid | |
|
19 | 18 7 | ringidcl | |
20 | 15 19 | syl | |
21 | 18 8 | grpinvcl | |
22 | 17 20 21 | syl2anc | |
23 | simp3 | |
|
24 | 5 6 18 1 | lssvscl | |
25 | 12 13 22 23 24 | syl22anc | |
26 | 11 25 | eqeltrrd | |