Metamath Proof Explorer

Theorem cnmsgnsubg

Description: The signs form a multiplicative subgroup of the complex numbers. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Hypothesis cnmsgnsubg.m 
|- M = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
Assertion cnmsgnsubg 
|- { 1 , -u 1 } e. ( SubGrp ` M )

Proof

Step Hyp Ref Expression
1 cnmsgnsubg.m 
 |-  M = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
2 elpri 
 |-  ( x e. { 1 , -u 1 } -> ( x = 1 \/ x = -u 1 ) )
3 id 
 |-  ( x = 1 -> x = 1 )
4 ax-1cn 
 |-  1 e. CC
5 3 4 eqeltrdi 
 |-  ( x = 1 -> x e. CC )
6 id 
 |-  ( x = -u 1 -> x = -u 1 )
7 neg1cn 
 |-  -u 1 e. CC
8 6 7 eqeltrdi 
 |-  ( x = -u 1 -> x e. CC )
9 5 8 jaoi 
 |-  ( ( x = 1 \/ x = -u 1 ) -> x e. CC )
10 2 9 syl 
 |-  ( x e. { 1 , -u 1 } -> x e. CC )
11 ax-1ne0 
 |-  1 =/= 0
12 11 a1i 
 |-  ( x = 1 -> 1 =/= 0 )
13 3 12 eqnetrd 
 |-  ( x = 1 -> x =/= 0 )
14 neg1ne0 
 |-  -u 1 =/= 0
15 14 a1i 
 |-  ( x = -u 1 -> -u 1 =/= 0 )
16 6 15 eqnetrd 
 |-  ( x = -u 1 -> x =/= 0 )
17 13 16 jaoi 
 |-  ( ( x = 1 \/ x = -u 1 ) -> x =/= 0 )
18 2 17 syl 
 |-  ( x e. { 1 , -u 1 } -> x =/= 0 )
19 elpri 
 |-  ( y e. { 1 , -u 1 } -> ( y = 1 \/ y = -u 1 ) )
20 oveq12 
 |-  ( ( x = 1 /\ y = 1 ) -> ( x x. y ) = ( 1 x. 1 ) )
21 4 mulid1i 
 |-  ( 1 x. 1 ) = 1
22 1ex 
 |-  1 e. _V
23 22 prid1 
 |-  1 e. { 1 , -u 1 }
24 21 23 eqeltri 
 |-  ( 1 x. 1 ) e. { 1 , -u 1 }
25 20 24 eqeltrdi 
 |-  ( ( x = 1 /\ y = 1 ) -> ( x x. y ) e. { 1 , -u 1 } )
26 oveq12 
 |-  ( ( x = -u 1 /\ y = 1 ) -> ( x x. y ) = ( -u 1 x. 1 ) )
27 7 mulid1i 
 |-  ( -u 1 x. 1 ) = -u 1
28 negex 
 |-  -u 1 e. _V
29 28 prid2 
 |-  -u 1 e. { 1 , -u 1 }
30 27 29 eqeltri 
 |-  ( -u 1 x. 1 ) e. { 1 , -u 1 }
31 26 30 eqeltrdi 
 |-  ( ( x = -u 1 /\ y = 1 ) -> ( x x. y ) e. { 1 , -u 1 } )
32 oveq12 
 |-  ( ( x = 1 /\ y = -u 1 ) -> ( x x. y ) = ( 1 x. -u 1 ) )
33 7 mulid2i 
 |-  ( 1 x. -u 1 ) = -u 1
34 33 29 eqeltri 
 |-  ( 1 x. -u 1 ) e. { 1 , -u 1 }
35 32 34 eqeltrdi 
 |-  ( ( x = 1 /\ y = -u 1 ) -> ( x x. y ) e. { 1 , -u 1 } )
36 oveq12 
 |-  ( ( x = -u 1 /\ y = -u 1 ) -> ( x x. y ) = ( -u 1 x. -u 1 ) )
37 neg1mulneg1e1 
 |-  ( -u 1 x. -u 1 ) = 1
38 37 23 eqeltri 
 |-  ( -u 1 x. -u 1 ) e. { 1 , -u 1 }
39 36 38 eqeltrdi 
 |-  ( ( x = -u 1 /\ y = -u 1 ) -> ( x x. y ) e. { 1 , -u 1 } )
40 25 31 35 39 ccase 
 |-  ( ( ( x = 1 \/ x = -u 1 ) /\ ( y = 1 \/ y = -u 1 ) ) -> ( x x. y ) e. { 1 , -u 1 } )
41 2 19 40 syl2an 
 |-  ( ( x e. { 1 , -u 1 } /\ y e. { 1 , -u 1 } ) -> ( x x. y ) e. { 1 , -u 1 } )
42 oveq2 
 |-  ( x = 1 -> ( 1 / x ) = ( 1 / 1 ) )
43 1div1e1 
 |-  ( 1 / 1 ) = 1
44 43 23 eqeltri 
 |-  ( 1 / 1 ) e. { 1 , -u 1 }
45 42 44 eqeltrdi 
 |-  ( x = 1 -> ( 1 / x ) e. { 1 , -u 1 } )
46 oveq2 
 |-  ( x = -u 1 -> ( 1 / x ) = ( 1 / -u 1 ) )
47 divneg2 
 |-  ( ( 1 e. CC /\ 1 e. CC /\ 1 =/= 0 ) -> -u ( 1 / 1 ) = ( 1 / -u 1 ) )
48 4 4 11 47 mp3an 
 |-  -u ( 1 / 1 ) = ( 1 / -u 1 )
49 43 negeqi 
 |-  -u ( 1 / 1 ) = -u 1
50 48 49 eqtr3i 
 |-  ( 1 / -u 1 ) = -u 1
51 50 29 eqeltri 
 |-  ( 1 / -u 1 ) e. { 1 , -u 1 }
52 46 51 eqeltrdi 
 |-  ( x = -u 1 -> ( 1 / x ) e. { 1 , -u 1 } )
53 45 52 jaoi 
 |-  ( ( x = 1 \/ x = -u 1 ) -> ( 1 / x ) e. { 1 , -u 1 } )
54 2 53 syl 
 |-  ( x e. { 1 , -u 1 } -> ( 1 / x ) e. { 1 , -u 1 } )
55 1 10 18 41 23 54 cnmsubglem 
 |-  { 1 , -u 1 } e. ( SubGrp ` M )