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\in ℂ\to \exists x\in ℂ\left(\left|x\right|=1\wedge \left|A\right|=xA\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢A=0\to \left|A\right|=\left|0\right|$$
2		abs0	$$⊢\left|0\right|=0$$
3	1 2	eqtrdi	$$⊢A=0\to \left|A\right|=0$$
4		oveq2	$$⊢A=0\to xA=x\cdot 0$$
5	3 4	eqeq12d	$$⊢A=0\to \left(\left|A\right|=xA\leftrightarrow 0=x\cdot 0\right)$$
6	5	anbi2d	$$⊢A=0\to \left(\left(\left|x\right|=1\wedge \left|A\right|=xA\right)\leftrightarrow \left(\left|x\right|=1\wedge 0=x\cdot 0\right)\right)$$
7	6	rexbidv	$$⊢A=0\to \left(\exists x\in ℂ\left(\left|x\right|=1\wedge \left|A\right|=xA\right)\leftrightarrow \exists x\in ℂ\left(\left|x\right|=1\wedge 0=x\cdot 0\right)\right)$$
8		simpl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to A\in ℂ$$
9	8	cjcld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \bar{A}\in ℂ$$
10		abscl	$$⊢A\in ℂ\to \left|A\right|\in ℝ$$
11	10	adantr	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|\in ℝ$$
12	11	recnd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|\in ℂ$$
13		abs00	$$⊢A\in ℂ\to \left(\left|A\right|=0\leftrightarrow A=0\right)$$
14	13	necon3bid	$$⊢A\in ℂ\to \left(\left|A\right|\ne 0\leftrightarrow A\ne 0\right)$$
15	14	biimpar	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|\ne 0$$
16	9 12 15	divcld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{\bar{A}}{\left|A\right|}\in ℂ$$
17		absdiv	$$⊢\left(\bar{A}\in ℂ\wedge \left|A\right|\in ℂ\wedge \left|A\right|\ne 0\right)\to \left|\frac{\bar{A}}{\left|A\right|}\right|=\frac{\left|\bar{A}\right|}{\left|\left|A\right|\right|}$$
18	9 12 15 17	syl3anc	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\frac{\bar{A}}{\left|A\right|}\right|=\frac{\left|\bar{A}\right|}{\left|\left|A\right|\right|}$$
19		abscj	$$⊢A\in ℂ\to \left|\bar{A}\right|=\left|A\right|$$
20	19	adantr	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\bar{A}\right|=\left|A\right|$$
21		absidm	$$⊢A\in ℂ\to \left|\left|A\right|\right|=\left|A\right|$$
22	21	adantr	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\left|A\right|\right|=\left|A\right|$$
23	20 22	oveq12d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{\left|\bar{A}\right|}{\left|\left|A\right|\right|}=\frac{\left|A\right|}{\left|A\right|}$$
24	12 15	dividd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{\left|A\right|}{\left|A\right|}=1$$
25	18 23 24	3eqtrd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\frac{\bar{A}}{\left|A\right|}\right|=1$$
26	8 9 12 15	divassd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{A\bar{A}}{\left|A\right|}=A\left(\frac{\bar{A}}{\left|A\right|}\right)$$
27	12	sqvald	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\left|A\right|}^2=\left|A\right|\left|A\right|$$
28		absvalsq	$$⊢A\in ℂ\to {\left|A\right|}^2=A\bar{A}$$
29	28	adantr	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\left|A\right|}^2=A\bar{A}$$
30	27 29	eqtr3d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|\left|A\right|=A\bar{A}$$
31	12 12 15 30	mvllmuld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|=\frac{A\bar{A}}{\left|A\right|}$$
32	16 8	mulcomd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(\frac{\bar{A}}{\left|A\right|}\right)A=A\left(\frac{\bar{A}}{\left|A\right|}\right)$$
33	26 31 32	3eqtr4d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|=\left(\frac{\bar{A}}{\left|A\right|}\right)A$$
34		fveqeq2	$$⊢x=\frac{\bar{A}}{\left|A\right|}\to \left(\left|x\right|=1\leftrightarrow \left|\frac{\bar{A}}{\left|A\right|}\right|=1\right)$$
35		oveq1	$$⊢x=\frac{\bar{A}}{\left|A\right|}\to xA=\left(\frac{\bar{A}}{\left|A\right|}\right)A$$
36	35	eqeq2d	$$⊢x=\frac{\bar{A}}{\left|A\right|}\to \left(\left|A\right|=xA\leftrightarrow \left|A\right|=\left(\frac{\bar{A}}{\left|A\right|}\right)A\right)$$
37	34 36	anbi12d	$$⊢x=\frac{\bar{A}}{\left|A\right|}\to \left(\left(\left|x\right|=1\wedge \left|A\right|=xA\right)\leftrightarrow \left(\left|\frac{\bar{A}}{\left|A\right|}\right|=1\wedge \left|A\right|=\left(\frac{\bar{A}}{\left|A\right|}\right)A\right)\right)$$
38	37	rspcev	$$⊢\left(\frac{\bar{A}}{\left|A\right|}\in ℂ\wedge \left(\left|\frac{\bar{A}}{\left|A\right|}\right|=1\wedge \left|A\right|=\left(\frac{\bar{A}}{\left|A\right|}\right)A\right)\right)\to \exists x\in ℂ\left(\left|x\right|=1\wedge \left|A\right|=xA\right)$$
39	16 25 33 38	syl12anc	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \exists x\in ℂ\left(\left|x\right|=1\wedge \left|A\right|=xA\right)$$
40		ax-icn	$$⊢\mathrm{i}\in ℂ$$
41		absi	$$⊢\left|\mathrm{i}\right|=1$$
42		it0e0	$$⊢\mathrm{i}\cdot 0=0$$
43	42	eqcomi	$$⊢0=\mathrm{i}\cdot 0$$
44	41 43	pm3.2i	$$⊢\left(\left|\mathrm{i}\right|=1\wedge 0=\mathrm{i}\cdot 0\right)$$
45		fveqeq2	$$⊢x=\mathrm{i}\to \left(\left|x\right|=1\leftrightarrow \left|\mathrm{i}\right|=1\right)$$
46		oveq1	$$⊢x=\mathrm{i}\to x\cdot 0=\mathrm{i}\cdot 0$$
47	46	eqeq2d	$$⊢x=\mathrm{i}\to \left(0=x\cdot 0\leftrightarrow 0=\mathrm{i}\cdot 0\right)$$
48	45 47	anbi12d	$$⊢x=\mathrm{i}\to \left(\left(\left|x\right|=1\wedge 0=x\cdot 0\right)\leftrightarrow \left(\left|\mathrm{i}\right|=1\wedge 0=\mathrm{i}\cdot 0\right)\right)$$
49	48	rspcev	$$⊢\left(\mathrm{i}\in ℂ\wedge \left(\left|\mathrm{i}\right|=1\wedge 0=\mathrm{i}\cdot 0\right)\right)\to \exists x\in ℂ\left(\left|x\right|=1\wedge 0=x\cdot 0\right)$$
50	40 44 49	mp2an	$$⊢\exists x\in ℂ\left(\left|x\right|=1\wedge 0=x\cdot 0\right)$$
51	50	a1i	$$⊢A\in ℂ\to \exists x\in ℂ\left(\left|x\right|=1\wedge 0=x\cdot 0\right)$$
52	7 39 51	pm2.61ne	$$⊢A\in ℂ\to \exists x\in ℂ\left(\left|x\right|=1\wedge \left|A\right|=xA\right)$$