Theorem psgnid 30423

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

Hypothesis

Ref	Expression
psgnid.s	⊢ 𝑆 = (pmSgn‘𝐷)

Assertion

Ref	Expression
psgnid	⊢ (𝐷 ∈ Fin → (𝑆‘( I ↾ 𝐷)) = 1)

Proof of Theorem psgnid

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

Syntax hints:   → wi 4   = wceq 1525   ∈ wcel 2083   ⊆ wss 3865  {cpr 4480   I cid 5354   ↾ cres 5452  ‘cfv 6232  (class class class)co 7023  Fincfn 8364  ℂcc 10388  1c1 10391  -cneg 10724   ↾_s cress 16317  0_gc0g 16546  Mndcmnd 17737   GrpHom cghm 18100  SymGrpcsymg 18240  pmSgncpsgn 18352  mulGrpcmgp 18933  Ringcrg 18991  ℂ_fldccnfld 20231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-cnex 10446  ax-resscn 10447  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-mulcom 10454  ax-addass 10455  ax-mulass 10456  ax-distr 10457  ax-i2m1 10458  ax-1ne0 10459  ax-1rid 10460  ax-rnegex 10461  ax-rrecex 10462  ax-cnre 10463  ax-pre-lttri 10464  ax-pre-lttrn 10465  ax-pre-ltadd 10466  ax-pre-mulgt0 10467  ax-addf 10469  ax-mulf 10470

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-xor 1497  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-ot 4487  df-uni 4752  df-int 4789  df-iun 4833  df-iin 4834  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-se 5410  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-isom 6241  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-om 7444  df-1st 7552  df-2nd 7553  df-tpos 7750  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-1o 7960  df-2o 7961  df-oadd 7964  df-er 8146  df-map 8265  df-en 8365  df-dom 8366  df-sdom 8367  df-fin 8368  df-card 9221  df-pnf 10530  df-mnf 10531  df-xr 10532  df-ltxr 10533  df-le 10534  df-sub 10725  df-neg 10726  df-div 11152  df-nn 11493  df-2 11554  df-3 11555  df-4 11556  df-5 11557  df-6 11558  df-7 11559  df-8 11560  df-9 11561  df-n0 11752  df-xnn0 11822  df-z 11836  df-dec 11953  df-uz 12098  df-rp 12244  df-fz 12747  df-fzo 12888  df-seq 13224  df-exp 13284  df-hash 13545  df-word 13712  df-lsw 13765  df-concat 13773  df-s1 13798  df-substr 13843  df-pfx 13873  df-splice 13952  df-reverse 13961  df-s2 14050  df-struct 16318  df-ndx 16319  df-slot 16320  df-base 16322  df-sets 16323  df-ress 16324  df-plusg 16411  df-mulr 16412  df-starv 16413  df-tset 16417  df-ple 16418  df-ds 16420  df-unif 16421  df-0g 16548  df-gsum 16549  df-mre 16690  df-mrc 16691  df-acs 16693  df-mgm 17685  df-sgrp 17727  df-mnd 17738  df-mhm 17778  df-submnd 17779  df-grp 17868  df-minusg 17869  df-subg 18034  df-ghm 18101  df-gim 18144  df-oppg 18219  df-symg 18241  df-pmtr 18305  df-psgn 18354  df-cmn 18639  df-abl 18640  df-mgp 18934  df-ur 18946  df-ring 18993  df-cring 18994  df-oppr 19067  df-dvdsr 19085  df-unit 19086  df-invr 19116  df-dvr 19127  df-drng 19198  df-cnfld 20232

This theorem is referenced by:  evpmid  30424  psgnfzto1st  30665