nmophmi

Description: The norm of the scalar product of a bounded linear operator. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	nmophm.1	$⊢ T \in BndLinOp$
	Assertion	nmophmi	$⊢ A \in ℂ \to {norm}_{op} (A \cdot_{op} T) = \|A\| {norm}_{op} (T)$

Proof

Step	Hyp	Ref	Expression
1		nmophm.1	$⊢ T \in BndLinOp$
2		bdopf	$⊢ T \in BndLinOp \to T : ℋ ⟶ ℋ$
3	1 2	ax-mp	$⊢ T : ℋ ⟶ ℋ$
4		homval	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land x \in ℋ) \to (A \cdot_{op} T) (x) = A \cdot_{ℎ} T (x)$
5	3 4	mp3an2	$⊢ (A \in ℂ \land x \in ℋ) \to (A \cdot_{op} T) (x) = A \cdot_{ℎ} T (x)$
6	5	fveq2d	$⊢ (A \in ℂ \land x \in ℋ) \to {norm}_{ℎ} ((A \cdot_{op} T) (x)) = {norm}_{ℎ} (A \cdot_{ℎ} T (x))$
7	3	ffvelrni	$⊢ x \in ℋ \to T (x) \in ℋ$
8		norm-iii	$⊢ (A \in ℂ \land T (x) \in ℋ) \to {norm}_{ℎ} (A \cdot_{ℎ} T (x)) = \|A\| {norm}_{ℎ} (T (x))$
9	7 8	sylan2	$⊢ (A \in ℂ \land x \in ℋ) \to {norm}_{ℎ} (A \cdot_{ℎ} T (x)) = \|A\| {norm}_{ℎ} (T (x))$
10	6 9	eqtrd	$⊢ (A \in ℂ \land x \in ℋ) \to {norm}_{ℎ} ((A \cdot_{op} T) (x)) = \|A\| {norm}_{ℎ} (T (x))$
11	10	adantr	$⊢ ((A \in ℂ \land x \in ℋ) \land {norm}_{ℎ} (x) \leq 1) \to {norm}_{ℎ} ((A \cdot_{op} T) (x)) = \|A\| {norm}_{ℎ} (T (x))$
12		normcl	$⊢ T (x) \in ℋ \to {norm}_{ℎ} (T (x)) \in ℝ$
13	7 12	syl	$⊢ x \in ℋ \to {norm}_{ℎ} (T (x)) \in ℝ$
14	13	ad2antlr	$⊢ ((A \in ℂ \land x \in ℋ) \land {norm}_{ℎ} (x) \leq 1) \to {norm}_{ℎ} (T (x)) \in ℝ$
15		abscl	$⊢ A \in ℂ \to \|A\| \in ℝ$
16		absge0	$⊢ A \in ℂ \to 0 \leq \|A\|$
17	15 16	jca	$⊢ A \in ℂ \to (\|A\| \in ℝ \land 0 \leq \|A\|)$
18	17	ad2antrr	$⊢ ((A \in ℂ \land x \in ℋ) \land {norm}_{ℎ} (x) \leq 1) \to (\|A\| \in ℝ \land 0 \leq \|A\|)$
19		nmoplb	$⊢ (T : ℋ ⟶ ℋ \land x \in ℋ \land {norm}_{ℎ} (x) \leq 1) \to {norm}_{ℎ} (T (x)) \leq {norm}_{op} (T)$
20	3 19	mp3an1	$⊢ (x \in ℋ \land {norm}_{ℎ} (x) \leq 1) \to {norm}_{ℎ} (T (x)) \leq {norm}_{op} (T)$
21	20	adantll	$⊢ ((A \in ℂ \land x \in ℋ) \land {norm}_{ℎ} (x) \leq 1) \to {norm}_{ℎ} (T (x)) \leq {norm}_{op} (T)$
22		nmopre	$⊢ T \in BndLinOp \to {norm}_{op} (T) \in ℝ$
23	1 22	ax-mp	$⊢ {norm}_{op} (T) \in ℝ$
24		lemul2a	$⊢ (({norm}_{ℎ} (T (x)) \in ℝ \land {norm}_{op} (T) \in ℝ \land (\|A\| \in ℝ \land 0 \leq \|A\|)) \land {norm}_{ℎ} (T (x)) \leq {norm}_{op} (T)) \to \|A\| {norm}_{ℎ} (T (x)) \leq \|A\| {norm}_{op} (T)$
25	23 24	mp3anl2	$⊢ (({norm}_{ℎ} (T (x)) \in ℝ \land (\|A\| \in ℝ \land 0 \leq \|A\|)) \land {norm}_{ℎ} (T (x)) \leq {norm}_{op} (T)) \to \|A\| {norm}_{ℎ} (T (x)) \leq \|A\| {norm}_{op} (T)$
26	14 18 21 25	syl21anc	$⊢ ((A \in ℂ \land x \in ℋ) \land {norm}_{ℎ} (x) \leq 1) \to \|A\| {norm}_{ℎ} (T (x)) \leq \|A\| {norm}_{op} (T)$
27	11 26	eqbrtrd	$⊢ ((A \in ℂ \land x \in ℋ) \land {norm}_{ℎ} (x) \leq 1) \to {norm}_{ℎ} ((A \cdot_{op} T) (x)) \leq \|A\| {norm}_{op} (T)$
28	27	ex	$⊢ (A \in ℂ \land x \in ℋ) \to ({norm}_{ℎ} (x) \leq 1 \to {norm}_{ℎ} ((A \cdot_{op} T) (x)) \leq \|A\| {norm}_{op} (T))$
29	28	ralrimiva	$⊢ A \in ℂ \to \forall x \in ℋ ({norm}_{ℎ} (x) \leq 1 \to {norm}_{ℎ} ((A \cdot_{op} T) (x)) \leq \|A\| {norm}_{op} (T))$
30		homulcl	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ) \to (A \cdot_{op} T) : ℋ ⟶ ℋ$
31	3 30	mpan2	$⊢ A \in ℂ \to (A \cdot_{op} T) : ℋ ⟶ ℋ$
32		remulcl	$⊢ (\|A\| \in ℝ \land {norm}_{op} (T) \in ℝ) \to \|A\| {norm}_{op} (T) \in ℝ$
33	15 23 32	sylancl	$⊢ A \in ℂ \to \|A\| {norm}_{op} (T) \in ℝ$
34	33	rexrd	$⊢ A \in ℂ \to \|A\| {norm}_{op} (T) \in ℝ^{*}$
35		nmopub	$⊢ ((A \cdot_{op} T) : ℋ ⟶ ℋ \land \|A\| {norm}_{op} (T) \in ℝ^{*}) \to ({norm}_{op} (A \cdot_{op} T) \leq \|A\| {norm}_{op} (T) \leftrightarrow \forall x \in ℋ ({norm}_{ℎ} (x) \leq 1 \to {norm}_{ℎ} ((A \cdot_{op} T) (x)) \leq \|A\| {norm}_{op} (T)))$
36	31 34 35	syl2anc	$⊢ A \in ℂ \to ({norm}_{op} (A \cdot_{op} T) \leq \|A\| {norm}_{op} (T) \leftrightarrow \forall x \in ℋ ({norm}_{ℎ} (x) \leq 1 \to {norm}_{ℎ} ((A \cdot_{op} T) (x)) \leq \|A\| {norm}_{op} (T)))$
37	29 36	mpbird	$⊢ A \in ℂ \to {norm}_{op} (A \cdot_{op} T) \leq \|A\| {norm}_{op} (T)$
38		fveq2	$⊢ A = 0 \to \|A\| = \|0\|$
39		abs0	$⊢ \|0\| = 0$
40	38 39	eqtrdi	$⊢ A = 0 \to \|A\| = 0$
41	40	oveq1d	$⊢ A = 0 \to \|A\| {norm}_{op} (T) = 0 \cdot {norm}_{op} (T)$
42	23	recni	$⊢ {norm}_{op} (T) \in ℂ$
43	42	mul02i	$⊢ 0 \cdot {norm}_{op} (T) = 0$
44	41 43	eqtrdi	$⊢ A = 0 \to \|A\| {norm}_{op} (T) = 0$
45	44	adantl	$⊢ (A \in ℂ \land A = 0) \to \|A\| {norm}_{op} (T) = 0$
46		nmopge0	$⊢ (A \cdot_{op} T) : ℋ ⟶ ℋ \to 0 \leq {norm}_{op} (A \cdot_{op} T)$
47	31 46	syl	$⊢ A \in ℂ \to 0 \leq {norm}_{op} (A \cdot_{op} T)$
48	47	adantr	$⊢ (A \in ℂ \land A = 0) \to 0 \leq {norm}_{op} (A \cdot_{op} T)$
49	45 48	eqbrtrd	$⊢ (A \in ℂ \land A = 0) \to \|A\| {norm}_{op} (T) \leq {norm}_{op} (A \cdot_{op} T)$
50		nmoplb	$⊢ ((A \cdot_{op} T) : ℋ ⟶ ℋ \land x \in ℋ \land {norm}_{ℎ} (x) \leq 1) \to {norm}_{ℎ} ((A \cdot_{op} T) (x)) \leq {norm}_{op} (A \cdot_{op} T)$
51	31 50	syl3an1	$⊢ (A \in ℂ \land x \in ℋ \land {norm}_{ℎ} (x) \leq 1) \to {norm}_{ℎ} ((A \cdot_{op} T) (x)) \leq {norm}_{op} (A \cdot_{op} T)$
52	51	3expa	$⊢ ((A \in ℂ \land x \in ℋ) \land {norm}_{ℎ} (x) \leq 1) \to {norm}_{ℎ} ((A \cdot_{op} T) (x)) \leq {norm}_{op} (A \cdot_{op} T)$
53	11 52	eqbrtrrd	$⊢ ((A \in ℂ \land x \in ℋ) \land {norm}_{ℎ} (x) \leq 1) \to \|A\| {norm}_{ℎ} (T (x)) \leq {norm}_{op} (A \cdot_{op} T)$
54	53	adantllr	$⊢ (((A \in ℂ \land A \neq 0) \land x \in ℋ) \land {norm}_{ℎ} (x) \leq 1) \to \|A\| {norm}_{ℎ} (T (x)) \leq {norm}_{op} (A \cdot_{op} T)$
55	13	adantl	$⊢ ((A \in ℂ \land A \neq 0) \land x \in ℋ) \to {norm}_{ℎ} (T (x)) \in ℝ$
56		nmopxr	$⊢ (A \cdot_{op} T) : ℋ ⟶ ℋ \to {norm}_{op} (A \cdot_{op} T) \in ℝ^{*}$
57	31 56	syl	$⊢ A \in ℂ \to {norm}_{op} (A \cdot_{op} T) \in ℝ^{*}$
58		nmopgtmnf	$⊢ (A \cdot_{op} T) : ℋ ⟶ ℋ \to −∞ < {norm}_{op} (A \cdot_{op} T)$
59	31 58	syl	$⊢ A \in ℂ \to −∞ < {norm}_{op} (A \cdot_{op} T)$
60		xrre	$⊢ (({norm}_{op} (A \cdot_{op} T) \in ℝ^{*} \land \|A\| {norm}_{op} (T) \in ℝ) \land (−∞ < {norm}_{op} (A \cdot_{op} T) \land {norm}_{op} (A \cdot_{op} T) \leq \|A\| {norm}_{op} (T))) \to {norm}_{op} (A \cdot_{op} T) \in ℝ$
61	57 33 59 37 60	syl22anc	$⊢ A \in ℂ \to {norm}_{op} (A \cdot_{op} T) \in ℝ$
62	61	ad2antrr	$⊢ ((A \in ℂ \land A \neq 0) \land x \in ℋ) \to {norm}_{op} (A \cdot_{op} T) \in ℝ$
63	15	ad2antrr	$⊢ ((A \in ℂ \land A \neq 0) \land x \in ℋ) \to \|A\| \in ℝ$
64		absgt0	$⊢ A \in ℂ \to (A \neq 0 \leftrightarrow 0 < \|A\|)$
65	64	biimpa	$⊢ (A \in ℂ \land A \neq 0) \to 0 < \|A\|$
66	65	adantr	$⊢ ((A \in ℂ \land A \neq 0) \land x \in ℋ) \to 0 < \|A\|$
67		lemuldiv2	$⊢ ({norm}_{ℎ} (T (x)) \in ℝ \land {norm}_{op} (A \cdot_{op} T) \in ℝ \land (\|A\| \in ℝ \land 0 < \|A\|)) \to (\|A\| {norm}_{ℎ} (T (x)) \leq {norm}_{op} (A \cdot_{op} T) \leftrightarrow {norm}_{ℎ} (T (x)) \leq \frac{{norm}_{op} (A \cdot_{op} T)}{\|A\|})$
68	55 62 63 66 67	syl112anc	$⊢ ((A \in ℂ \land A \neq 0) \land x \in ℋ) \to (\|A\| {norm}_{ℎ} (T (x)) \leq {norm}_{op} (A \cdot_{op} T) \leftrightarrow {norm}_{ℎ} (T (x)) \leq \frac{{norm}_{op} (A \cdot_{op} T)}{\|A\|})$
69	68	adantr	$⊢ (((A \in ℂ \land A \neq 0) \land x \in ℋ) \land {norm}_{ℎ} (x) \leq 1) \to (\|A\| {norm}_{ℎ} (T (x)) \leq {norm}_{op} (A \cdot_{op} T) \leftrightarrow {norm}_{ℎ} (T (x)) \leq \frac{{norm}_{op} (A \cdot_{op} T)}{\|A\|})$
70	54 69	mpbid	$⊢ (((A \in ℂ \land A \neq 0) \land x \in ℋ) \land {norm}_{ℎ} (x) \leq 1) \to {norm}_{ℎ} (T (x)) \leq \frac{{norm}_{op} (A \cdot_{op} T)}{\|A\|}$
71	70	ex	$⊢ ((A \in ℂ \land A \neq 0) \land x \in ℋ) \to ({norm}_{ℎ} (x) \leq 1 \to {norm}_{ℎ} (T (x)) \leq \frac{{norm}_{op} (A \cdot_{op} T)}{\|A\|})$
72	71	ralrimiva	$⊢ (A \in ℂ \land A \neq 0) \to \forall x \in ℋ ({norm}_{ℎ} (x) \leq 1 \to {norm}_{ℎ} (T (x)) \leq \frac{{norm}_{op} (A \cdot_{op} T)}{\|A\|})$
73	61	adantr	$⊢ (A \in ℂ \land A \neq 0) \to {norm}_{op} (A \cdot_{op} T) \in ℝ$
74	15	adantr	$⊢ (A \in ℂ \land A \neq 0) \to \|A\| \in ℝ$
75		abs00	$⊢ A \in ℂ \to (\|A\| = 0 \leftrightarrow A = 0)$
76	75	necon3bid	$⊢ A \in ℂ \to (\|A\| \neq 0 \leftrightarrow A \neq 0)$
77	76	biimpar	$⊢ (A \in ℂ \land A \neq 0) \to \|A\| \neq 0$
78	73 74 77	redivcld	$⊢ (A \in ℂ \land A \neq 0) \to \frac{{norm}_{op} (A \cdot_{op} T)}{\|A\|} \in ℝ$
79	78	rexrd	$⊢ (A \in ℂ \land A \neq 0) \to \frac{{norm}_{op} (A \cdot_{op} T)}{\|A\|} \in ℝ^{*}$
80		nmopub	$⊢ (T : ℋ ⟶ ℋ \land \frac{{norm}_{op} (A \cdot_{op} T)}{\|A\|} \in ℝ^{*}) \to ({norm}_{op} (T) \leq \frac{{norm}_{op} (A \cdot_{op} T)}{\|A\|} \leftrightarrow \forall x \in ℋ ({norm}_{ℎ} (x) \leq 1 \to {norm}_{ℎ} (T (x)) \leq \frac{{norm}_{op} (A \cdot_{op} T)}{\|A\|}))$
81	3 79 80	sylancr	$⊢ (A \in ℂ \land A \neq 0) \to ({norm}_{op} (T) \leq \frac{{norm}_{op} (A \cdot_{op} T)}{\|A\|} \leftrightarrow \forall x \in ℋ ({norm}_{ℎ} (x) \leq 1 \to {norm}_{ℎ} (T (x)) \leq \frac{{norm}_{op} (A \cdot_{op} T)}{\|A\|}))$
82	72 81	mpbird	$⊢ (A \in ℂ \land A \neq 0) \to {norm}_{op} (T) \leq \frac{{norm}_{op} (A \cdot_{op} T)}{\|A\|}$
83	23	a1i	$⊢ (A \in ℂ \land A \neq 0) \to {norm}_{op} (T) \in ℝ$
84		lemuldiv2	$⊢ ({norm}_{op} (T) \in ℝ \land {norm}_{op} (A \cdot_{op} T) \in ℝ \land (\|A\| \in ℝ \land 0 < \|A\|)) \to (\|A\| {norm}_{op} (T) \leq {norm}_{op} (A \cdot_{op} T) \leftrightarrow {norm}_{op} (T) \leq \frac{{norm}_{op} (A \cdot_{op} T)}{\|A\|})$
85	83 73 74 65 84	syl112anc	$⊢ (A \in ℂ \land A \neq 0) \to (\|A\| {norm}_{op} (T) \leq {norm}_{op} (A \cdot_{op} T) \leftrightarrow {norm}_{op} (T) \leq \frac{{norm}_{op} (A \cdot_{op} T)}{\|A\|})$
86	82 85	mpbird	$⊢ (A \in ℂ \land A \neq 0) \to \|A\| {norm}_{op} (T) \leq {norm}_{op} (A \cdot_{op} T)$
87	49 86	pm2.61dane	$⊢ A \in ℂ \to \|A\| {norm}_{op} (T) \leq {norm}_{op} (A \cdot_{op} T)$
88	61 33	letri3d	$⊢ A \in ℂ \to ({norm}_{op} (A \cdot_{op} T) = \|A\| {norm}_{op} (T) \leftrightarrow ({norm}_{op} (A \cdot_{op} T) \leq \|A\| {norm}_{op} (T) \land \|A\| {norm}_{op} (T) \leq {norm}_{op} (A \cdot_{op} T)))$
89	37 87 88	mpbir2and	$⊢ A \in ℂ \to {norm}_{op} (A \cdot_{op} T) = \|A\| {norm}_{op} (T)$

Metamath Proof Explorer

Theorem nmophmi

Proof