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	mulridd	⊢ ( 𝐴 ∈ ℋ → ( ( 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ℎ ‘ 𝐴 ) )