Metamath Proof Explorer

Theorem abs1m

Description: For any complex number, there exists a unit-magnitude multiplier that produces its absolute value. Part of proof of Theorem 13-2.12 of Gleason p. 195. (Contributed by NM, 26-Mar-2005)

Ref Expression
Assertion abs1m 
|- ( A e. CC -> E. x e. CC ( ( abs ` x ) = 1 /\ ( abs ` A ) = ( x x. A ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( A = 0 -> ( abs ` A ) = ( abs ` 0 ) )
2 abs0 
 |-  ( abs ` 0 ) = 0
3 1 2 eqtrdi 
 |-  ( A = 0 -> ( abs ` A ) = 0 )
4 oveq2 
 |-  ( A = 0 -> ( x x. A ) = ( x x. 0 ) )
5 3 4 eqeq12d 
 |-  ( A = 0 -> ( ( abs ` A ) = ( x x. A ) <-> 0 = ( x x. 0 ) ) )
6 5 anbi2d 
 |-  ( A = 0 -> ( ( ( abs ` x ) = 1 /\ ( abs ` A ) = ( x x. A ) ) <-> ( ( abs ` x ) = 1 /\ 0 = ( x x. 0 ) ) ) )
7 6 rexbidv 
 |-  ( A = 0 -> ( E. x e. CC ( ( abs ` x ) = 1 /\ ( abs ` A ) = ( x x. A ) ) <-> E. x e. CC ( ( abs ` x ) = 1 /\ 0 = ( x x. 0 ) ) ) )
8 simpl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> A e. CC )
9 8 cjcld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( * ` A ) e. CC )
10 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
11 10 adantr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. RR )
12 11 recnd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. CC )
13 abs00 
 |-  ( A e. CC -> ( ( abs ` A ) = 0 <-> A = 0 ) )
14 13 necon3bid 
 |-  ( A e. CC -> ( ( abs ` A ) =/= 0 <-> A =/= 0 ) )
15 14 biimpar 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) =/= 0 )
16 9 12 15 divcld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( * ` A ) / ( abs ` A ) ) e. CC )
17 absdiv 
 |-  ( ( ( * ` A ) e. CC /\ ( abs ` A ) e. CC /\ ( abs ` A ) =/= 0 ) -> ( abs ` ( ( * ` A ) / ( abs ` A ) ) ) = ( ( abs ` ( * ` A ) ) / ( abs ` ( abs ` A ) ) ) )
18 9 12 15 17 syl3anc 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( ( * ` A ) / ( abs ` A ) ) ) = ( ( abs ` ( * ` A ) ) / ( abs ` ( abs ` A ) ) ) )
19 abscj 
 |-  ( A e. CC -> ( abs ` ( * ` A ) ) = ( abs ` A ) )
20 19 adantr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( * ` A ) ) = ( abs ` A ) )
21 absidm 
 |-  ( A e. CC -> ( abs ` ( abs ` A ) ) = ( abs ` A ) )
22 21 adantr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( abs ` A ) ) = ( abs ` A ) )
23 20 22 oveq12d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( abs ` ( * ` A ) ) / ( abs ` ( abs ` A ) ) ) = ( ( abs ` A ) / ( abs ` A ) ) )
24 12 15 dividd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( abs ` A ) / ( abs ` A ) ) = 1 )
25 18 23 24 3eqtrd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( ( * ` A ) / ( abs ` A ) ) ) = 1 )
26 8 9 12 15 divassd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( A x. ( * ` A ) ) / ( abs ` A ) ) = ( A x. ( ( * ` A ) / ( abs ` A ) ) ) )
27 12 sqvald 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( abs ` A ) ^ 2 ) = ( ( abs ` A ) x. ( abs ` A ) ) )
28 absvalsq 
 |-  ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
29 28 adantr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
30 27 29 eqtr3d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( abs ` A ) x. ( abs ` A ) ) = ( A x. ( * ` A ) ) )
31 12 12 15 30 mvllmuld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) = ( ( A x. ( * ` A ) ) / ( abs ` A ) ) )
32 16 8 mulcomd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( ( * ` A ) / ( abs ` A ) ) x. A ) = ( A x. ( ( * ` A ) / ( abs ` A ) ) ) )
33 26 31 32 3eqtr4d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) = ( ( ( * ` A ) / ( abs ` A ) ) x. A ) )
34 fveqeq2 
 |-  ( x = ( ( * ` A ) / ( abs ` A ) ) -> ( ( abs ` x ) = 1 <-> ( abs ` ( ( * ` A ) / ( abs ` A ) ) ) = 1 ) )
35 oveq1 
 |-  ( x = ( ( * ` A ) / ( abs ` A ) ) -> ( x x. A ) = ( ( ( * ` A ) / ( abs ` A ) ) x. A ) )
36 35 eqeq2d 
 |-  ( x = ( ( * ` A ) / ( abs ` A ) ) -> ( ( abs ` A ) = ( x x. A ) <-> ( abs ` A ) = ( ( ( * ` A ) / ( abs ` A ) ) x. A ) ) )
37 34 36 anbi12d 
 |-  ( x = ( ( * ` A ) / ( abs ` A ) ) -> ( ( ( abs ` x ) = 1 /\ ( abs ` A ) = ( x x. A ) ) <-> ( ( abs ` ( ( * ` A ) / ( abs ` A ) ) ) = 1 /\ ( abs ` A ) = ( ( ( * ` A ) / ( abs ` A ) ) x. A ) ) ) )
38 37 rspcev 
 |-  ( ( ( ( * ` A ) / ( abs ` A ) ) e. CC /\ ( ( abs ` ( ( * ` A ) / ( abs ` A ) ) ) = 1 /\ ( abs ` A ) = ( ( ( * ` A ) / ( abs ` A ) ) x. A ) ) ) -> E. x e. CC ( ( abs ` x ) = 1 /\ ( abs ` A ) = ( x x. A ) ) )
39 16 25 33 38 syl12anc 
 |-  ( ( A e. CC /\ A =/= 0 ) -> E. x e. CC ( ( abs ` x ) = 1 /\ ( abs ` A ) = ( x x. A ) ) )
40 ax-icn 
 |-  _i e. CC
41 absi 
 |-  ( abs ` _i ) = 1
42 it0e0 
 |-  ( _i x. 0 ) = 0
43 42 eqcomi 
 |-  0 = ( _i x. 0 )
44 41 43 pm3.2i 
 |-  ( ( abs ` _i ) = 1 /\ 0 = ( _i x. 0 ) )
45 fveqeq2 
 |-  ( x = _i -> ( ( abs ` x ) = 1 <-> ( abs ` _i ) = 1 ) )
46 oveq1 
 |-  ( x = _i -> ( x x. 0 ) = ( _i x. 0 ) )
47 46 eqeq2d 
 |-  ( x = _i -> ( 0 = ( x x. 0 ) <-> 0 = ( _i x. 0 ) ) )
48 45 47 anbi12d 
 |-  ( x = _i -> ( ( ( abs ` x ) = 1 /\ 0 = ( x x. 0 ) ) <-> ( ( abs ` _i ) = 1 /\ 0 = ( _i x. 0 ) ) ) )
49 48 rspcev 
 |-  ( ( _i e. CC /\ ( ( abs ` _i ) = 1 /\ 0 = ( _i x. 0 ) ) ) -> E. x e. CC ( ( abs ` x ) = 1 /\ 0 = ( x x. 0 ) ) )
50 40 44 49 mp2an 
 |-  E. x e. CC ( ( abs ` x ) = 1 /\ 0 = ( x x. 0 ) )
51 50 a1i 
 |-  ( A e. CC -> E. x e. CC ( ( abs ` x ) = 1 /\ 0 = ( x x. 0 ) ) )
52 7 39 51 pm2.61ne 
 |-  ( A e. CC -> E. x e. CC ( ( abs ` x ) = 1 /\ ( abs ` A ) = ( x x. A ) ) )