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 | |
|
lspsnneg.m | |
||
lspsnneg.n | |
||
Assertion | lspsnneg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lspsnneg.v | |
|
2 | lspsnneg.m | |
|
3 | lspsnneg.n | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | eqid | |
|
7 | eqid | |
|
8 | 1 2 4 5 6 7 | lmodvneg1 | |
9 | 8 | sneqd | |
10 | 9 | fveq2d | |
11 | simpl | |
|
12 | 4 | lmodfgrp | |
13 | eqid | |
|
14 | 4 13 6 | lmod1cl | |
15 | 13 7 | grpinvcl | |
16 | 12 14 15 | syl2anc | |
17 | 16 | adantr | |
18 | simpr | |
|
19 | 4 13 1 5 3 | lspsnvsi | |
20 | 11 17 18 19 | syl3anc | |
21 | 10 20 | eqsstrrd | |
22 | 1 2 | lmodvnegcl | |
23 | 1 2 4 5 6 7 | lmodvneg1 | |
24 | 22 23 | syldan | |
25 | lmodgrp | |
|
26 | 1 2 | grpinvinv | |
27 | 25 26 | sylan | |
28 | 24 27 | eqtrd | |
29 | 28 | sneqd | |
30 | 29 | fveq2d | |
31 | 4 13 1 5 3 | lspsnvsi | |
32 | 11 17 22 31 | syl3anc | |
33 | 30 32 | eqsstrrd | |
34 | 21 33 | eqssd | |