This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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