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 
|- U = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
Assertion cnmsgngrp 
|- U e. Grp

Proof

Step Hyp Ref Expression
1 cnmsgngrp.u 
 |-  U = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
2 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
3 2 cnmsgnsubg 
 |-  { 1 , -u 1 } e. ( SubGrp ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) )
4 cnex 
 |-  CC e. _V
5 4 difexi 
 |-  ( CC \ { 0 } ) e. _V
6 ax-1cn 
 |-  1 e. CC
7 ax-1ne0 
 |-  1 =/= 0
8 eldifsn 
 |-  ( 1 e. ( CC \ { 0 } ) <-> ( 1 e. CC /\ 1 =/= 0 ) )
9 6 7 8 mpbir2an 
 |-  1 e. ( CC \ { 0 } )
10 neg1cn 
 |-  -u 1 e. CC
11 neg1ne0 
 |-  -u 1 =/= 0
12 eldifsn 
 |-  ( -u 1 e. ( CC \ { 0 } ) <-> ( -u 1 e. CC /\ -u 1 =/= 0 ) )
13 10 11 12 mpbir2an 
 |-  -u 1 e. ( CC \ { 0 } )
14 prssi 
 |-  ( ( 1 e. ( CC \ { 0 } ) /\ -u 1 e. ( CC \ { 0 } ) ) -> { 1 , -u 1 } C_ ( CC \ { 0 } ) )
15 9 13 14 mp2an 
 |-  { 1 , -u 1 } C_ ( CC \ { 0 } )
16 ressabs 
 |-  ( ( ( CC \ { 0 } ) e. _V /\ { 1 , -u 1 } C_ ( CC \ { 0 } ) ) -> ( ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) )
17 5 15 16 mp2an 
 |-  ( ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
18 1 17 eqtr4i 
 |-  U = ( ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) |`s { 1 , -u 1 } )
19 18 subggrp 
 |-  ( { 1 , -u 1 } e. ( SubGrp ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) -> U e. Grp )
20 3 19 ax-mp 
 |-  U e. Grp