leopmul2i

Description: Scalar product applied to operator ordering. (Contributed by NM, 12-Aug-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	leopmul2i	$⊢ ((A \in ℝ \land T \in HrmOp \land U \in HrmOp) \land (0 \leq A \land T \leq_{op} U)) \to (A \cdot_{op} T) \leq_{op} (A \cdot_{op} U)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in ℝ \land T \in HrmOp \land U \in HrmOp) \to A \in ℝ$
2		hmopd	$⊢ (U \in HrmOp \land T \in HrmOp) \to U -_{op} T \in HrmOp$
3	2	ancoms	$⊢ (T \in HrmOp \land U \in HrmOp) \to U -_{op} T \in HrmOp$
4	3	3adant1	$⊢ (A \in ℝ \land T \in HrmOp \land U \in HrmOp) \to U -_{op} T \in HrmOp$
5		leopmuli	$⊢ ((A \in ℝ \land U -_{op} T \in HrmOp) \land (0 \leq A \land 0_{hop} \leq_{op} (U -_{op} T))) \to 0_{hop} \leq_{op} (A \cdot_{op} (U -_{op} T))$
6	5	exp32	$⊢ (A \in ℝ \land U -_{op} T \in HrmOp) \to (0 \leq A \to (0_{hop} \leq_{op} (U -_{op} T) \to 0_{hop} \leq_{op} (A \cdot_{op} (U -_{op} T))))$
7	1 4 6	syl2anc	$⊢ (A \in ℝ \land T \in HrmOp \land U \in HrmOp) \to (0 \leq A \to (0_{hop} \leq_{op} (U -_{op} T) \to 0_{hop} \leq_{op} (A \cdot_{op} (U -_{op} T))))$
8	7	imp	$⊢ ((A \in ℝ \land T \in HrmOp \land U \in HrmOp) \land 0 \leq A) \to (0_{hop} \leq_{op} (U -_{op} T) \to 0_{hop} \leq_{op} (A \cdot_{op} (U -_{op} T)))$
9		leop3	$⊢ (T \in HrmOp \land U \in HrmOp) \to (T \leq_{op} U \leftrightarrow 0_{hop} \leq_{op} (U -_{op} T))$
10	9	3adant1	$⊢ (A \in ℝ \land T \in HrmOp \land U \in HrmOp) \to (T \leq_{op} U \leftrightarrow 0_{hop} \leq_{op} (U -_{op} T))$
11	10	adantr	$⊢ ((A \in ℝ \land T \in HrmOp \land U \in HrmOp) \land 0 \leq A) \to (T \leq_{op} U \leftrightarrow 0_{hop} \leq_{op} (U -_{op} T))$
12		hmopm	$⊢ (A \in ℝ \land T \in HrmOp) \to A \cdot_{op} T \in HrmOp$
13		hmopm	$⊢ (A \in ℝ \land U \in HrmOp) \to A \cdot_{op} U \in HrmOp$
14		leop3	$⊢ (A \cdot_{op} T \in HrmOp \land A \cdot_{op} U \in HrmOp) \to ((A \cdot_{op} T) \leq_{op} (A \cdot_{op} U) \leftrightarrow 0_{hop} \leq_{op} ((A \cdot_{op} U) -_{op} (A \cdot_{op} T)))$
15	12 13 14	syl2an	$⊢ ((A \in ℝ \land T \in HrmOp) \land (A \in ℝ \land U \in HrmOp)) \to ((A \cdot_{op} T) \leq_{op} (A \cdot_{op} U) \leftrightarrow 0_{hop} \leq_{op} ((A \cdot_{op} U) -_{op} (A \cdot_{op} T)))$
16	15	3impdi	$⊢ (A \in ℝ \land T \in HrmOp \land U \in HrmOp) \to ((A \cdot_{op} T) \leq_{op} (A \cdot_{op} U) \leftrightarrow 0_{hop} \leq_{op} ((A \cdot_{op} U) -_{op} (A \cdot_{op} T)))$
17		recn	$⊢ A \in ℝ \to A \in ℂ$
18		hmopf	$⊢ U \in HrmOp \to U : ℋ ⟶ ℋ$
19		hmopf	$⊢ T \in HrmOp \to T : ℋ ⟶ ℋ$
20		hosubdi	$⊢ (A \in ℂ \land U : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to A \cdot_{op} (U -_{op} T) = (A \cdot_{op} U) -_{op} (A \cdot_{op} T)$
21	17 18 19 20	syl3an	$⊢ (A \in ℝ \land U \in HrmOp \land T \in HrmOp) \to A \cdot_{op} (U -_{op} T) = (A \cdot_{op} U) -_{op} (A \cdot_{op} T)$
22	21	3com23	$⊢ (A \in ℝ \land T \in HrmOp \land U \in HrmOp) \to A \cdot_{op} (U -_{op} T) = (A \cdot_{op} U) -_{op} (A \cdot_{op} T)$
23	22	breq2d	$⊢ (A \in ℝ \land T \in HrmOp \land U \in HrmOp) \to (0_{hop} \leq_{op} (A \cdot_{op} (U -_{op} T)) \leftrightarrow 0_{hop} \leq_{op} ((A \cdot_{op} U) -_{op} (A \cdot_{op} T)))$
24	16 23	bitr4d	$⊢ (A \in ℝ \land T \in HrmOp \land U \in HrmOp) \to ((A \cdot_{op} T) \leq_{op} (A \cdot_{op} U) \leftrightarrow 0_{hop} \leq_{op} (A \cdot_{op} (U -_{op} T)))$
25	24	adantr	$⊢ ((A \in ℝ \land T \in HrmOp \land U \in HrmOp) \land 0 \leq A) \to ((A \cdot_{op} T) \leq_{op} (A \cdot_{op} U) \leftrightarrow 0_{hop} \leq_{op} (A \cdot_{op} (U -_{op} T)))$
26	8 11 25	3imtr4d	$⊢ ((A \in ℝ \land T \in HrmOp \land U \in HrmOp) \land 0 \leq A) \to (T \leq_{op} U \to (A \cdot_{op} T) \leq_{op} (A \cdot_{op} U))$
27	26	impr	$⊢ ((A \in ℝ \land T \in HrmOp \land U \in HrmOp) \land (0 \leq A \land T \leq_{op} U)) \to (A \cdot_{op} T) \leq_{op} (A \cdot_{op} U)$

Metamath Proof Explorer

Theorem leopmul2i

Proof