psgnprfval

Description: The permutation sign function for a pair. (Contributed by AV, 10-Dec-2018)

	Ref	Expression
Hypotheses	psgnprfval.0	\|- D = { 1 , 2 }
	psgnprfval.g	\|- G = ( SymGrp ` D )
	psgnprfval.b	\|- B = ( Base ` G )
	psgnprfval.t	\|- T = ran ( pmTrsp ` D )
	psgnprfval.n	\|- N = ( pmSgn ` D )
Assertion	psgnprfval	\|- ( X e. B -> ( N ` X ) = ( iota s E. w e. Word T ( X = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		psgnprfval.0	\|- D = { 1 , 2 }
2		psgnprfval.g	\|- G = ( SymGrp ` D )
3		psgnprfval.b	\|- B = ( Base ` G )
4		psgnprfval.t	\|- T = ran ( pmTrsp ` D )
5		psgnprfval.n	\|- N = ( pmSgn ` D )
6		id	\|- ( X e. B -> X e. B )
7		elpri	\|- ( X e. { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } } -> ( X = { <. 1 , 1 >. , <. 2 , 2 >. } \/ X = { <. 1 , 2 >. , <. 2 , 1 >. } ) )
8		prfi	\|- { <. 1 , 1 >. , <. 2 , 2 >. } e. Fin
9		eleq1	\|- ( X = { <. 1 , 1 >. , <. 2 , 2 >. } -> ( X e. Fin <-> { <. 1 , 1 >. , <. 2 , 2 >. } e. Fin ) )
10	8 9	mpbiri	\|- ( X = { <. 1 , 1 >. , <. 2 , 2 >. } -> X e. Fin )
11		prfi	\|- { <. 1 , 2 >. , <. 2 , 1 >. } e. Fin
12		eleq1	\|- ( X = { <. 1 , 2 >. , <. 2 , 1 >. } -> ( X e. Fin <-> { <. 1 , 2 >. , <. 2 , 1 >. } e. Fin ) )
13	11 12	mpbiri	\|- ( X = { <. 1 , 2 >. , <. 2 , 1 >. } -> X e. Fin )
14	10 13	jaoi	\|- ( ( X = { <. 1 , 1 >. , <. 2 , 2 >. } \/ X = { <. 1 , 2 >. , <. 2 , 1 >. } ) -> X e. Fin )
15		diffi	\|- ( X e. Fin -> ( X \ _I ) e. Fin )
16		dmfi	\|- ( ( X \ _I ) e. Fin -> dom ( X \ _I ) e. Fin )
17	7 14 15 16	4syl	\|- ( X e. { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } } -> dom ( X \ _I ) e. Fin )
18		1ex	\|- 1 e. _V
19		2nn	\|- 2 e. NN
20	2 3 1	symg2bas	\|- ( ( 1 e. _V /\ 2 e. NN ) -> B = { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } } )
21	18 19 20	mp2an	\|- B = { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } }
22	17 21	eleq2s	\|- ( X e. B -> dom ( X \ _I ) e. Fin )
23	2 5 3	psgneldm	\|- ( X e. dom N <-> ( X e. B /\ dom ( X \ _I ) e. Fin ) )
24	6 22 23	sylanbrc	\|- ( X e. B -> X e. dom N )
25	2 4 5	psgnval	\|- ( X e. dom N -> ( N ` X ) = ( iota s E. w e. Word T ( X = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
26	24 25	syl	\|- ( X e. B -> ( N ` X ) = ( iota s E. w e. Word T ( X = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
27	6 26	syl	\|- ( X e. B -> ( N ` X ) = ( iota s E. w e. Word T ( X = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )

Metamath Proof Explorer

Theorem psgnprfval

Proof