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∈ℋ→normfn⁡bra⁡A=normℎ⁡A

Proof

Step Hyp Ref Expression
1 2fveq3 ⊢A=0ℎ→normfn⁡bra⁡A=normfn⁡bra⁡0ℎ
2 fveq2 ⊢A=0ℎ→normℎ⁡A=normℎ⁡0ℎ
3 1 2 eqeq12d ⊢A=0ℎ→normfn⁡bra⁡A=normℎ⁡A↔normfn⁡bra⁡0ℎ=normℎ⁡0ℎ
4 brafn ⊢A∈ℋ→bra⁡A:ℋ⟶ℂ
5 nmfnval ⊢bra⁡A:ℋ⟶ℂ→normfn⁡bra⁡A=supx|∃y∈ℋnormℎ⁡y≤1∧x=bra⁡A⁡yℝ*<
6 4 5 syl ⊢A∈ℋ→normfn⁡bra⁡A=supx|∃y∈ℋnormℎ⁡y≤1∧x=bra⁡A⁡yℝ*<
7 6 adantr ⊢A∈ℋ∧A≠0ℎ→normfn⁡bra⁡A=supx|∃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⋅ihA
23 22 fveq2d ⊢A∈ℋ∧y∈ℋ→bra⁡A⁡y=y⋅ihA
24 23 adantr ⊢A∈ℋ∧y∈ℋ∧normℎ⁡y≤1→bra⁡A⁡y=y⋅ihA
25 21 24 sylan9eqr ⊢A∈ℋ∧y∈ℋ∧normℎ⁡y≤1∧z=bra⁡A⁡y→z=y⋅ihA
26 bcs2 ⊢y∈ℋ∧A∈ℋ∧normℎ⁡y≤1→y⋅ihA≤normℎ⁡A
27 26 3expa ⊢y∈ℋ∧A∈ℋ∧normℎ⁡y≤1→y⋅ihA≤normℎ⁡A
28 27 ancom1s ⊢A∈ℋ∧y∈ℋ∧normℎ⁡y≤1→y⋅ihA≤normℎ⁡A
29 28 adantr ⊢A∈ℋ∧y∈ℋ∧normℎ⁡y≤1∧z=bra⁡A⁡y→y⋅ihA≤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⁡yz≤normℎ⁡A
37 36 adantr ⊢A∈ℋ∧A≠0ℎ→∀z∈x|∃y∈ℋnormℎ⁡y≤1∧x=bra⁡A⁡yz≤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ℎ→1normℎ⁡A∈ℂ
43 simpl ⊢A∈ℋ∧A≠0ℎ→A∈ℋ
44 hvmulcl ⊢1normℎ⁡A∈ℂ∧A∈ℋ→1normℎ⁡A⋅ℎA∈ℋ
45 42 43 44 syl2anc ⊢A∈ℋ∧A≠0ℎ→1normℎ⁡A⋅ℎA∈ℋ
46 norm1 ⊢A∈ℋ∧A≠0ℎ→normℎ⁡1normℎ⁡A⋅ℎA=1
47 1le1 ⊢1≤1
48 46 47 eqbrtrdi ⊢A∈ℋ∧A≠0ℎ→normℎ⁡1normℎ⁡A⋅ℎA≤1
49 ax-his3 ⊢1normℎ⁡A∈ℂ∧A∈ℋ∧A∈ℋ→1normℎ⁡A⋅ℎA⋅ihA=1normℎ⁡A⁢A⋅ihA
50 42 43 43 49 syl3anc ⊢A∈ℋ∧A≠0ℎ→1normℎ⁡A⋅ℎA⋅ihA=1normℎ⁡A⁢A⋅ihA
51 12 adantr ⊢A∈ℋ∧A≠0ℎ→normℎ⁡A∈ℝ
52 51 41 rereccld ⊢A∈ℋ∧A≠0ℎ→1normℎ⁡A∈ℝ
53 hiidrcl ⊢A∈ℋ→A⋅ihA∈ℝ
54 53 adantr ⊢A∈ℋ∧A≠0ℎ→A⋅ihA∈ℝ
55 52 54 remulcld ⊢A∈ℋ∧A≠0ℎ→1normℎ⁡A⁢A⋅ihA∈ℝ
56 50 55 eqeltrd ⊢A∈ℋ∧A≠0ℎ→1normℎ⁡A⋅ℎA⋅ihA∈ℝ
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<1normℎ⁡A
60 0re ⊢0∈ℝ
61 ltle ⊢0∈ℝ∧1normℎ⁡A∈ℝ→0<1normℎ⁡A→0≤1normℎ⁡A
62 60 61 mpan ⊢1normℎ⁡A∈ℝ→0<1normℎ⁡A→0≤1normℎ⁡A
63 52 59 62 sylc ⊢A∈ℋ∧A≠0ℎ→0≤1normℎ⁡A
64 hiidge0 ⊢A∈ℋ→0≤A⋅ihA
65 64 adantr ⊢A∈ℋ∧A≠0ℎ→0≤A⋅ihA
66 52 54 63 65 mulge0d ⊢A∈ℋ∧A≠0ℎ→0≤1normℎ⁡A⁢A⋅ihA
67 66 50 breqtrrd ⊢A∈ℋ∧A≠0ℎ→0≤1normℎ⁡A⋅ℎA⋅ihA
68 56 67 absidd ⊢A∈ℋ∧A≠0ℎ→1normℎ⁡A⋅ℎA⋅ihA=1normℎ⁡A⋅ℎA⋅ihA
69 39 41 recid2d ⊢A∈ℋ∧A≠0ℎ→1normℎ⁡A⁢normℎ⁡A=1
70 69 oveq2d ⊢A∈ℋ∧A≠0ℎ→normℎ⁡A⁢1normℎ⁡A⁢normℎ⁡A=normℎ⁡A⋅1
71 39 42 39 mul12d ⊢A∈ℋ∧A≠0ℎ→normℎ⁡A⁢1normℎ⁡A⁢normℎ⁡A=1normℎ⁡A⁢normℎ⁡A⁢normℎ⁡A
72 38 sqvald ⊢A∈ℋ→normℎ⁡A2=normℎ⁡A⁢normℎ⁡A
73 normsq ⊢A∈ℋ→normℎ⁡A2=A⋅ihA
74 72 73 eqtr3d ⊢A∈ℋ→normℎ⁡A⁢normℎ⁡A=A⋅ihA
75 74 adantr ⊢A∈ℋ∧A≠0ℎ→normℎ⁡A⁢normℎ⁡A=A⋅ihA
76 75 oveq2d ⊢A∈ℋ∧A≠0ℎ→1normℎ⁡A⁢normℎ⁡A⁢normℎ⁡A=1normℎ⁡A⁢A⋅ihA
77 71 76 eqtrd ⊢A∈ℋ∧A≠0ℎ→normℎ⁡A⁢1normℎ⁡A⁢normℎ⁡A=1normℎ⁡A⁢A⋅ihA
78 38 mulridd ⊢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=1normℎ⁡A⁢A⋅ihA
81 50 68 80 3eqtr4rd ⊢A∈ℋ∧A≠0ℎ→normℎ⁡A=1normℎ⁡A⋅ℎA⋅ihA
82 fveq2 ⊢y=1normℎ⁡A⋅ℎA→normℎ⁡y=normℎ⁡1normℎ⁡A⋅ℎA
83 82 breq1d ⊢y=1normℎ⁡A⋅ℎA→normℎ⁡y≤1↔normℎ⁡1normℎ⁡A⋅ℎA≤1
84 fvoveq1 ⊢y=1normℎ⁡A⋅ℎA→y⋅ihA=1normℎ⁡A⋅ℎA⋅ihA
85 84 eqeq2d ⊢y=1normℎ⁡A⋅ℎA→normℎ⁡A=y⋅ihA↔normℎ⁡A=1normℎ⁡A⋅ℎA⋅ihA
86 83 85 anbi12d ⊢y=1normℎ⁡A⋅ℎA→normℎ⁡y≤1∧normℎ⁡A=y⋅ihA↔normℎ⁡1normℎ⁡A⋅ℎA≤1∧normℎ⁡A=1normℎ⁡A⋅ℎA⋅ihA
87 86 rspcev ⊢1normℎ⁡A⋅ℎA∈ℋ∧normℎ⁡1normℎ⁡A⋅ℎA≤1∧normℎ⁡A=1normℎ⁡A⋅ℎA⋅ihA→∃y∈ℋnormℎ⁡y≤1∧normℎ⁡A=y⋅ihA
88 45 48 81 87 syl12anc ⊢A∈ℋ∧A≠0ℎ→∃y∈ℋnormℎ⁡y≤1∧normℎ⁡A=y⋅ihA
89 23 eqeq2d ⊢A∈ℋ∧y∈ℋ→normℎ⁡A=bra⁡A⁡y↔normℎ⁡A=y⋅ihA
90 89 anbi2d ⊢A∈ℋ∧y∈ℋ→normℎ⁡y≤1∧normℎ⁡A=bra⁡A⁡y↔normℎ⁡y≤1∧normℎ⁡A=y⋅ihA
91 90 rexbidva ⊢A∈ℋ→∃y∈ℋnormℎ⁡y≤1∧normℎ⁡A=bra⁡A⁡y↔∃y∈ℋnormℎ⁡y≤1∧normℎ⁡A=y⋅ihA
92 91 adantr ⊢A∈ℋ∧A≠0ℎ→∃y∈ℋnormℎ⁡y≤1∧normℎ⁡A=bra⁡A⁡y↔∃y∈ℋnormℎ⁡y≤1∧normℎ⁡A=y⋅ihA
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⁡yz<w
100 97 99 sylan ⊢A∈ℋ∧A≠0ℎ∧z<normℎ⁡A→∃w∈x|∃y∈ℋnormℎ⁡y≤1∧x=bra⁡A⁡yz<w
101 100 adantlr ⊢A∈ℋ∧A≠0ℎ∧z∈ℝ∧z<normℎ⁡A→∃w∈x|∃y∈ℋnormℎ⁡y≤1∧x=bra⁡A⁡yz<w
102 101 ex ⊢A∈ℋ∧A≠0ℎ∧z∈ℝ→z<normℎ⁡A→∃w∈x|∃y∈ℋnormℎ⁡y≤1∧x=bra⁡A⁡yz<w
103 102 ralrimiva ⊢A∈ℋ∧A≠0ℎ→∀z∈ℝz<normℎ⁡A→∃w∈x|∃y∈ℋnormℎ⁡y≤1∧x=bra⁡A⁡yz<w
104 supxr2 ⊢x|∃y∈ℋnormℎ⁡y≤1∧x=bra⁡A⁡y⊆ℝ*∧normℎ⁡A∈ℝ*∧∀z∈x|∃y∈ℋnormℎ⁡y≤1∧x=bra⁡A⁡yz≤normℎ⁡A∧∀z∈ℝz<normℎ⁡A→∃w∈x|∃y∈ℋnormℎ⁡y≤1∧x=bra⁡A⁡yz<w→supx|∃y∈ℋnormℎ⁡y≤1∧x=bra⁡A⁡yℝ*<=normℎ⁡A
105 15 37 103 104 syl12anc ⊢A∈ℋ∧A≠0ℎ→supx|∃y∈ℋnormℎ⁡y≤1∧x=bra⁡A⁡yℝ*<=normℎ⁡A
106 7 105 eqtrd ⊢A∈ℋ∧A≠0ℎ→normfn⁡bra⁡A=normℎ⁡A
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 ⊢A∈ℋ→normfn⁡bra⁡0ℎ=normℎ⁡0ℎ
113 3 106 112 pm2.61ne ⊢A∈ℋ→normfn⁡bra⁡A=normℎ⁡A