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