Step |
Hyp |
Ref |
Expression |
1 |
|
psgnsn.0 |
|- D = { A } |
2 |
|
psgnsn.g |
|- G = ( SymGrp ` D ) |
3 |
|
psgnsn.b |
|- B = ( Base ` G ) |
4 |
|
psgnsn.n |
|- N = ( pmSgn ` D ) |
5 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
6 |
5
|
gsum0 |
|- ( G gsum (/) ) = ( 0g ` G ) |
7 |
2 3 1
|
symg1bas |
|- ( A e. V -> B = { { <. A , A >. } } ) |
8 |
7
|
eleq2d |
|- ( A e. V -> ( X e. B <-> X e. { { <. A , A >. } } ) ) |
9 |
8
|
biimpa |
|- ( ( A e. V /\ X e. B ) -> X e. { { <. A , A >. } } ) |
10 |
|
elsni |
|- ( X e. { { <. A , A >. } } -> X = { <. A , A >. } ) |
11 |
1
|
reseq2i |
|- ( _I |` D ) = ( _I |` { A } ) |
12 |
|
snex |
|- { A } e. _V |
13 |
12
|
snid |
|- { A } e. { { A } } |
14 |
1 13
|
eqeltri |
|- D e. { { A } } |
15 |
2
|
symgid |
|- ( D e. { { A } } -> ( _I |` D ) = ( 0g ` G ) ) |
16 |
14 15
|
mp1i |
|- ( A e. V -> ( _I |` D ) = ( 0g ` G ) ) |
17 |
|
restidsing |
|- ( _I |` { A } ) = ( { A } X. { A } ) |
18 |
|
xpsng |
|- ( ( A e. V /\ A e. V ) -> ( { A } X. { A } ) = { <. A , A >. } ) |
19 |
18
|
anidms |
|- ( A e. V -> ( { A } X. { A } ) = { <. A , A >. } ) |
20 |
17 19
|
syl5eq |
|- ( A e. V -> ( _I |` { A } ) = { <. A , A >. } ) |
21 |
11 16 20
|
3eqtr3a |
|- ( A e. V -> ( 0g ` G ) = { <. A , A >. } ) |
22 |
21
|
adantr |
|- ( ( A e. V /\ X e. B ) -> ( 0g ` G ) = { <. A , A >. } ) |
23 |
|
id |
|- ( { <. A , A >. } = X -> { <. A , A >. } = X ) |
24 |
23
|
eqcoms |
|- ( X = { <. A , A >. } -> { <. A , A >. } = X ) |
25 |
22 24
|
sylan9eqr |
|- ( ( X = { <. A , A >. } /\ ( A e. V /\ X e. B ) ) -> ( 0g ` G ) = X ) |
26 |
25
|
ex |
|- ( X = { <. A , A >. } -> ( ( A e. V /\ X e. B ) -> ( 0g ` G ) = X ) ) |
27 |
10 26
|
syl |
|- ( X e. { { <. A , A >. } } -> ( ( A e. V /\ X e. B ) -> ( 0g ` G ) = X ) ) |
28 |
9 27
|
mpcom |
|- ( ( A e. V /\ X e. B ) -> ( 0g ` G ) = X ) |
29 |
6 28
|
eqtr2id |
|- ( ( A e. V /\ X e. B ) -> X = ( G gsum (/) ) ) |
30 |
29
|
fveq2d |
|- ( ( A e. V /\ X e. B ) -> ( N ` X ) = ( N ` ( G gsum (/) ) ) ) |
31 |
1 12
|
eqeltri |
|- D e. _V |
32 |
|
wrd0 |
|- (/) e. Word (/) |
33 |
31 32
|
pm3.2i |
|- ( D e. _V /\ (/) e. Word (/) ) |
34 |
1
|
fveq2i |
|- ( pmTrsp ` D ) = ( pmTrsp ` { A } ) |
35 |
|
pmtrsn |
|- ( pmTrsp ` { A } ) = (/) |
36 |
34 35
|
eqtri |
|- ( pmTrsp ` D ) = (/) |
37 |
36
|
rneqi |
|- ran ( pmTrsp ` D ) = ran (/) |
38 |
|
rn0 |
|- ran (/) = (/) |
39 |
37 38
|
eqtr2i |
|- (/) = ran ( pmTrsp ` D ) |
40 |
2 39 4
|
psgnvalii |
|- ( ( D e. _V /\ (/) e. Word (/) ) -> ( N ` ( G gsum (/) ) ) = ( -u 1 ^ ( # ` (/) ) ) ) |
41 |
33 40
|
mp1i |
|- ( ( A e. V /\ X e. B ) -> ( N ` ( G gsum (/) ) ) = ( -u 1 ^ ( # ` (/) ) ) ) |
42 |
|
hash0 |
|- ( # ` (/) ) = 0 |
43 |
42
|
oveq2i |
|- ( -u 1 ^ ( # ` (/) ) ) = ( -u 1 ^ 0 ) |
44 |
|
neg1cn |
|- -u 1 e. CC |
45 |
|
exp0 |
|- ( -u 1 e. CC -> ( -u 1 ^ 0 ) = 1 ) |
46 |
44 45
|
ax-mp |
|- ( -u 1 ^ 0 ) = 1 |
47 |
43 46
|
eqtri |
|- ( -u 1 ^ ( # ` (/) ) ) = 1 |
48 |
47
|
a1i |
|- ( ( A e. V /\ X e. B ) -> ( -u 1 ^ ( # ` (/) ) ) = 1 ) |
49 |
30 41 48
|
3eqtrd |
|- ( ( A e. V /\ X e. B ) -> ( N ` X ) = 1 ) |