zrhpsgninv

Description: The embedded sign of a permutation equals the embedded sign of the inverse of the permutation. (Contributed by SO, 9-Jul-2018)

	Ref	Expression
Hypotheses	zrhpsgninv.p	$⊢ P = {Base}_{SymGrp (N)}$
	zrhpsgninv.y	$⊢ Y = ℤRHom (R)$
	zrhpsgninv.s	$⊢ S = pmSgn (N)$
Assertion	zrhpsgninv	$⊢ (R \in Ring \land N \in Fin \land F \in P) \to (Y \circ S) (F^{-1}) = (Y \circ S) (F)$

Proof

Step	Hyp	Ref	Expression
1		zrhpsgninv.p	$⊢ P = {Base}_{SymGrp (N)}$
2		zrhpsgninv.y	$⊢ Y = ℤRHom (R)$
3		zrhpsgninv.s	$⊢ S = pmSgn (N)$
4		eqid	$⊢ SymGrp (N) = SymGrp (N)$
5	4 3 1	psgninv	$⊢ (N \in Fin \land F \in P) \to S (F^{-1}) = S (F)$
6	5	3adant1	$⊢ (R \in Ring \land N \in Fin \land F \in P) \to S (F^{-1}) = S (F)$
7	6	fveq2d	$⊢ (R \in Ring \land N \in Fin \land F \in P) \to Y (S (F^{-1})) = Y (S (F))$
8		eqid	$⊢ {mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\} = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\}$
9	4 3 8	psgnghm2	$⊢ N \in Fin \to S \in (SymGrp (N) GrpHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\}))$
10		eqid	$⊢ {Base}_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})} = {Base}_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})}$
11	1 10	ghmf	$⊢ S \in (SymGrp (N) GrpHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})) \to S : P ⟶ {Base}_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})}$
12	9 11	syl	$⊢ N \in Fin \to S : P ⟶ {Base}_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})}$
13	12	3ad2ant2	$⊢ (R \in Ring \land N \in Fin \land F \in P) \to S : P ⟶ {Base}_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})}$
14		eqid	$⊢ {inv}_{g} (SymGrp (N)) = {inv}_{g} (SymGrp (N))$
15	4 1 14	symginv	$⊢ F \in P \to {inv}_{g} (SymGrp (N)) (F) = F^{-1}$
16	15	3ad2ant3	$⊢ (R \in Ring \land N \in Fin \land F \in P) \to {inv}_{g} (SymGrp (N)) (F) = F^{-1}$
17	4	symggrp	$⊢ N \in Fin \to SymGrp (N) \in Grp$
18	17	3ad2ant2	$⊢ (R \in Ring \land N \in Fin \land F \in P) \to SymGrp (N) \in Grp$
19		simp3	$⊢ (R \in Ring \land N \in Fin \land F \in P) \to F \in P$
20	1 14	grpinvcl	$⊢ (SymGrp (N) \in Grp \land F \in P) \to {inv}_{g} (SymGrp (N)) (F) \in P$
21	18 19 20	syl2anc	$⊢ (R \in Ring \land N \in Fin \land F \in P) \to {inv}_{g} (SymGrp (N)) (F) \in P$
22	16 21	eqeltrrd	$⊢ (R \in Ring \land N \in Fin \land F \in P) \to F^{-1} \in P$
23		fvco3	$⊢ (S : P ⟶ {Base}_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})} \land F^{-1} \in P) \to (Y \circ S) (F^{-1}) = Y (S (F^{-1}))$
24	13 22 23	syl2anc	$⊢ (R \in Ring \land N \in Fin \land F \in P) \to (Y \circ S) (F^{-1}) = Y (S (F^{-1}))$
25		fvco3	$⊢ (S : P ⟶ {Base}_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})} \land F \in P) \to (Y \circ S) (F) = Y (S (F))$
26	13 19 25	syl2anc	$⊢ (R \in Ring \land N \in Fin \land F \in P) \to (Y \circ S) (F) = Y (S (F))$
27	7 24 26	3eqtr4d	$⊢ (R \in Ring \land N \in Fin \land F \in P) \to (Y \circ S) (F^{-1}) = (Y \circ S) (F)$

Metamath Proof Explorer

Theorem zrhpsgninv

Proof