Theorem leopadd

Description: The sum of two positive operators is positive. Exercise 1(i) of Retherford p. 49. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	leopadd	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ ( 0hop ≤op 𝑇 ∧ 0hop ≤op 𝑈 ) ) → 0hop ≤op ( 𝑇 +op 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		r19.26	⊢ ( ∀ 𝑥 ∈ ℋ ( 0 ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∧ 0 ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) ↔ ( ∀ 𝑥 ∈ ℋ 0 ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∧ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
2		hmopre	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ )
3		hmopre	⊢ ( ( 𝑈 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) → ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ )
4		addge0	⊢ ( ( ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ ∧ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ ) ∧ ( 0 ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∧ 0 ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) ) → 0 ≤ ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) + ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
5	4	ex	⊢ ( ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ ∧ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ ) → ( ( 0 ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∧ 0 ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) → 0 ≤ ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) + ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) ) )
6	2 3 5	syl2an	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑈 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) ) → ( ( 0 ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∧ 0 ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) → 0 ≤ ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) + ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) ) )
7	6	anandirs	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ 𝑥 ∈ ℋ ) → ( ( 0 ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∧ 0 ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) → 0 ≤ ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) + ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) ) )
8		hmopf	⊢ ( 𝑇 ∈ HrmOp → 𝑇 : ℋ ⟶ ℋ )
9		hmopf	⊢ ( 𝑈 ∈ HrmOp → 𝑈 : ℋ ⟶ ℋ )
10	8 9	anim12i	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) )
11		hosval	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 +op 𝑈 ) ‘ 𝑥 ) = ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑈 ‘ 𝑥 ) ) )
12	11	oveq1d	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑇 +op 𝑈 ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑈 ‘ 𝑥 ) ) ·ih 𝑥 ) )
13	12	3expa	⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑇 +op 𝑈 ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑈 ‘ 𝑥 ) ) ·ih 𝑥 ) )
14		ffvelcdm	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
15	14	adantlr	⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
16		ffvelcdm	⊢ ( ( 𝑈 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑈 ‘ 𝑥 ) ∈ ℋ )
17	16	adantll	⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( 𝑈 ‘ 𝑥 ) ∈ ℋ )
18		simpr	⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → 𝑥 ∈ ℋ )
19		ax-his2	⊢ ( ( ( 𝑇 ‘ 𝑥 ) ∈ ℋ ∧ ( 𝑈 ‘ 𝑥 ) ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑈 ‘ 𝑥 ) ) ·ih 𝑥 ) = ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) + ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
20	15 17 18 19	syl3anc	⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑈 ‘ 𝑥 ) ) ·ih 𝑥 ) = ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) + ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
21	13 20	eqtrd	⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑇 +op 𝑈 ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) + ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
22	10 21	sylan	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑇 +op 𝑈 ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) + ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
23	22	breq2d	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ 𝑥 ∈ ℋ ) → ( 0 ≤ ( ( ( 𝑇 +op 𝑈 ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ 0 ≤ ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) + ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) ) )
24	7 23	sylibrd	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ 𝑥 ∈ ℋ ) → ( ( 0 ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∧ 0 ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) → 0 ≤ ( ( ( 𝑇 +op 𝑈 ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
25	24	ralimdva	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( ∀ 𝑥 ∈ ℋ ( 0 ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∧ 0 ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) → ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑇 +op 𝑈 ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
26	1 25	biimtrrid	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( ( ∀ 𝑥 ∈ ℋ 0 ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∧ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) → ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑇 +op 𝑈 ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
27		leoppos	⊢ ( 𝑇 ∈ HrmOp → ( 0hop ≤op 𝑇 ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) )
28		leoppos	⊢ ( 𝑈 ∈ HrmOp → ( 0hop ≤op 𝑈 ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
29	27 28	bi2anan9	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( ( 0hop ≤op 𝑇 ∧ 0hop ≤op 𝑈 ) ↔ ( ∀ 𝑥 ∈ ℋ 0 ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∧ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) ) )
30		hmops	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 +op 𝑈 ) ∈ HrmOp )
31		leoppos	⊢ ( ( 𝑇 +op 𝑈 ) ∈ HrmOp → ( 0hop ≤op ( 𝑇 +op 𝑈 ) ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑇 +op 𝑈 ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
32	30 31	syl	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 0hop ≤op ( 𝑇 +op 𝑈 ) ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑇 +op 𝑈 ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
33	26 29 32	3imtr4d	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( ( 0hop ≤op 𝑇 ∧ 0hop ≤op 𝑈 ) → 0hop ≤op ( 𝑇 +op 𝑈 ) ) )
34	33	imp	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ ( 0hop ≤op 𝑇 ∧ 0hop ≤op 𝑈 ) ) → 0hop ≤op ( 𝑇 +op 𝑈 ) )