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 ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℂ ( ( abs ‘ 𝑥 ) = 1 ∧ ( abs ‘ 𝐴 ) = ( 𝑥 · 𝐴 ) ) )

Proof

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