Metamath Proof Explorer

Theorem norm1

Description: From any nonzero Hilbert space vector, construct a vector whose norm is 1. (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion norm1 ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)=1$

Proof

Step Hyp Ref Expression
1 normcl ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({A}\right)\in ℝ$
2 1 adantr ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left({A}\right)\in ℝ$
3 normne0 ${⊢}{A}\in ℋ\to \left({norm}_{ℎ}\left({A}\right)\ne 0↔{A}\ne {0}_{ℎ}\right)$
4 3 biimpar ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left({A}\right)\ne 0$
5 2 4 rereccld ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to \frac{1}{{norm}_{ℎ}\left({A}\right)}\in ℝ$
6 5 recnd ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to \frac{1}{{norm}_{ℎ}\left({A}\right)}\in ℂ$
7 simpl ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {A}\in ℋ$
8 norm-iii ${⊢}\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\in ℂ\wedge {A}\in ℋ\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)=\left|\frac{1}{{norm}_{ℎ}\left({A}\right)}\right|{norm}_{ℎ}\left({A}\right)$
9 6 7 8 syl2anc ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)=\left|\frac{1}{{norm}_{ℎ}\left({A}\right)}\right|{norm}_{ℎ}\left({A}\right)$
10 normgt0 ${⊢}{A}\in ℋ\to \left({A}\ne {0}_{ℎ}↔0<{norm}_{ℎ}\left({A}\right)\right)$
11 10 biimpa ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to 0<{norm}_{ℎ}\left({A}\right)$
12 1re ${⊢}1\in ℝ$
13 0le1 ${⊢}0\le 1$
14 divge0 ${⊢}\left(\left(1\in ℝ\wedge 0\le 1\right)\wedge \left({norm}_{ℎ}\left({A}\right)\in ℝ\wedge 0<{norm}_{ℎ}\left({A}\right)\right)\right)\to 0\le \frac{1}{{norm}_{ℎ}\left({A}\right)}$
15 12 13 14 mpanl12 ${⊢}\left({norm}_{ℎ}\left({A}\right)\in ℝ\wedge 0<{norm}_{ℎ}\left({A}\right)\right)\to 0\le \frac{1}{{norm}_{ℎ}\left({A}\right)}$
16 2 11 15 syl2anc ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to 0\le \frac{1}{{norm}_{ℎ}\left({A}\right)}$
17 5 16 absidd ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to \left|\frac{1}{{norm}_{ℎ}\left({A}\right)}\right|=\frac{1}{{norm}_{ℎ}\left({A}\right)}$
18 17 oveq1d ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to \left|\frac{1}{{norm}_{ℎ}\left({A}\right)}\right|{norm}_{ℎ}\left({A}\right)=\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){norm}_{ℎ}\left({A}\right)$
19 1 recnd ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({A}\right)\in ℂ$
20 19 adantr ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left({A}\right)\in ℂ$
21 20 4 recid2d ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to \left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){norm}_{ℎ}\left({A}\right)=1$
22 9 18 21 3eqtrd ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)=1$