Theorem cnmsgngrp

Description: The group of signs under multiplication. (Contributed by Stefan O'Rear, 28-Aug-2015)

	Ref	Expression
Hypothesis	cnmsgngrp.u	⊢ 𝑈 = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
Assertion	cnmsgngrp	⊢ 𝑈 ∈ Grp

Proof

Step	Hyp	Ref	Expression
1		cnmsgngrp.u	⊢ 𝑈 = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
2		eqid	⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
3	2	cnmsgnsubg	⊢ { 1 , - 1 } ∈ ( SubGrp ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) )
4		cnex	⊢ ℂ ∈ V
5	4	difexi	⊢ ( ℂ ∖ { 0 } ) ∈ V
6		ax-1cn	⊢ 1 ∈ ℂ
7		ax-1ne0	⊢ 1 ≠ 0
8		eldifsn	⊢ ( 1 ∈ ( ℂ ∖ { 0 } ) ↔ ( 1 ∈ ℂ ∧ 1 ≠ 0 ) )
9	6 7 8	mpbir2an	⊢ 1 ∈ ( ℂ ∖ { 0 } )
10		neg1cn	⊢ - 1 ∈ ℂ
11		neg1ne0	⊢ - 1 ≠ 0
12		eldifsn	⊢ ( - 1 ∈ ( ℂ ∖ { 0 } ) ↔ ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) )
13	10 11 12	mpbir2an	⊢ - 1 ∈ ( ℂ ∖ { 0 } )
14		prssi	⊢ ( ( 1 ∈ ( ℂ ∖ { 0 } ) ∧ - 1 ∈ ( ℂ ∖ { 0 } ) ) → { 1 , - 1 } ⊆ ( ℂ ∖ { 0 } ) )
15	9 13 14	mp2an	⊢ { 1 , - 1 } ⊆ ( ℂ ∖ { 0 } )
16		ressabs	⊢ ( ( ( ℂ ∖ { 0 } ) ∈ V ∧ { 1 , - 1 } ⊆ ( ℂ ∖ { 0 } ) ) → ( ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ↾s { 1 , - 1 } ) = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) )
17	5 15 16	mp2an	⊢ ( ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ↾s { 1 , - 1 } ) = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
18	1 17	eqtr4i	⊢ 𝑈 = ( ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ↾s { 1 , - 1 } )
19	18	subggrp	⊢ ( { 1 , - 1 } ∈ ( SubGrp ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) → 𝑈 ∈ Grp )
20	3 19	ax-mp	⊢ 𝑈 ∈ Grp