Step | Hyp | Ref
| Expression |
1 | | 2fveq3 6502 |
. . 3
⊢ (𝐴 = 0ℎ →
(normfn‘(bra‘𝐴)) =
(normfn‘(bra‘0ℎ))) |
2 | | fveq2 6497 |
. . 3
⊢ (𝐴 = 0ℎ →
(normℎ‘𝐴) =
(normℎ‘0ℎ)) |
3 | 1, 2 | eqeq12d 2788 |
. 2
⊢ (𝐴 = 0ℎ →
((normfn‘(bra‘𝐴)) = (normℎ‘𝐴) ↔
(normfn‘(bra‘0ℎ)) =
(normℎ‘0ℎ))) |
4 | | brafn 29521 |
. . . . 5
⊢ (𝐴 ∈ ℋ →
(bra‘𝐴):
ℋ⟶ℂ) |
5 | | nmfnval 29450 |
. . . . 5
⊢
((bra‘𝐴):
ℋ⟶ℂ → (normfn‘(bra‘𝐴)) = sup({𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))}, ℝ*, <
)) |
6 | 4, 5 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ℋ →
(normfn‘(bra‘𝐴)) = sup({𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))}, ℝ*, <
)) |
7 | 6 | adantr 473 |
. . 3
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normfn‘(bra‘𝐴)) = sup({𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))}, ℝ*, <
)) |
8 | | nmfnsetre 29451 |
. . . . . . . 8
⊢
((bra‘𝐴):
ℋ⟶ℂ → {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))} ⊆ ℝ) |
9 | 4, 8 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℋ → {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))} ⊆ ℝ) |
10 | | ressxr 10483 |
. . . . . . 7
⊢ ℝ
⊆ ℝ* |
11 | 9, 10 | syl6ss 3865 |
. . . . . 6
⊢ (𝐴 ∈ ℋ → {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))} ⊆
ℝ*) |
12 | | normcl 28697 |
. . . . . . 7
⊢ (𝐴 ∈ ℋ →
(normℎ‘𝐴) ∈ ℝ) |
13 | 12 | rexrd 10489 |
. . . . . 6
⊢ (𝐴 ∈ ℋ →
(normℎ‘𝐴) ∈
ℝ*) |
14 | 11, 13 | jca 504 |
. . . . 5
⊢ (𝐴 ∈ ℋ → ({𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))} ⊆ ℝ* ∧
(normℎ‘𝐴) ∈
ℝ*)) |
15 | 14 | adantr 473 |
. . . 4
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ({𝑥 ∣
∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))} ⊆ ℝ* ∧
(normℎ‘𝐴) ∈
ℝ*)) |
16 | | vex 3413 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
17 | | eqeq1 2777 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑥 = (abs‘((bra‘𝐴)‘𝑦)) ↔ 𝑧 = (abs‘((bra‘𝐴)‘𝑦)))) |
18 | 17 | anbi2d 620 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 →
(((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦))) ↔
((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (abs‘((bra‘𝐴)‘𝑦))))) |
19 | 18 | rexbidv 3237 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦))) ↔ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (abs‘((bra‘𝐴)‘𝑦))))) |
20 | 16, 19 | elab 3577 |
. . . . . . 7
⊢ (𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))} ↔ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (abs‘((bra‘𝐴)‘𝑦)))) |
21 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (abs‘((bra‘𝐴)‘𝑦)) → 𝑧 = (abs‘((bra‘𝐴)‘𝑦))) |
22 | | braval 29518 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
((bra‘𝐴)‘𝑦) = (𝑦 ·ih 𝐴)) |
23 | 22 | fveq2d 6501 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(abs‘((bra‘𝐴)‘𝑦)) = (abs‘(𝑦 ·ih 𝐴))) |
24 | 23 | adantr 473 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧
(normℎ‘𝑦) ≤ 1) → (abs‘((bra‘𝐴)‘𝑦)) = (abs‘(𝑦 ·ih 𝐴))) |
25 | 21, 24 | sylan9eqr 2831 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧
(normℎ‘𝑦) ≤ 1) ∧ 𝑧 = (abs‘((bra‘𝐴)‘𝑦))) → 𝑧 = (abs‘(𝑦 ·ih 𝐴))) |
26 | | bcs2 28754 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℋ ∧ 𝐴 ∈ ℋ ∧
(normℎ‘𝑦) ≤ 1) → (abs‘(𝑦
·ih 𝐴)) ≤ (normℎ‘𝐴)) |
27 | 26 | 3expa 1099 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∈ ℋ ∧ 𝐴 ∈ ℋ) ∧
(normℎ‘𝑦) ≤ 1) → (abs‘(𝑦
·ih 𝐴)) ≤ (normℎ‘𝐴)) |
28 | 27 | ancom1s 641 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧
(normℎ‘𝑦) ≤ 1) → (abs‘(𝑦
·ih 𝐴)) ≤ (normℎ‘𝐴)) |
29 | 28 | adantr 473 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧
(normℎ‘𝑦) ≤ 1) ∧ 𝑧 = (abs‘((bra‘𝐴)‘𝑦))) → (abs‘(𝑦 ·ih 𝐴)) ≤
(normℎ‘𝐴)) |
30 | 25, 29 | eqbrtrd 4948 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧
(normℎ‘𝑦) ≤ 1) ∧ 𝑧 = (abs‘((bra‘𝐴)‘𝑦))) → 𝑧 ≤ (normℎ‘𝐴)) |
31 | 30 | exp41 427 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℋ → (𝑦 ∈ ℋ →
((normℎ‘𝑦) ≤ 1 → (𝑧 = (abs‘((bra‘𝐴)‘𝑦)) → 𝑧 ≤ (normℎ‘𝐴))))) |
32 | 31 | imp4a 415 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℋ → (𝑦 ∈ ℋ →
(((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (abs‘((bra‘𝐴)‘𝑦))) → 𝑧 ≤ (normℎ‘𝐴)))) |
33 | 32 | rexlimdv 3223 |
. . . . . . . 8
⊢ (𝐴 ∈ ℋ →
(∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (abs‘((bra‘𝐴)‘𝑦))) → 𝑧 ≤ (normℎ‘𝐴))) |
34 | 33 | imp 398 |
. . . . . . 7
⊢ ((𝐴 ∈ ℋ ∧
∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (abs‘((bra‘𝐴)‘𝑦)))) → 𝑧 ≤ (normℎ‘𝐴)) |
35 | 20, 34 | sylan2b 585 |
. . . . . 6
⊢ ((𝐴 ∈ ℋ ∧ 𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))}) → 𝑧 ≤ (normℎ‘𝐴)) |
36 | 35 | ralrimiva 3127 |
. . . . 5
⊢ (𝐴 ∈ ℋ →
∀𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))}𝑧 ≤ (normℎ‘𝐴)) |
37 | 36 | adantr 473 |
. . . 4
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ∀𝑧 ∈
{𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))}𝑧 ≤ (normℎ‘𝐴)) |
38 | 12 | recnd 10467 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℋ →
(normℎ‘𝐴) ∈ ℂ) |
39 | 38 | adantr 473 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘𝐴) ∈ ℂ) |
40 | | normne0 28702 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℋ →
((normℎ‘𝐴) ≠ 0 ↔ 𝐴 ≠
0ℎ)) |
41 | 40 | biimpar 470 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘𝐴) ≠ 0) |
42 | 39, 41 | reccld 11209 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (1 / (normℎ‘𝐴)) ∈ ℂ) |
43 | | simpl 475 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ 𝐴 ∈
ℋ) |
44 | | hvmulcl 28585 |
. . . . . . . . . . . 12
⊢ (((1 /
(normℎ‘𝐴)) ∈ ℂ ∧ 𝐴 ∈ ℋ) → ((1 /
(normℎ‘𝐴)) ·ℎ 𝐴) ∈
ℋ) |
45 | 42, 43, 44 | syl2anc 576 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ((1 / (normℎ‘𝐴)) ·ℎ 𝐴) ∈
ℋ) |
46 | | norm1 28821 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘((1 /
(normℎ‘𝐴)) ·ℎ 𝐴)) = 1) |
47 | | 1le1 11068 |
. . . . . . . . . . . 12
⊢ 1 ≤
1 |
48 | 46, 47 | syl6eqbr 4965 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘((1 /
(normℎ‘𝐴)) ·ℎ 𝐴)) ≤ 1) |
49 | | ax-his3 28656 |
. . . . . . . . . . . . 13
⊢ (((1 /
(normℎ‘𝐴)) ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (((1 /
(normℎ‘𝐴)) ·ℎ 𝐴)
·ih 𝐴) = ((1 /
(normℎ‘𝐴)) · (𝐴 ·ih 𝐴))) |
50 | 42, 43, 43, 49 | syl3anc 1352 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (((1 / (normℎ‘𝐴)) ·ℎ 𝐴)
·ih 𝐴) = ((1 /
(normℎ‘𝐴)) · (𝐴 ·ih 𝐴))) |
51 | 12 | adantr 473 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘𝐴) ∈ ℝ) |
52 | 51, 41 | rereccld 11267 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (1 / (normℎ‘𝐴)) ∈ ℝ) |
53 | | hiidrcl 28667 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℋ → (𝐴
·ih 𝐴) ∈ ℝ) |
54 | 53 | adantr 473 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (𝐴
·ih 𝐴) ∈ ℝ) |
55 | 52, 54 | remulcld 10469 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ((1 / (normℎ‘𝐴)) · (𝐴 ·ih 𝐴)) ∈
ℝ) |
56 | 50, 55 | eqeltrd 2861 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (((1 / (normℎ‘𝐴)) ·ℎ 𝐴)
·ih 𝐴) ∈ ℝ) |
57 | | normgt0 28699 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℋ → (𝐴 ≠ 0ℎ
↔ 0 < (normℎ‘𝐴))) |
58 | 57 | biimpa 469 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ 0 < (normℎ‘𝐴)) |
59 | 51, 58 | recgt0d 11374 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ 0 < (1 / (normℎ‘𝐴))) |
60 | | 0re 10440 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℝ |
61 | | ltle 10528 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℝ ∧ (1 / (normℎ‘𝐴)) ∈ ℝ) → (0 < (1 /
(normℎ‘𝐴)) → 0 ≤ (1 /
(normℎ‘𝐴)))) |
62 | 60, 61 | mpan 678 |
. . . . . . . . . . . . . . . 16
⊢ ((1 /
(normℎ‘𝐴)) ∈ ℝ → (0 < (1 /
(normℎ‘𝐴)) → 0 ≤ (1 /
(normℎ‘𝐴)))) |
63 | 52, 59, 62 | sylc 65 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ 0 ≤ (1 / (normℎ‘𝐴))) |
64 | | hiidge0 28670 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℋ → 0 ≤
(𝐴
·ih 𝐴)) |
65 | 64 | adantr 473 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ 0 ≤ (𝐴
·ih 𝐴)) |
66 | 52, 54, 63, 65 | mulge0d 11017 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ 0 ≤ ((1 / (normℎ‘𝐴)) · (𝐴 ·ih 𝐴))) |
67 | 66, 50 | breqtrrd 4954 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ 0 ≤ (((1 / (normℎ‘𝐴)) ·ℎ 𝐴)
·ih 𝐴)) |
68 | 56, 67 | absidd 14642 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (abs‘(((1 / (normℎ‘𝐴)) ·ℎ 𝐴)
·ih 𝐴)) = (((1 /
(normℎ‘𝐴)) ·ℎ 𝐴)
·ih 𝐴)) |
69 | 39, 41 | recid2d 11212 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ((1 / (normℎ‘𝐴)) ·
(normℎ‘𝐴)) = 1) |
70 | 69 | oveq2d 6991 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ((normℎ‘𝐴) · ((1 /
(normℎ‘𝐴)) ·
(normℎ‘𝐴))) = ((normℎ‘𝐴) · 1)) |
71 | 39, 42, 39 | mul12d 10648 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ((normℎ‘𝐴) · ((1 /
(normℎ‘𝐴)) ·
(normℎ‘𝐴))) = ((1 /
(normℎ‘𝐴)) ·
((normℎ‘𝐴) ·
(normℎ‘𝐴)))) |
72 | 38 | sqvald 13321 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℋ →
((normℎ‘𝐴)↑2) =
((normℎ‘𝐴) ·
(normℎ‘𝐴))) |
73 | | normsq 28706 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℋ →
((normℎ‘𝐴)↑2) = (𝐴 ·ih 𝐴)) |
74 | 72, 73 | eqtr3d 2811 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℋ →
((normℎ‘𝐴) ·
(normℎ‘𝐴)) = (𝐴 ·ih 𝐴)) |
75 | 74 | adantr 473 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ((normℎ‘𝐴) ·
(normℎ‘𝐴)) = (𝐴 ·ih 𝐴)) |
76 | 75 | oveq2d 6991 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ((1 / (normℎ‘𝐴)) ·
((normℎ‘𝐴) ·
(normℎ‘𝐴))) = ((1 /
(normℎ‘𝐴)) · (𝐴 ·ih 𝐴))) |
77 | 71, 76 | eqtrd 2809 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ((normℎ‘𝐴) · ((1 /
(normℎ‘𝐴)) ·
(normℎ‘𝐴))) = ((1 /
(normℎ‘𝐴)) · (𝐴 ·ih 𝐴))) |
78 | 38 | mulid1d 10456 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℋ →
((normℎ‘𝐴) · 1) =
(normℎ‘𝐴)) |
79 | 78 | adantr 473 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ((normℎ‘𝐴) · 1) =
(normℎ‘𝐴)) |
80 | 70, 77, 79 | 3eqtr3rd 2818 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘𝐴) = ((1 /
(normℎ‘𝐴)) · (𝐴 ·ih 𝐴))) |
81 | 50, 68, 80 | 3eqtr4rd 2820 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘𝐴) = (abs‘(((1 /
(normℎ‘𝐴)) ·ℎ 𝐴)
·ih 𝐴))) |
82 | | fveq2 6497 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ((1 /
(normℎ‘𝐴)) ·ℎ 𝐴) →
(normℎ‘𝑦) = (normℎ‘((1 /
(normℎ‘𝐴)) ·ℎ 𝐴))) |
83 | 82 | breq1d 4936 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ((1 /
(normℎ‘𝐴)) ·ℎ 𝐴) →
((normℎ‘𝑦) ≤ 1 ↔
(normℎ‘((1 / (normℎ‘𝐴))
·ℎ 𝐴)) ≤ 1)) |
84 | | fvoveq1 6998 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ((1 /
(normℎ‘𝐴)) ·ℎ 𝐴) → (abs‘(𝑦
·ih 𝐴)) = (abs‘(((1 /
(normℎ‘𝐴)) ·ℎ 𝐴)
·ih 𝐴))) |
85 | 84 | eqeq2d 2783 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ((1 /
(normℎ‘𝐴)) ·ℎ 𝐴) →
((normℎ‘𝐴) = (abs‘(𝑦 ·ih 𝐴)) ↔
(normℎ‘𝐴) = (abs‘(((1 /
(normℎ‘𝐴)) ·ℎ 𝐴)
·ih 𝐴)))) |
86 | 83, 85 | anbi12d 622 |
. . . . . . . . . . . 12
⊢ (𝑦 = ((1 /
(normℎ‘𝐴)) ·ℎ 𝐴) →
(((normℎ‘𝑦) ≤ 1 ∧
(normℎ‘𝐴) = (abs‘(𝑦 ·ih 𝐴))) ↔
((normℎ‘((1 / (normℎ‘𝐴))
·ℎ 𝐴)) ≤ 1 ∧
(normℎ‘𝐴) = (abs‘(((1 /
(normℎ‘𝐴)) ·ℎ 𝐴)
·ih 𝐴))))) |
87 | 86 | rspcev 3530 |
. . . . . . . . . . 11
⊢ ((((1 /
(normℎ‘𝐴)) ·ℎ 𝐴) ∈ ℋ ∧
((normℎ‘((1 / (normℎ‘𝐴))
·ℎ 𝐴)) ≤ 1 ∧
(normℎ‘𝐴) = (abs‘(((1 /
(normℎ‘𝐴)) ·ℎ 𝐴)
·ih 𝐴)))) → ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧
(normℎ‘𝐴) = (abs‘(𝑦 ·ih 𝐴)))) |
88 | 45, 48, 81, 87 | syl12anc 825 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ∃𝑦 ∈
ℋ ((normℎ‘𝑦) ≤ 1 ∧
(normℎ‘𝐴) = (abs‘(𝑦 ·ih 𝐴)))) |
89 | 23 | eqeq2d 2783 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
((normℎ‘𝐴) = (abs‘((bra‘𝐴)‘𝑦)) ↔
(normℎ‘𝐴) = (abs‘(𝑦 ·ih 𝐴)))) |
90 | 89 | anbi2d 620 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(((normℎ‘𝑦) ≤ 1 ∧
(normℎ‘𝐴) = (abs‘((bra‘𝐴)‘𝑦))) ↔
((normℎ‘𝑦) ≤ 1 ∧
(normℎ‘𝐴) = (abs‘(𝑦 ·ih 𝐴))))) |
91 | 90 | rexbidva 3236 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℋ →
(∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧
(normℎ‘𝐴) = (abs‘((bra‘𝐴)‘𝑦))) ↔ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧
(normℎ‘𝐴) = (abs‘(𝑦 ·ih 𝐴))))) |
92 | 91 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (∃𝑦 ∈
ℋ ((normℎ‘𝑦) ≤ 1 ∧
(normℎ‘𝐴) = (abs‘((bra‘𝐴)‘𝑦))) ↔ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧
(normℎ‘𝐴) = (abs‘(𝑦 ·ih 𝐴))))) |
93 | 88, 92 | mpbird 249 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ∃𝑦 ∈
ℋ ((normℎ‘𝑦) ≤ 1 ∧
(normℎ‘𝐴) = (abs‘((bra‘𝐴)‘𝑦)))) |
94 | | fvex 6510 |
. . . . . . . . . 10
⊢
(normℎ‘𝐴) ∈ V |
95 | | eqeq1 2777 |
. . . . . . . . . . . 12
⊢ (𝑥 =
(normℎ‘𝐴) → (𝑥 = (abs‘((bra‘𝐴)‘𝑦)) ↔
(normℎ‘𝐴) = (abs‘((bra‘𝐴)‘𝑦)))) |
96 | 95 | anbi2d 620 |
. . . . . . . . . . 11
⊢ (𝑥 =
(normℎ‘𝐴) →
(((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦))) ↔
((normℎ‘𝑦) ≤ 1 ∧
(normℎ‘𝐴) = (abs‘((bra‘𝐴)‘𝑦))))) |
97 | 96 | rexbidv 3237 |
. . . . . . . . . 10
⊢ (𝑥 =
(normℎ‘𝐴) → (∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦))) ↔ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧
(normℎ‘𝐴) = (abs‘((bra‘𝐴)‘𝑦))))) |
98 | 94, 97 | elab 3577 |
. . . . . . . . 9
⊢
((normℎ‘𝐴) ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))} ↔ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧
(normℎ‘𝐴) = (abs‘((bra‘𝐴)‘𝑦)))) |
99 | 93, 98 | sylibr 226 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘𝐴) ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))}) |
100 | | breq2 4930 |
. . . . . . . . 9
⊢ (𝑤 =
(normℎ‘𝐴) → (𝑧 < 𝑤 ↔ 𝑧 < (normℎ‘𝐴))) |
101 | 100 | rspcev 3530 |
. . . . . . . 8
⊢
(((normℎ‘𝐴) ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))} ∧ 𝑧 < (normℎ‘𝐴)) → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))}𝑧 < 𝑤) |
102 | 99, 101 | sylan 572 |
. . . . . . 7
⊢ (((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑧 <
(normℎ‘𝐴)) → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))}𝑧 < 𝑤) |
103 | 102 | adantlr 703 |
. . . . . 6
⊢ ((((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑧 ∈ ℝ)
∧ 𝑧 <
(normℎ‘𝐴)) → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))}𝑧 < 𝑤) |
104 | 103 | ex 405 |
. . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑧 ∈ ℝ)
→ (𝑧 <
(normℎ‘𝐴) → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))}𝑧 < 𝑤)) |
105 | 104 | ralrimiva 3127 |
. . . 4
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ∀𝑧 ∈
ℝ (𝑧 <
(normℎ‘𝐴) → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))}𝑧 < 𝑤)) |
106 | | supxr2 12522 |
. . . 4
⊢ ((({𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))} ⊆ ℝ* ∧
(normℎ‘𝐴) ∈ ℝ*) ∧
(∀𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))}𝑧 ≤ (normℎ‘𝐴) ∧ ∀𝑧 ∈ ℝ (𝑧 <
(normℎ‘𝐴) → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))}𝑧 < 𝑤))) → sup({𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))}, ℝ*, < ) =
(normℎ‘𝐴)) |
107 | 15, 37, 105, 106 | syl12anc 825 |
. . 3
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ sup({𝑥 ∣
∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘((bra‘𝐴)‘𝑦)))}, ℝ*, < ) =
(normℎ‘𝐴)) |
108 | 7, 107 | eqtrd 2809 |
. 2
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normfn‘(bra‘𝐴)) = (normℎ‘𝐴)) |
109 | | nmfn0 29561 |
. . . 4
⊢
(normfn‘( ℋ × {0})) = 0 |
110 | | bra0 29524 |
. . . . 5
⊢
(bra‘0ℎ) = ( ℋ ×
{0}) |
111 | 110 | fveq2i 6500 |
. . . 4
⊢
(normfn‘(bra‘0ℎ)) =
(normfn‘( ℋ × {0})) |
112 | | norm0 28700 |
. . . 4
⊢
(normℎ‘0ℎ) =
0 |
113 | 109, 111,
112 | 3eqtr4i 2807 |
. . 3
⊢
(normfn‘(bra‘0ℎ)) =
(normℎ‘0ℎ) |
114 | 113 | a1i 11 |
. 2
⊢ (𝐴 ∈ ℋ →
(normfn‘(bra‘0ℎ)) =
(normℎ‘0ℎ)) |
115 | 3, 108, 114 | pm2.61ne 3048 |
1
⊢ (𝐴 ∈ ℋ →
(normfn‘(bra‘𝐴)) = (normℎ‘𝐴)) |