Theorem 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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) → ( 0hop ≤op 𝑇 ↔ 0hop ≤op ( 𝐴 ·op 𝑇 ) ) )

Proof

Step	Hyp	Ref	Expression
1		3simpa	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) → ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ) )
2	1	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) ∧ 0hop ≤op 𝑇 ) → ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ) )
3		0re	⊢ 0 ∈ ℝ
4		ltle	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 < 𝐴 → 0 ≤ 𝐴 ) )
5	4	3impia	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 0 ≤ 𝐴 )
6	3 5	mp3an1	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 0 ≤ 𝐴 )
7	6	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) → 0 ≤ 𝐴 )
8	7	anim1i	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) ∧ 0hop ≤op 𝑇 ) → ( 0 ≤ 𝐴 ∧ 0hop ≤op 𝑇 ) )
9		leopmuli	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ) ∧ ( 0 ≤ 𝐴 ∧ 0hop ≤op 𝑇 ) ) → 0hop ≤op ( 𝐴 ·op 𝑇 ) )
10	2 8 9	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) ∧ 0hop ≤op 𝑇 ) → 0hop ≤op ( 𝐴 ·op 𝑇 ) )
11		gt0ne0	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 )
12		rereccl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ ℝ )
13	11 12	syldan	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 1 / 𝐴 ) ∈ ℝ )
14	13	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) → ( 1 / 𝐴 ) ∈ ℝ )
15		hmopm	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ) → ( 𝐴 ·op 𝑇 ) ∈ HrmOp )
16	15	3adant3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) → ( 𝐴 ·op 𝑇 ) ∈ HrmOp )
17		recgt0	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 0 < ( 1 / 𝐴 ) )
18		ltle	⊢ ( ( 0 ∈ ℝ ∧ ( 1 / 𝐴 ) ∈ ℝ ) → ( 0 < ( 1 / 𝐴 ) → 0 ≤ ( 1 / 𝐴 ) ) )
19	3 13 18	sylancr	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 0 < ( 1 / 𝐴 ) → 0 ≤ ( 1 / 𝐴 ) ) )
20	17 19	mpd	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 0 ≤ ( 1 / 𝐴 ) )
21	20	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) → 0 ≤ ( 1 / 𝐴 ) )
22	14 16 21	jca31	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) → ( ( ( 1 / 𝐴 ) ∈ ℝ ∧ ( 𝐴 ·op 𝑇 ) ∈ HrmOp ) ∧ 0 ≤ ( 1 / 𝐴 ) ) )
23		leopmuli	⊢ ( ( ( ( 1 / 𝐴 ) ∈ ℝ ∧ ( 𝐴 ·op 𝑇 ) ∈ HrmOp ) ∧ ( 0 ≤ ( 1 / 𝐴 ) ∧ 0hop ≤op ( 𝐴 ·op 𝑇 ) ) ) → 0hop ≤op ( ( 1 / 𝐴 ) ·op ( 𝐴 ·op 𝑇 ) ) )
24	23	anassrs	⊢ ( ( ( ( ( 1 / 𝐴 ) ∈ ℝ ∧ ( 𝐴 ·op 𝑇 ) ∈ HrmOp ) ∧ 0 ≤ ( 1 / 𝐴 ) ) ∧ 0hop ≤op ( 𝐴 ·op 𝑇 ) ) → 0hop ≤op ( ( 1 / 𝐴 ) ·op ( 𝐴 ·op 𝑇 ) ) )
25	22 24	sylan	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) ∧ 0hop ≤op ( 𝐴 ·op 𝑇 ) ) → 0hop ≤op ( ( 1 / 𝐴 ) ·op ( 𝐴 ·op 𝑇 ) ) )
26		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
27	26	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ∈ ℂ )
28	27 11	recid2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( ( 1 / 𝐴 ) · 𝐴 ) = 1 )
29	28	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( ( ( 1 / 𝐴 ) · 𝐴 ) ·op 𝑇 ) = ( 1 ·op 𝑇 ) )
30	29	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) → ( ( ( 1 / 𝐴 ) · 𝐴 ) ·op 𝑇 ) = ( 1 ·op 𝑇 ) )
31	27 11	reccld	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 1 / 𝐴 ) ∈ ℂ )
32	31	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) → ( 1 / 𝐴 ) ∈ ℂ )
33	26	3ad2ant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) → 𝐴 ∈ ℂ )
34		hmopf	⊢ ( 𝑇 ∈ HrmOp → 𝑇 : ℋ ⟶ ℋ )
35	34	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) → 𝑇 : ℋ ⟶ ℋ )
36		homulass	⊢ ( ( ( 1 / 𝐴 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ( ( 1 / 𝐴 ) · 𝐴 ) ·op 𝑇 ) = ( ( 1 / 𝐴 ) ·op ( 𝐴 ·op 𝑇 ) ) )
37	32 33 35 36	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) → ( ( ( 1 / 𝐴 ) · 𝐴 ) ·op 𝑇 ) = ( ( 1 / 𝐴 ) ·op ( 𝐴 ·op 𝑇 ) ) )
38		homulid2	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 1 ·op 𝑇 ) = 𝑇 )
39	34 38	syl	⊢ ( 𝑇 ∈ HrmOp → ( 1 ·op 𝑇 ) = 𝑇 )
40	39	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) → ( 1 ·op 𝑇 ) = 𝑇 )
41	30 37 40	3eqtr3d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) → ( ( 1 / 𝐴 ) ·op ( 𝐴 ·op 𝑇 ) ) = 𝑇 )
42	41	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) ∧ 0hop ≤op ( 𝐴 ·op 𝑇 ) ) → ( ( 1 / 𝐴 ) ·op ( 𝐴 ·op 𝑇 ) ) = 𝑇 )
43	25 42	breqtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) ∧ 0hop ≤op ( 𝐴 ·op 𝑇 ) ) → 0hop ≤op 𝑇 )
44	10 43	impbida	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴 ) → ( 0hop ≤op 𝑇 ↔ 0hop ≤op ( 𝐴 ·op 𝑇 ) ) )