Metamath Proof Explorer

Theorem psgnvalii

Description: Any representation of a permutation is length matching the permutation sign. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Hypotheses psgnval.g 
|- G = ( SymGrp ` D )
psgnval.t 
|- T = ran ( pmTrsp ` D )
psgnval.n 
|- N = ( pmSgn ` D )
Assertion psgnvalii 
|- ( ( D e. V /\ W e. Word T ) -> ( N ` ( G gsum W ) ) = ( -u 1 ^ ( # ` W ) ) )

Proof

Step Hyp Ref Expression
1 psgnval.g 
 |-  G = ( SymGrp ` D )
2 psgnval.t 
 |-  T = ran ( pmTrsp ` D )
3 psgnval.n 
 |-  N = ( pmSgn ` D )
4 1 2 3 psgneldm2i 
 |-  ( ( D e. V /\ W e. Word T ) -> ( G gsum W ) e. dom N )
5 1 2 3 psgnval 
 |-  ( ( G gsum W ) e. dom N -> ( N ` ( G gsum W ) ) = ( iota s E. w e. Word T ( ( G gsum W ) = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
6 4 5 syl 
 |-  ( ( D e. V /\ W e. Word T ) -> ( N ` ( G gsum W ) ) = ( iota s E. w e. Word T ( ( G gsum W ) = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
7 simpr 
 |-  ( ( D e. V /\ W e. Word T ) -> W e. Word T )
8 eqidd 
 |-  ( ( D e. V /\ W e. Word T ) -> ( G gsum W ) = ( G gsum W ) )
9 eqidd 
 |-  ( ( D e. V /\ W e. Word T ) -> ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` W ) ) )
10 oveq2 
 |-  ( w = W -> ( G gsum w ) = ( G gsum W ) )
11 10 eqeq2d 
 |-  ( w = W -> ( ( G gsum W ) = ( G gsum w ) <-> ( G gsum W ) = ( G gsum W ) ) )
12 fveq2 
 |-  ( w = W -> ( # ` w ) = ( # ` W ) )
13 12 oveq2d 
 |-  ( w = W -> ( -u 1 ^ ( # ` w ) ) = ( -u 1 ^ ( # ` W ) ) )
14 13 eqeq2d 
 |-  ( w = W -> ( ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` w ) ) <-> ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` W ) ) ) )
15 11 14 anbi12d 
 |-  ( w = W -> ( ( ( G gsum W ) = ( G gsum w ) /\ ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` w ) ) ) <-> ( ( G gsum W ) = ( G gsum W ) /\ ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` W ) ) ) ) )
16 15 rspcev 
 |-  ( ( W e. Word T /\ ( ( G gsum W ) = ( G gsum W ) /\ ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` W ) ) ) ) -> E. w e. Word T ( ( G gsum W ) = ( G gsum w ) /\ ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` w ) ) ) )
17 7 8 9 16 syl12anc 
 |-  ( ( D e. V /\ W e. Word T ) -> E. w e. Word T ( ( G gsum W ) = ( G gsum w ) /\ ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` w ) ) ) )
18 ovexd 
 |-  ( ( D e. V /\ W e. Word T ) -> ( -u 1 ^ ( # ` W ) ) e. _V )
19 1 2 3 psgneu 
 |-  ( ( G gsum W ) e. dom N -> E! s E. w e. Word T ( ( G gsum W ) = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) )
20 4 19 syl 
 |-  ( ( D e. V /\ W e. Word T ) -> E! s E. w e. Word T ( ( G gsum W ) = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) )
21 eqeq1 
 |-  ( s = ( -u 1 ^ ( # ` W ) ) -> ( s = ( -u 1 ^ ( # ` w ) ) <-> ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` w ) ) ) )
22 21 anbi2d 
 |-  ( s = ( -u 1 ^ ( # ` W ) ) -> ( ( ( G gsum W ) = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) <-> ( ( G gsum W ) = ( G gsum w ) /\ ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` w ) ) ) ) )
23 22 rexbidv 
 |-  ( s = ( -u 1 ^ ( # ` W ) ) -> ( E. w e. Word T ( ( G gsum W ) = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) <-> E. w e. Word T ( ( G gsum W ) = ( G gsum w ) /\ ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` w ) ) ) ) )
24 23 adantl 
 |-  ( ( ( D e. V /\ W e. Word T ) /\ s = ( -u 1 ^ ( # ` W ) ) ) -> ( E. w e. Word T ( ( G gsum W ) = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) <-> E. w e. Word T ( ( G gsum W ) = ( G gsum w ) /\ ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` w ) ) ) ) )
25 18 20 24 iota2d 
 |-  ( ( D e. V /\ W e. Word T ) -> ( E. w e. Word T ( ( G gsum W ) = ( G gsum w ) /\ ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` w ) ) ) <-> ( iota s E. w e. Word T ( ( G gsum W ) = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) = ( -u 1 ^ ( # ` W ) ) ) )
26 17 25 mpbid 
 |-  ( ( D e. V /\ W e. Word T ) -> ( iota s E. w e. Word T ( ( G gsum W ) = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) = ( -u 1 ^ ( # ` W ) ) )
27 6 26 eqtrd 
 |-  ( ( D e. V /\ W e. Word T ) -> ( N ` ( G gsum W ) ) = ( -u 1 ^ ( # ` W ) ) )