Theorem psgnid

Description: Permutation sign of the identity. (Contributed by Thierry Arnoux, 21-Aug-2020)

	Ref	Expression
Hypothesis	psgnid.s	⊢ 𝑆 = ( pmSgn ‘ 𝐷 )
Assertion	psgnid	⊢ ( 𝐷 ∈ Fin → ( 𝑆 ‘ ( I ↾ 𝐷 ) ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		psgnid.s	⊢ 𝑆 = ( pmSgn ‘ 𝐷 )
2		eqid	⊢ ( SymGrp ‘ 𝐷 ) = ( SymGrp ‘ 𝐷 )
3	2	symgid	⊢ ( 𝐷 ∈ Fin → ( I ↾ 𝐷 ) = ( 0g ‘ ( SymGrp ‘ 𝐷 ) ) )
4	3	fveq2d	⊢ ( 𝐷 ∈ Fin → ( 𝑆 ‘ ( I ↾ 𝐷 ) ) = ( 𝑆 ‘ ( 0g ‘ ( SymGrp ‘ 𝐷 ) ) ) )
5		eqid	⊢ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
6	2 1 5	psgnghm2	⊢ ( 𝐷 ∈ Fin → 𝑆 ∈ ( ( SymGrp ‘ 𝐷 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
7		eqid	⊢ ( 0g ‘ ( SymGrp ‘ 𝐷 ) ) = ( 0g ‘ ( SymGrp ‘ 𝐷 ) )
8		cnring	⊢ ℂfld ∈ Ring
9		eqid	⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
10	9	ringmgp	⊢ ( ℂfld ∈ Ring → ( mulGrp ‘ ℂfld ) ∈ Mnd )
11	8 10	ax-mp	⊢ ( mulGrp ‘ ℂfld ) ∈ Mnd
12		1ex	⊢ 1 ∈ V
13	12	prid1	⊢ 1 ∈ { 1 , - 1 }
14		ax-1cn	⊢ 1 ∈ ℂ
15		neg1cn	⊢ - 1 ∈ ℂ
16		prssi	⊢ ( ( 1 ∈ ℂ ∧ - 1 ∈ ℂ ) → { 1 , - 1 } ⊆ ℂ )
17	14 15 16	mp2an	⊢ { 1 , - 1 } ⊆ ℂ
18		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
19	9 18	mgpbas	⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
20		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
21	9 20	ringidval	⊢ 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
22	5 19 21	ress0g	⊢ ( ( ( mulGrp ‘ ℂfld ) ∈ Mnd ∧ 1 ∈ { 1 , - 1 } ∧ { 1 , - 1 } ⊆ ℂ ) → 1 = ( 0g ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
23	11 13 17 22	mp3an	⊢ 1 = ( 0g ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) )
24	7 23	ghmid	⊢ ( 𝑆 ∈ ( ( SymGrp ‘ 𝐷 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) → ( 𝑆 ‘ ( 0g ‘ ( SymGrp ‘ 𝐷 ) ) ) = 1 )
25	6 24	syl	⊢ ( 𝐷 ∈ Fin → ( 𝑆 ‘ ( 0g ‘ ( SymGrp ‘ 𝐷 ) ) ) = 1 )
26	4 25	eqtrd	⊢ ( 𝐷 ∈ Fin → ( 𝑆 ‘ ( I ↾ 𝐷 ) ) = 1 )