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 ( 𝐴 ∈ ℋ → ( normfn ‘ ( bra ‘ 𝐴 ) ) = ( normℎ ‘ 𝐴 ) )

Proof

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