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 e. ~H -> ( normfn ` ( bra ` A ) ) = ( normh ` A ) )

Proof

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