Theorem cnmsgn0g

Description: The neutral element of the sign subgroup of the complex numbers. (Contributed by Thierry Arnoux, 1-Nov-2023)

	Ref	Expression
Hypothesis	cnmsgn0g.1	⊢ 𝑈 = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
Assertion	cnmsgn0g	⊢ 1 = ( 0g ‘ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		cnmsgn0g.1	⊢ 𝑈 = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
2		cnring	⊢ ℂfld ∈ Ring
3		eqid	⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
4	3	ringmgp	⊢ ( ℂfld ∈ Ring → ( mulGrp ‘ ℂfld ) ∈ Mnd )
5	2 4	ax-mp	⊢ ( mulGrp ‘ ℂfld ) ∈ Mnd
6		1ex	⊢ 1 ∈ V
7	6	prid1	⊢ 1 ∈ { 1 , - 1 }
8		ax-1cn	⊢ 1 ∈ ℂ
9		neg1cn	⊢ - 1 ∈ ℂ
10		prssi	⊢ ( ( 1 ∈ ℂ ∧ - 1 ∈ ℂ ) → { 1 , - 1 } ⊆ ℂ )
11	8 9 10	mp2an	⊢ { 1 , - 1 } ⊆ ℂ
12		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
13	3 12	mgpbas	⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
14		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
15	3 14	ringidval	⊢ 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
16	1 13 15	ress0g	⊢ ( ( ( mulGrp ‘ ℂfld ) ∈ Mnd ∧ 1 ∈ { 1 , - 1 } ∧ { 1 , - 1 } ⊆ ℂ ) → 1 = ( 0g ‘ 𝑈 ) )
17	5 7 11 16	mp3an	⊢ 1 = ( 0g ‘ 𝑈 )