nmopleid

Description: A nonzero, bounded Hermitian operator divided by its norm is less than or equal to the identity operator. (Contributed by NM, 12-Aug-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	nmopleid	$⊢ (T \in HrmOp \land {norm}_{op} (T) \in ℝ \land T \neq 0_{hop}) \to ((\frac{1}{{norm}_{op} (T)}) \cdot_{op} T) \leq_{op} I_{op}$

Proof

Step	Hyp	Ref	Expression
1		hmoplin	$⊢ T \in HrmOp \to T \in LinOp$
2		nmlnopne0	$⊢ T \in LinOp \to ({norm}_{op} (T) \neq 0 \leftrightarrow T \neq 0_{hop})$
3	2	biimpar	$⊢ (T \in LinOp \land T \neq 0_{hop}) \to {norm}_{op} (T) \neq 0$
4	1 3	sylan	$⊢ (T \in HrmOp \land T \neq 0_{hop}) \to {norm}_{op} (T) \neq 0$
5	4	adantlr	$⊢ ((T \in HrmOp \land {norm}_{op} (T) \in ℝ) \land T \neq 0_{hop}) \to {norm}_{op} (T) \neq 0$
6		rereccl	$⊢ ({norm}_{op} (T) \in ℝ \land {norm}_{op} (T) \neq 0) \to \frac{1}{{norm}_{op} (T)} \in ℝ$
7	6	adantll	$⊢ ((T \in HrmOp \land {norm}_{op} (T) \in ℝ) \land {norm}_{op} (T) \neq 0) \to \frac{1}{{norm}_{op} (T)} \in ℝ$
8		simpll	$⊢ ((T \in HrmOp \land {norm}_{op} (T) \in ℝ) \land {norm}_{op} (T) \neq 0) \to T \in HrmOp$
9		idhmop	$⊢ I_{op} \in HrmOp$
10		hmopm	$⊢ ({norm}_{op} (T) \in ℝ \land I_{op} \in HrmOp) \to {norm}_{op} (T) \cdot_{op} I_{op} \in HrmOp$
11	9 10	mpan2	$⊢ {norm}_{op} (T) \in ℝ \to {norm}_{op} (T) \cdot_{op} I_{op} \in HrmOp$
12	11	ad2antlr	$⊢ ((T \in HrmOp \land {norm}_{op} (T) \in ℝ) \land {norm}_{op} (T) \neq 0) \to {norm}_{op} (T) \cdot_{op} I_{op} \in HrmOp$
13		simplr	$⊢ ((T \in HrmOp \land {norm}_{op} (T) \in ℝ) \land {norm}_{op} (T) \neq 0) \to {norm}_{op} (T) \in ℝ$
14		hmopf	$⊢ T \in HrmOp \to T : ℋ ⟶ ℋ$
15		nmopgt0	$⊢ T : ℋ ⟶ ℋ \to ({norm}_{op} (T) \neq 0 \leftrightarrow 0 < {norm}_{op} (T))$
16	15	biimpa	$⊢ (T : ℋ ⟶ ℋ \land {norm}_{op} (T) \neq 0) \to 0 < {norm}_{op} (T)$
17	14 16	sylan	$⊢ (T \in HrmOp \land {norm}_{op} (T) \neq 0) \to 0 < {norm}_{op} (T)$
18	17	adantlr	$⊢ ((T \in HrmOp \land {norm}_{op} (T) \in ℝ) \land {norm}_{op} (T) \neq 0) \to 0 < {norm}_{op} (T)$
19	13 18	recgt0d	$⊢ ((T \in HrmOp \land {norm}_{op} (T) \in ℝ) \land {norm}_{op} (T) \neq 0) \to 0 < \frac{1}{{norm}_{op} (T)}$
20		0re	$⊢ 0 \in ℝ$
21		ltle	$⊢ (0 \in ℝ \land \frac{1}{{norm}_{op} (T)} \in ℝ) \to (0 < \frac{1}{{norm}_{op} (T)} \to 0 \leq \frac{1}{{norm}_{op} (T)})$
22	20 6 21	sylancr	$⊢ ({norm}_{op} (T) \in ℝ \land {norm}_{op} (T) \neq 0) \to (0 < \frac{1}{{norm}_{op} (T)} \to 0 \leq \frac{1}{{norm}_{op} (T)})$
23	22	adantll	$⊢ ((T \in HrmOp \land {norm}_{op} (T) \in ℝ) \land {norm}_{op} (T) \neq 0) \to (0 < \frac{1}{{norm}_{op} (T)} \to 0 \leq \frac{1}{{norm}_{op} (T)})$
24	19 23	mpd	$⊢ ((T \in HrmOp \land {norm}_{op} (T) \in ℝ) \land {norm}_{op} (T) \neq 0) \to 0 \leq \frac{1}{{norm}_{op} (T)}$
25		leopnmid	$⊢ (T \in HrmOp \land {norm}_{op} (T) \in ℝ) \to T \leq_{op} ({norm}_{op} (T) \cdot_{op} I_{op})$
26	25	adantr	$⊢ ((T \in HrmOp \land {norm}_{op} (T) \in ℝ) \land {norm}_{op} (T) \neq 0) \to T \leq_{op} ({norm}_{op} (T) \cdot_{op} I_{op})$
27		leopmul2i	$⊢ ((\frac{1}{{norm}_{op} (T)} \in ℝ \land T \in HrmOp \land {norm}_{op} (T) \cdot_{op} I_{op} \in HrmOp) \land (0 \leq \frac{1}{{norm}_{op} (T)} \land T \leq_{op} ({norm}_{op} (T) \cdot_{op} I_{op}))) \to ((\frac{1}{{norm}_{op} (T)}) \cdot_{op} T) \leq_{op} ((\frac{1}{{norm}_{op} (T)}) \cdot_{op} ({norm}_{op} (T) \cdot_{op} I_{op}))$
28	7 8 12 24 26 27	syl32anc	$⊢ ((T \in HrmOp \land {norm}_{op} (T) \in ℝ) \land {norm}_{op} (T) \neq 0) \to ((\frac{1}{{norm}_{op} (T)}) \cdot_{op} T) \leq_{op} ((\frac{1}{{norm}_{op} (T)}) \cdot_{op} ({norm}_{op} (T) \cdot_{op} I_{op}))$
29		recn	$⊢ {norm}_{op} (T) \in ℝ \to {norm}_{op} (T) \in ℂ$
30		reccl	$⊢ ({norm}_{op} (T) \in ℂ \land {norm}_{op} (T) \neq 0) \to \frac{1}{{norm}_{op} (T)} \in ℂ$
31		simpl	$⊢ ({norm}_{op} (T) \in ℂ \land {norm}_{op} (T) \neq 0) \to {norm}_{op} (T) \in ℂ$
32		hoif	$⊢ I_{op} : ℋ \underset{1-1 onto}{⟶} ℋ$
33		f1of	$⊢ I_{op} : ℋ \underset{1-1 onto}{⟶} ℋ \to I_{op} : ℋ ⟶ ℋ$
34	32 33	ax-mp	$⊢ I_{op} : ℋ ⟶ ℋ$
35		homulass	$⊢ (\frac{1}{{norm}_{op} (T)} \in ℂ \land {norm}_{op} (T) \in ℂ \land I_{op} : ℋ ⟶ ℋ) \to (\frac{1}{{norm}_{op} (T)}) {norm}_{op} (T) \cdot_{op} I_{op} = (\frac{1}{{norm}_{op} (T)}) \cdot_{op} ({norm}_{op} (T) \cdot_{op} I_{op})$
36	34 35	mp3an3	$⊢ (\frac{1}{{norm}_{op} (T)} \in ℂ \land {norm}_{op} (T) \in ℂ) \to (\frac{1}{{norm}_{op} (T)}) {norm}_{op} (T) \cdot_{op} I_{op} = (\frac{1}{{norm}_{op} (T)}) \cdot_{op} ({norm}_{op} (T) \cdot_{op} I_{op})$
37	30 31 36	syl2anc	$⊢ ({norm}_{op} (T) \in ℂ \land {norm}_{op} (T) \neq 0) \to (\frac{1}{{norm}_{op} (T)}) {norm}_{op} (T) \cdot_{op} I_{op} = (\frac{1}{{norm}_{op} (T)}) \cdot_{op} ({norm}_{op} (T) \cdot_{op} I_{op})$
38		recid2	$⊢ ({norm}_{op} (T) \in ℂ \land {norm}_{op} (T) \neq 0) \to (\frac{1}{{norm}_{op} (T)}) {norm}_{op} (T) = 1$
39	38	oveq1d	$⊢ ({norm}_{op} (T) \in ℂ \land {norm}_{op} (T) \neq 0) \to (\frac{1}{{norm}_{op} (T)}) {norm}_{op} (T) \cdot_{op} I_{op} = 1 \cdot_{op} I_{op}$
40	37 39	eqtr3d	$⊢ ({norm}_{op} (T) \in ℂ \land {norm}_{op} (T) \neq 0) \to (\frac{1}{{norm}_{op} (T)}) \cdot_{op} ({norm}_{op} (T) \cdot_{op} I_{op}) = 1 \cdot_{op} I_{op}$
41		homullid	$⊢ I_{op} : ℋ ⟶ ℋ \to 1 \cdot_{op} I_{op} = I_{op}$
42	34 41	ax-mp	$⊢ 1 \cdot_{op} I_{op} = I_{op}$
43	40 42	eqtrdi	$⊢ ({norm}_{op} (T) \in ℂ \land {norm}_{op} (T) \neq 0) \to (\frac{1}{{norm}_{op} (T)}) \cdot_{op} ({norm}_{op} (T) \cdot_{op} I_{op}) = I_{op}$
44	29 43	sylan	$⊢ ({norm}_{op} (T) \in ℝ \land {norm}_{op} (T) \neq 0) \to (\frac{1}{{norm}_{op} (T)}) \cdot_{op} ({norm}_{op} (T) \cdot_{op} I_{op}) = I_{op}$
45	44	adantll	$⊢ ((T \in HrmOp \land {norm}_{op} (T) \in ℝ) \land {norm}_{op} (T) \neq 0) \to (\frac{1}{{norm}_{op} (T)}) \cdot_{op} ({norm}_{op} (T) \cdot_{op} I_{op}) = I_{op}$
46	28 45	breqtrd	$⊢ ((T \in HrmOp \land {norm}_{op} (T) \in ℝ) \land {norm}_{op} (T) \neq 0) \to ((\frac{1}{{norm}_{op} (T)}) \cdot_{op} T) \leq_{op} I_{op}$
47	5 46	syldan	$⊢ ((T \in HrmOp \land {norm}_{op} (T) \in ℝ) \land T \neq 0_{hop}) \to ((\frac{1}{{norm}_{op} (T)}) \cdot_{op} T) \leq_{op} I_{op}$
48	47	3impa	$⊢ (T \in HrmOp \land {norm}_{op} (T) \in ℝ \land T \neq 0_{hop}) \to ((\frac{1}{{norm}_{op} (T)}) \cdot_{op} T) \leq_{op} I_{op}$

Metamath Proof Explorer

Theorem nmopleid

Proof