# Metamath Proof Explorer

## Theorem branmfn

Description: The norm of the bra function. (Contributed by NM, 24-May-2006) (New usage is discouraged.)

Ref Expression
Assertion branmfn $⊢ A ∈ ℋ → norm fn ⁡ bra ⁡ A = norm ℎ ⁡ A$

### Proof

Step Hyp Ref Expression
1 2fveq3 $⊢ A = 0 ℎ → norm fn ⁡ bra ⁡ A = norm fn ⁡ bra ⁡ 0 ℎ$
2 fveq2 $⊢ A = 0 ℎ → norm ℎ ⁡ A = norm ℎ ⁡ 0 ℎ$
3 1 2 eqeq12d $⊢ A = 0 ℎ → norm fn ⁡ bra ⁡ A = norm ℎ ⁡ A ↔ norm fn ⁡ bra ⁡ 0 ℎ = norm ℎ ⁡ 0 ℎ$
4 brafn $⊢ A ∈ ℋ → bra ⁡ A : ℋ ⟶ ℂ$
5 nmfnval $⊢ bra ⁡ A : ℋ ⟶ ℂ → norm fn ⁡ bra ⁡ A = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y ℝ * <$
6 4 5 syl $⊢ A ∈ ℋ → norm fn ⁡ bra ⁡ A = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y ℝ * <$
7 6 adantr $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm fn ⁡ bra ⁡ A = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y ℝ * <$
8 nmfnsetre $⊢ bra ⁡ A : ℋ ⟶ ℂ → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y ⊆ ℝ$
9 4 8 syl $⊢ A ∈ ℋ → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y ⊆ ℝ$
10 ressxr $⊢ ℝ ⊆ ℝ *$
11 9 10 sstrdi $⊢ A ∈ ℋ → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y ⊆ ℝ *$
12 normcl $⊢ A ∈ ℋ → norm ℎ ⁡ A ∈ ℝ$
13 12 rexrd $⊢ A ∈ ℋ → norm ℎ ⁡ A ∈ ℝ *$
14 11 13 jca $⊢ A ∈ ℋ → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y ⊆ ℝ * ∧ norm ℎ ⁡ A ∈ ℝ *$
15 14 adantr $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y ⊆ ℝ * ∧ norm ℎ ⁡ A ∈ ℝ *$
16 vex $⊢ z ∈ V$
17 eqeq1 $⊢ x = z → x = bra ⁡ A ⁡ y ↔ z = bra ⁡ A ⁡ y$
18 17 anbi2d $⊢ x = z → norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y ↔ norm ℎ ⁡ y ≤ 1 ∧ z = bra ⁡ A ⁡ y$
19 18 rexbidv $⊢ x = z → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y ↔ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ z = bra ⁡ A ⁡ y$
20 16 19 elab $⊢ z ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y ↔ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ z = bra ⁡ A ⁡ y$
21 id $⊢ z = bra ⁡ A ⁡ y → z = bra ⁡ A ⁡ y$
22 braval $⊢ A ∈ ℋ ∧ y ∈ ℋ → bra ⁡ A ⁡ y = y ⋅ ih A$
23 22 fveq2d $⊢ A ∈ ℋ ∧ y ∈ ℋ → bra ⁡ A ⁡ y = y ⋅ ih A$
24 23 adantr $⊢ A ∈ ℋ ∧ y ∈ ℋ ∧ norm ℎ ⁡ y ≤ 1 → bra ⁡ A ⁡ y = y ⋅ ih A$
25 21 24 sylan9eqr $⊢ A ∈ ℋ ∧ y ∈ ℋ ∧ norm ℎ ⁡ y ≤ 1 ∧ z = bra ⁡ A ⁡ y → z = y ⋅ ih A$
26 bcs2 $⊢ y ∈ ℋ ∧ A ∈ ℋ ∧ norm ℎ ⁡ y ≤ 1 → y ⋅ ih A ≤ norm ℎ ⁡ A$
27 26 3expa $⊢ y ∈ ℋ ∧ A ∈ ℋ ∧ norm ℎ ⁡ y ≤ 1 → y ⋅ ih A ≤ norm ℎ ⁡ A$
28 27 ancom1s $⊢ A ∈ ℋ ∧ y ∈ ℋ ∧ norm ℎ ⁡ y ≤ 1 → y ⋅ ih A ≤ norm ℎ ⁡ A$
29 28 adantr $⊢ A ∈ ℋ ∧ y ∈ ℋ ∧ norm ℎ ⁡ y ≤ 1 ∧ z = bra ⁡ A ⁡ y → y ⋅ ih A ≤ norm ℎ ⁡ A$
30 25 29 eqbrtrd $⊢ A ∈ ℋ ∧ y ∈ ℋ ∧ norm ℎ ⁡ y ≤ 1 ∧ z = bra ⁡ A ⁡ y → z ≤ norm ℎ ⁡ A$
31 30 exp41 $⊢ A ∈ ℋ → y ∈ ℋ → norm ℎ ⁡ y ≤ 1 → z = bra ⁡ A ⁡ y → z ≤ norm ℎ ⁡ A$
32 31 imp4a $⊢ A ∈ ℋ → y ∈ ℋ → norm ℎ ⁡ y ≤ 1 ∧ z = bra ⁡ A ⁡ y → z ≤ norm ℎ ⁡ A$
33 32 rexlimdv $⊢ A ∈ ℋ → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ z = bra ⁡ A ⁡ y → z ≤ norm ℎ ⁡ A$
34 33 imp $⊢ A ∈ ℋ ∧ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ z = bra ⁡ A ⁡ y → z ≤ norm ℎ ⁡ A$
35 20 34 sylan2b $⊢ A ∈ ℋ ∧ z ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y → z ≤ norm ℎ ⁡ A$
36 35 ralrimiva $⊢ A ∈ ℋ → ∀ z ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y z ≤ norm ℎ ⁡ A$
37 36 adantr $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → ∀ z ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y z ≤ norm ℎ ⁡ A$
38 12 recnd $⊢ A ∈ ℋ → norm ℎ ⁡ A ∈ ℂ$
39 38 adantr $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A ∈ ℂ$
40 normne0 $⊢ A ∈ ℋ → norm ℎ ⁡ A ≠ 0 ↔ A ≠ 0 ℎ$
41 40 biimpar $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A ≠ 0$
42 39 41 reccld $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ∈ ℂ$
43 simpl $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → A ∈ ℋ$
44 hvmulcl $⊢ 1 norm ℎ ⁡ A ∈ ℂ ∧ A ∈ ℋ → 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℋ$
45 42 43 44 syl2anc $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℋ$
46 norm1 $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1$
47 1le1 $⊢ 1 ≤ 1$
48 46 47 eqbrtrdi $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ 1$
49 ax-his3 $⊢ 1 norm ℎ ⁡ A ∈ ℂ ∧ A ∈ ℋ ∧ A ∈ ℋ → 1 norm ℎ ⁡ A ⋅ ℎ A ⋅ ih A = 1 norm ℎ ⁡ A ⁢ A ⋅ ih A$
50 42 43 43 49 syl3anc $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ⋅ ℎ A ⋅ ih A = 1 norm ℎ ⁡ A ⁢ A ⋅ ih A$
51 12 adantr $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A ∈ ℝ$
52 51 41 rereccld $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ∈ ℝ$
53 hiidrcl $⊢ A ∈ ℋ → A ⋅ ih A ∈ ℝ$
54 53 adantr $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → A ⋅ ih A ∈ ℝ$
55 52 54 remulcld $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ⁢ A ⋅ ih A ∈ ℝ$
56 50 55 eqeltrd $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ⋅ ℎ A ⋅ ih A ∈ ℝ$
57 normgt0 $⊢ A ∈ ℋ → A ≠ 0 ℎ ↔ 0 < norm ℎ ⁡ A$
58 57 biimpa $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 0 < norm ℎ ⁡ A$
59 51 58 recgt0d $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 0 < 1 norm ℎ ⁡ A$
60 0re $⊢ 0 ∈ ℝ$
61 ltle $⊢ 0 ∈ ℝ ∧ 1 norm ℎ ⁡ A ∈ ℝ → 0 < 1 norm ℎ ⁡ A → 0 ≤ 1 norm ℎ ⁡ A$
62 60 61 mpan $⊢ 1 norm ℎ ⁡ A ∈ ℝ → 0 < 1 norm ℎ ⁡ A → 0 ≤ 1 norm ℎ ⁡ A$
63 52 59 62 sylc $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 0 ≤ 1 norm ℎ ⁡ A$
64 hiidge0 $⊢ A ∈ ℋ → 0 ≤ A ⋅ ih A$
65 64 adantr $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 0 ≤ A ⋅ ih A$
66 52 54 63 65 mulge0d $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 0 ≤ 1 norm ℎ ⁡ A ⁢ A ⋅ ih A$
67 66 50 breqtrrd $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 0 ≤ 1 norm ℎ ⁡ A ⋅ ℎ A ⋅ ih A$
68 56 67 absidd $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ⋅ ℎ A ⋅ ih A = 1 norm ℎ ⁡ A ⋅ ℎ A ⋅ ih A$
69 39 41 recid2d $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ⁢ norm ℎ ⁡ A = 1$
70 69 oveq2d $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A ⁢ 1 norm ℎ ⁡ A ⁢ norm ℎ ⁡ A = norm ℎ ⁡ A ⋅ 1$
71 39 42 39 mul12d $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A ⁢ 1 norm ℎ ⁡ A ⁢ norm ℎ ⁡ A = 1 norm ℎ ⁡ A ⁢ norm ℎ ⁡ A ⁢ norm ℎ ⁡ A$
72 38 sqvald $⊢ A ∈ ℋ → norm ℎ ⁡ A 2 = norm ℎ ⁡ A ⁢ norm ℎ ⁡ A$
73 normsq $⊢ A ∈ ℋ → norm ℎ ⁡ A 2 = A ⋅ ih A$
74 72 73 eqtr3d $⊢ A ∈ ℋ → norm ℎ ⁡ A ⁢ norm ℎ ⁡ A = A ⋅ ih A$
75 74 adantr $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A ⁢ norm ℎ ⁡ A = A ⋅ ih A$
76 75 oveq2d $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ⁢ norm ℎ ⁡ A ⁢ norm ℎ ⁡ A = 1 norm ℎ ⁡ A ⁢ A ⋅ ih A$
77 71 76 eqtrd $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A ⁢ 1 norm ℎ ⁡ A ⁢ norm ℎ ⁡ A = 1 norm ℎ ⁡ A ⁢ A ⋅ ih A$
78 38 mulid1d $⊢ A ∈ ℋ → norm ℎ ⁡ A ⋅ 1 = norm ℎ ⁡ A$
79 78 adantr $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A ⋅ 1 = norm ℎ ⁡ A$
80 70 77 79 3eqtr3rd $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A = 1 norm ℎ ⁡ A ⁢ A ⋅ ih A$
81 50 68 80 3eqtr4rd $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A = 1 norm ℎ ⁡ A ⋅ ℎ A ⋅ ih A$
82 fveq2 $⊢ y = 1 norm ℎ ⁡ A ⋅ ℎ A → norm ℎ ⁡ y = norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A$
83 82 breq1d $⊢ y = 1 norm ℎ ⁡ A ⋅ ℎ A → norm ℎ ⁡ y ≤ 1 ↔ norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ 1$
84 fvoveq1 $⊢ y = 1 norm ℎ ⁡ A ⋅ ℎ A → y ⋅ ih A = 1 norm ℎ ⁡ A ⋅ ℎ A ⋅ ih A$
85 84 eqeq2d $⊢ y = 1 norm ℎ ⁡ A ⋅ ℎ A → norm ℎ ⁡ A = y ⋅ ih A ↔ norm ℎ ⁡ A = 1 norm ℎ ⁡ A ⋅ ℎ A ⋅ ih A$
86 83 85 anbi12d $⊢ y = 1 norm ℎ ⁡ A ⋅ ℎ A → norm ℎ ⁡ y ≤ 1 ∧ norm ℎ ⁡ A = y ⋅ ih A ↔ norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ 1 ∧ norm ℎ ⁡ A = 1 norm ℎ ⁡ A ⋅ ℎ A ⋅ ih A$
87 86 rspcev $⊢ 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℋ ∧ norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ 1 ∧ norm ℎ ⁡ A = 1 norm ℎ ⁡ A ⋅ ℎ A ⋅ ih A → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ norm ℎ ⁡ A = y ⋅ ih A$
88 45 48 81 87 syl12anc $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ norm ℎ ⁡ A = y ⋅ ih A$
89 23 eqeq2d $⊢ A ∈ ℋ ∧ y ∈ ℋ → norm ℎ ⁡ A = bra ⁡ A ⁡ y ↔ norm ℎ ⁡ A = y ⋅ ih A$
90 89 anbi2d $⊢ A ∈ ℋ ∧ y ∈ ℋ → norm ℎ ⁡ y ≤ 1 ∧ norm ℎ ⁡ A = bra ⁡ A ⁡ y ↔ norm ℎ ⁡ y ≤ 1 ∧ norm ℎ ⁡ A = y ⋅ ih A$
91 90 rexbidva $⊢ A ∈ ℋ → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ norm ℎ ⁡ A = bra ⁡ A ⁡ y ↔ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ norm ℎ ⁡ A = y ⋅ ih A$
92 91 adantr $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ norm ℎ ⁡ A = bra ⁡ A ⁡ y ↔ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ norm ℎ ⁡ A = y ⋅ ih A$
93 88 92 mpbird $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ norm ℎ ⁡ A = bra ⁡ A ⁡ y$
94 eqeq1 $⊢ x = norm ℎ ⁡ A → x = bra ⁡ A ⁡ y ↔ norm ℎ ⁡ A = bra ⁡ A ⁡ y$
95 94 anbi2d $⊢ x = norm ℎ ⁡ A → norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y ↔ norm ℎ ⁡ y ≤ 1 ∧ norm ℎ ⁡ A = bra ⁡ A ⁡ y$
96 95 rexbidv $⊢ x = norm ℎ ⁡ A → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y ↔ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ norm ℎ ⁡ A = bra ⁡ A ⁡ y$
97 39 93 96 elabd $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y$
98 breq2 $⊢ w = norm ℎ ⁡ A → z < w ↔ z < norm ℎ ⁡ A$
99 98 rspcev $⊢ norm ℎ ⁡ A ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y ∧ z < norm ℎ ⁡ A → ∃ w ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y z < w$
100 97 99 sylan $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ z < norm ℎ ⁡ A → ∃ w ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y z < w$
101 100 adantlr $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ z ∈ ℝ ∧ z < norm ℎ ⁡ A → ∃ w ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y z < w$
102 101 ex $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ z ∈ ℝ → z < norm ℎ ⁡ A → ∃ w ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y z < w$
103 102 ralrimiva $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → ∀ z ∈ ℝ z < norm ℎ ⁡ A → ∃ w ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y z < w$
104 supxr2 $⊢ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y ⊆ ℝ * ∧ norm ℎ ⁡ A ∈ ℝ * ∧ ∀ z ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y z ≤ norm ℎ ⁡ A ∧ ∀ z ∈ ℝ z < norm ℎ ⁡ A → ∃ w ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y z < w → sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y ℝ * < = norm ℎ ⁡ A$
105 15 37 103 104 syl12anc $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = bra ⁡ A ⁡ y ℝ * < = norm ℎ ⁡ A$
106 7 105 eqtrd $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm fn ⁡ bra ⁡ A = norm ℎ ⁡ A$
107 nmfn0 $⊢ norm fn ⁡ ℋ × 0 = 0$
108 bra0 $⊢ bra ⁡ 0 ℎ = ℋ × 0$
109 108 fveq2i $⊢ norm fn ⁡ bra ⁡ 0 ℎ = norm fn ⁡ ℋ × 0$
110 norm0 $⊢ norm ℎ ⁡ 0 ℎ = 0$
111 107 109 110 3eqtr4i $⊢ norm fn ⁡ bra ⁡ 0 ℎ = norm ℎ ⁡ 0 ℎ$
112 111 a1i $⊢ A ∈ ℋ → norm fn ⁡ bra ⁡ 0 ℎ = norm ℎ ⁡ 0 ℎ$
113 3 106 112 pm2.61ne $⊢ A ∈ ℋ → norm fn ⁡ bra ⁡ A = norm ℎ ⁡ A$