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 \in B \to N (X) = (ι s \| \exists w \in Word T (X = \sum_{G} w \land s = {(- 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 \in B \to X \in B$
7		elpri	$⊢ X \in \{\{⟨1, 1⟩, ⟨2, 2⟩\}, \{⟨1, 2⟩, ⟨2, 1⟩\}\} \to (X = \{⟨1, 1⟩, ⟨2, 2⟩\} \lor X = \{⟨1, 2⟩, ⟨2, 1⟩\})$
8		prfi	$⊢ \{⟨1, 1⟩, ⟨2, 2⟩\} \in Fin$
9		eleq1	$⊢ X = \{⟨1, 1⟩, ⟨2, 2⟩\} \to (X \in Fin \leftrightarrow \{⟨1, 1⟩, ⟨2, 2⟩\} \in Fin)$
10	8 9	mpbiri	$⊢ X = \{⟨1, 1⟩, ⟨2, 2⟩\} \to X \in Fin$
11		prfi	$⊢ \{⟨1, 2⟩, ⟨2, 1⟩\} \in Fin$
12		eleq1	$⊢ X = \{⟨1, 2⟩, ⟨2, 1⟩\} \to (X \in Fin \leftrightarrow \{⟨1, 2⟩, ⟨2, 1⟩\} \in Fin)$
13	11 12	mpbiri	$⊢ X = \{⟨1, 2⟩, ⟨2, 1⟩\} \to X \in Fin$
14	10 13	jaoi	$⊢ (X = \{⟨1, 1⟩, ⟨2, 2⟩\} \lor X = \{⟨1, 2⟩, ⟨2, 1⟩\}) \to X \in Fin$
15		diffi	$⊢ X \in Fin \to X ∖ I \in Fin$
16	14 15	syl	$⊢ (X = \{⟨1, 1⟩, ⟨2, 2⟩\} \lor X = \{⟨1, 2⟩, ⟨2, 1⟩\}) \to X ∖ I \in Fin$
17		dmfi	$⊢ X ∖ I \in Fin \to dom (X ∖ I) \in Fin$
18	7 16 17	3syl	$⊢ X \in \{\{⟨1, 1⟩, ⟨2, 2⟩\}, \{⟨1, 2⟩, ⟨2, 1⟩\}\} \to dom (X ∖ I) \in Fin$
19		1ex	$⊢ 1 \in V$
20		2nn	$⊢ 2 \in ℕ$
21	2 3 1	symg2bas	$⊢ (1 \in V \land 2 \in ℕ) \to B = \{\{⟨1, 1⟩, ⟨2, 2⟩\}, \{⟨1, 2⟩, ⟨2, 1⟩\}\}$
22	19 20 21	mp2an	$⊢ B = \{\{⟨1, 1⟩, ⟨2, 2⟩\}, \{⟨1, 2⟩, ⟨2, 1⟩\}\}$
23	18 22	eleq2s	$⊢ X \in B \to dom (X ∖ I) \in Fin$
24	2 5 3	psgneldm	$⊢ X \in dom N \leftrightarrow (X \in B \land dom (X ∖ I) \in Fin)$
25	6 23 24	sylanbrc	$⊢ X \in B \to X \in dom N$
26	2 4 5	psgnval	$⊢ X \in dom N \to N (X) = (ι s \| \exists w \in Word T (X = \sum_{G} w \land s = {(- 1)}^{\|w\|}))$
27	25 26	syl	$⊢ X \in B \to N (X) = (ι s \| \exists w \in Word T (X = \sum_{G} w \land s = {(- 1)}^{\|w\|}))$
28	6 27	syl	$⊢ X \in B \to N (X) = (ι s \| \exists w \in Word T (X = \sum_{G} w \land s = {(- 1)}^{\|w\|}))$

Metamath Proof Explorer

Theorem psgnprfval

Proof