Theorem branmfnt 9951

Description: The norm of the bra function.

Assertion

Ref	Expression
branmfnt	|- (A e. H~ -> (normfn` (bra` A)) = (normh` A))

Proof of Theorem branmfnt

Step	Hyp	Ref	Expression
1		fveq2 3709	. . . 4 |- (A = 0h -> (bra` A) = (bra` 0h))
2	1	fveq2d 3713	. . 3 |- (A = 0h -> (normfn` (bra` A)) = (normfn` (bra` 0h)))
3		fveq2 3709	. . 3 |- (A = 0h -> (normh` A) = (normh` 0h))
4	2, 3	eqeq12d 1481	. 2 |- (A = 0h -> ((normfn` (bra` A)) = (normh` A) <-> (normfn` (bra` 0h)) = (normh` 0h)))
5		brafnt 9787	. . . . 5 |- (A e. H~ -> (bra` A):H~-->CC)
6		nmfnvalt 9720	. . . . 5 |- ((bra` A):H~-->CC -> (normfn` (bra` A)) = sup({x | E.y e. H~ ((normh` y) <_ 1 /\ x = (abs` ((bra` A)` y)))}, RR*, < ))
7	5, 6	syl 10	. . . 4 |- (A e. H~ -> (normfn` (bra` A)) = sup({x | E.y e. H~ ((normh` y) <_ 1 /\ x = (abs` ((bra` A)` y)))}, RR*, < ))
8	7	adantr 389	. . 3 |- ((A e. H~ /\ A =/= 0h) -> (normfn` (bra` A)) = sup({x | E.y e. H~ ((normh` y) <_ 1 /\ x = (abs` ((bra` A)` y)))}, RR*, < ))
9		supxr2 6029	. . . 4 |- ((({x | E.y e. H~ ((normh` y) <_ 1 /\ x = (abs` ((bra` A)` y)))} (_ 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))
10		nmfnsetret 9721	. . . . . . . 8 |- ((bra` A):H~-->CC -> {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (abs` ((bra` A)` y)))} (_ RR)
11	5, 10	syl 10	. . . . . . 7 |- (A e. H~ -> {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (abs` ((bra` A)` y)))} (_ RR)
12		ressxr 5470	. . . . . . . 8 |- RR (_ RR*
13	12	a1i 8	. . . . . . 7 |- (A e. H~ -> RR (_ RR*)
14	11, 13	sstrd 2064	. . . . . 6 |- (A e. H~ -> {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (abs` ((bra` A)` y)))} (_ RR*)
15		normclt 8912	. . . . . . 7 |- (A e. H~ -> (normh` A) e. RR)
16		rexrt 5471	. . . . . . 7 |- ((normh` A) e. RR -> (normh` A) e. RR*)
17	15, 16	syl 10	. . . . . 6 |- (A e. H~ -> (normh` A) e. RR*)
18	14, 17	jca 288	. . . . 5 |- (A e. H~ -> ({x | E.y e. H~ ((normh` y) <_ 1 /\ x = (abs` ((bra` A)` y)))} (_ RR* /\ (normh` A) e. RR*))
19	18	adantr 389	. . . 4 |- ((A e. H~ /\ A =/= 0h) -> ({x | E.y e. H~ ((normh` y) <_ 1 /\ x = (abs` ((bra` A)` y)))} (_ RR* /\ (normh` A) e. RR*))
20		id 59	. . . . . . . . . . . . . 14 |- (z = (abs` ((bra` A)` y)) -> z = (abs` ((bra` A)` y)))
21		bravalvalt 9784	. . . . . . . . . . . . . . . 16 |- ((A e. H~ /\ y e. H~) -> ((bra` A)` y) = (y .ih A))
22	21	fveq2d 3713	. . . . . . . . . . . . . . 15 |- ((A e. H~ /\ y e. H~) -> (abs` ((bra` A)` y)) = (abs` (y .ih A)))
23	22	adantr 389	. . . . . . . . . . . . . 14 |- (((A e. H~ /\ y e. H~) /\ (normh` y) <_ 1) -> (abs` ((bra` A)` y)) = (abs` (y .ih A)))
24	20, 23	sylan9eqr 1521	. . . . . . . . . . . . 13 |- ((((A e. H~ /\ y e. H~) /\ (normh` y) <_ 1) /\ z = (abs` ((bra` A)` y))) -> z = (abs` (y .ih A)))
25		bcs2t 8970	. . . . . . . . . . . . . . . 16 |- ((y e. H~ /\ A e. H~ /\ (normh` y) <_ 1) -> (abs` (y .ih A)) <_ (normh` A))
26	25	3expa 831	. . . . . . . . . . . . . . 15 |- (((y e. H~ /\ A e. H~) /\ (normh` y) <_ 1) -> (abs` (y .ih A)) <_ (normh` A))
27	26	ancom1s 489	. . . . . . . . . . . . . 14 |- (((A e. H~ /\ y e. H~) /\ (normh` y) <_ 1) -> (abs` (y .ih A)) <_ (normh` A))
28	27	adantr 389	. . . . . . . . . . . . 13 |- ((((A e. H~ /\ y e. H~) /\ (normh` y) <_ 1) /\ z = (abs` ((bra` A)` y))) -> (abs` (y .ih A)) <_ (normh` A))
29	24, 28	eqbrtrd 2625	. . . . . . . . . . . 12 |- ((((A e. H~ /\ y e. H~) /\ (normh` y) <_ 1) /\ z = (abs` ((bra` A)` y))) -> z <_ (normh` A))
30	29	exp41 382	. . . . . . . . . . 11 |- (A e. H~ -> (y e. H~ -> ((normh` y) <_ 1 -> (z = (abs` ((bra` A)` y)) -> z <_ (normh` A)))))
31	30	imp4a 364	. . . . . . . . . 10 |- (A e. H~ -> (y e. H~ -> (((normh` y) <_ 1 /\ z = (abs` ((bra` A)` y))) -> z <_ (normh` A))))
32	31	r19.23adv 1738	. . . . . . . . 9 |- (A e. H~ -> (E.y e. H~ ((normh` y) <_ 1 /\ z = (abs` ((bra` A)` y))) -> z <_ (normh` A)))
33	32	imp 350	. . . . . . . 8 |- ((A e. H~ /\ E.y e. H~ ((normh` y) <_ 1 /\ z = (abs` ((bra` A)` y)))) -> z <_ (normh` A))
34		visset 1804	. . . . . . . . 9 |- z e. V
35		eqeq1 1473	. . . . . . . . . . 11 |- (x = z -> (x = (abs` ((bra` A)` y)) <-> z = (abs` ((bra` A)` y))))
36	35	anbi2d 614	. . . . . . . . . 10 |- (x = z -> (((normh` y) <_ 1 /\ x = (abs` ((bra` A)` y))) <-> ((normh` y) <_ 1 /\ z = (abs` ((bra` A)` y)))))
37	36	rexbidv 1656	. . . . . . . . 9 |- (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)))))
38	34, 37	elab 1888	. . . . . . . 8 |- (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))))
39	33, 38	sylan2b 452	. . . . . . 7 |- ((A e. H~ /\ z e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (abs` ((bra` A)` y)))}) -> z <_ (normh` A))
40	39	r19.21aiva 1706	. . . . . 6 |- (A e. H~ -> A.z e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (abs` ((bra` A)` y)))}z <_ (normh` A))
41	40	adantr 389	. . . . 5 |- ((A e. H~ /\ A =/= 0h) -> A.z e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (abs` ((bra` A)` y)))}z <_ (normh` A))
42		breq2 2613	. . . . . . . . . 10 |- (w = (normh` A) -> (z < w <-> z < (normh` A)))
43	42	rcla4ev 1868	. . . . . . . . 9 |- (((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)
44		fveq2 3709	. . . . . . . . . . . . . . 15 |- (y = ((1 / (normh` A)) .h A) -> (normh` y) = (normh` ((1 / (normh` A)) .h A)))
45	44	breq1d 2619	. . . . . . . . . . . . . 14 |- (y = ((1 / (normh` A)) .h A) -> ((normh` y) <_ 1 <-> (normh` ((1 / (normh` A)) .h A)) <_ 1))
46		opreq1 3953	. . . . . . . . . . . . . . . 16 |- (y = ((1 / (normh` A)) .h A) -> (y .ih A) = (((1 / (normh` A)) .h A) .ih A))
47	46	fveq2d 3713	. . . . . . . . . . . . . . 15 |- (y = ((1 / (normh` A)) .h A) -> (abs` (y .ih A)) = (abs` (((1 /