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 ) ) )