leopmul

Description: The scalar product of a positive real and a positive operator is a positive operator. Exercise 1(ii) of Retherford p. 49. (Contributed by NM, 23-Aug-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	leopmul	$⊢ (A \in ℝ \land T \in HrmOp \land 0 < A) \to (0_{hop} \leq_{op} T \leftrightarrow 0_{hop} \leq_{op} (A \cdot_{op} T))$

Proof

Step	Hyp	Ref	Expression
1		3simpa	$⊢ (A \in ℝ \land T \in HrmOp \land 0 < A) \to (A \in ℝ \land T \in HrmOp)$
2	1	adantr	$⊢ ((A \in ℝ \land T \in HrmOp \land 0 < A) \land 0_{hop} \leq_{op} T) \to (A \in ℝ \land T \in HrmOp)$
3		0re	$⊢ 0 \in ℝ$
4		ltle	$⊢ (0 \in ℝ \land A \in ℝ) \to (0 < A \to 0 \leq A)$
5	4	3impia	$⊢ (0 \in ℝ \land A \in ℝ \land 0 < A) \to 0 \leq A$
6	3 5	mp3an1	$⊢ (A \in ℝ \land 0 < A) \to 0 \leq A$
7	6	3adant2	$⊢ (A \in ℝ \land T \in HrmOp \land 0 < A) \to 0 \leq A$
8	7	anim1i	$⊢ ((A \in ℝ \land T \in HrmOp \land 0 < A) \land 0_{hop} \leq_{op} T) \to (0 \leq A \land 0_{hop} \leq_{op} T)$
9		leopmuli	$⊢ ((A \in ℝ \land T \in HrmOp) \land (0 \leq A \land 0_{hop} \leq_{op} T)) \to 0_{hop} \leq_{op} (A \cdot_{op} T)$
10	2 8 9	syl2anc	$⊢ ((A \in ℝ \land T \in HrmOp \land 0 < A) \land 0_{hop} \leq_{op} T) \to 0_{hop} \leq_{op} (A \cdot_{op} T)$
11		gt0ne0	$⊢ (A \in ℝ \land 0 < A) \to A \neq 0$
12		rereccl	$⊢ (A \in ℝ \land A \neq 0) \to \frac{1}{A} \in ℝ$
13	11 12	syldan	$⊢ (A \in ℝ \land 0 < A) \to \frac{1}{A} \in ℝ$
14	13	3adant2	$⊢ (A \in ℝ \land T \in HrmOp \land 0 < A) \to \frac{1}{A} \in ℝ$
15		hmopm	$⊢ (A \in ℝ \land T \in HrmOp) \to A \cdot_{op} T \in HrmOp$
16	15	3adant3	$⊢ (A \in ℝ \land T \in HrmOp \land 0 < A) \to A \cdot_{op} T \in HrmOp$
17		recgt0	$⊢ (A \in ℝ \land 0 < A) \to 0 < \frac{1}{A}$
18		ltle	$⊢ (0 \in ℝ \land \frac{1}{A} \in ℝ) \to (0 < \frac{1}{A} \to 0 \leq \frac{1}{A})$
19	3 13 18	sylancr	$⊢ (A \in ℝ \land 0 < A) \to (0 < \frac{1}{A} \to 0 \leq \frac{1}{A})$
20	17 19	mpd	$⊢ (A \in ℝ \land 0 < A) \to 0 \leq \frac{1}{A}$
21	20	3adant2	$⊢ (A \in ℝ \land T \in HrmOp \land 0 < A) \to 0 \leq \frac{1}{A}$
22	14 16 21	jca31	$⊢ (A \in ℝ \land T \in HrmOp \land 0 < A) \to ((\frac{1}{A} \in ℝ \land A \cdot_{op} T \in HrmOp) \land 0 \leq \frac{1}{A})$
23		leopmuli	$⊢ ((\frac{1}{A} \in ℝ \land A \cdot_{op} T \in HrmOp) \land (0 \leq \frac{1}{A} \land 0_{hop} \leq_{op} (A \cdot_{op} T))) \to 0_{hop} \leq_{op} ((\frac{1}{A}) \cdot_{op} (A \cdot_{op} T))$
24	23	anassrs	$⊢ (((\frac{1}{A} \in ℝ \land A \cdot_{op} T \in HrmOp) \land 0 \leq \frac{1}{A}) \land 0_{hop} \leq_{op} (A \cdot_{op} T)) \to 0_{hop} \leq_{op} ((\frac{1}{A}) \cdot_{op} (A \cdot_{op} T))$
25	22 24	sylan	$⊢ ((A \in ℝ \land T \in HrmOp \land 0 < A) \land 0_{hop} \leq_{op} (A \cdot_{op} T)) \to 0_{hop} \leq_{op} ((\frac{1}{A}) \cdot_{op} (A \cdot_{op} T))$
26		recn	$⊢ A \in ℝ \to A \in ℂ$
27	26	adantr	$⊢ (A \in ℝ \land 0 < A) \to A \in ℂ$
28	27 11	recid2d	$⊢ (A \in ℝ \land 0 < A) \to (\frac{1}{A}) A = 1$
29	28	oveq1d	$⊢ (A \in ℝ \land 0 < A) \to (\frac{1}{A}) A \cdot_{op} T = 1 \cdot_{op} T$
30	29	3adant2	$⊢ (A \in ℝ \land T \in HrmOp \land 0 < A) \to (\frac{1}{A}) A \cdot_{op} T = 1 \cdot_{op} T$
31	27 11	reccld	$⊢ (A \in ℝ \land 0 < A) \to \frac{1}{A} \in ℂ$
32	31	3adant2	$⊢ (A \in ℝ \land T \in HrmOp \land 0 < A) \to \frac{1}{A} \in ℂ$
33	26	3ad2ant1	$⊢ (A \in ℝ \land T \in HrmOp \land 0 < A) \to A \in ℂ$
34		hmopf	$⊢ T \in HrmOp \to T : ℋ ⟶ ℋ$
35	34	3ad2ant2	$⊢ (A \in ℝ \land T \in HrmOp \land 0 < A) \to T : ℋ ⟶ ℋ$
36		homulass	$⊢ (\frac{1}{A} \in ℂ \land A \in ℂ \land T : ℋ ⟶ ℋ) \to (\frac{1}{A}) A \cdot_{op} T = (\frac{1}{A}) \cdot_{op} (A \cdot_{op} T)$
37	32 33 35 36	syl3anc	$⊢ (A \in ℝ \land T \in HrmOp \land 0 < A) \to (\frac{1}{A}) A \cdot_{op} T = (\frac{1}{A}) \cdot_{op} (A \cdot_{op} T)$
38		homulid2	$⊢ T : ℋ ⟶ ℋ \to 1 \cdot_{op} T = T$
39	34 38	syl	$⊢ T \in HrmOp \to 1 \cdot_{op} T = T$
40	39	3ad2ant2	$⊢ (A \in ℝ \land T \in HrmOp \land 0 < A) \to 1 \cdot_{op} T = T$
41	30 37 40	3eqtr3d	$⊢ (A \in ℝ \land T \in HrmOp \land 0 < A) \to (\frac{1}{A}) \cdot_{op} (A \cdot_{op} T) = T$
42	41	adantr	$⊢ ((A \in ℝ \land T \in HrmOp \land 0 < A) \land 0_{hop} \leq_{op} (A \cdot_{op} T)) \to (\frac{1}{A}) \cdot_{op} (A \cdot_{op} T) = T$
43	25 42	breqtrd	$⊢ ((A \in ℝ \land T \in HrmOp \land 0 < A) \land 0_{hop} \leq_{op} (A \cdot_{op} T)) \to 0_{hop} \leq_{op} T$
44	10 43	impbida	$⊢ (A \in ℝ \land T \in HrmOp \land 0 < A) \to (0_{hop} \leq_{op} T \leftrightarrow 0_{hop} \leq_{op} (A \cdot_{op} T))$

Metamath Proof Explorer

Theorem leopmul

Proof