Metamath Proof Explorer

Theorem leopmul2i

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

Ref Expression
Assertion leopmul2i ( ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ ( 0 ≤ 𝐴 ∧ 𝑇 ≤op 𝑈 ) ) → ( 𝐴 ·op 𝑇 ) ≤op ( 𝐴 ·op 𝑈 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → 𝐴 ∈ ℝ )
2 hmopd ⊢ ( ( 𝑈 ∈ HrmOp ∧ 𝑇 ∈ HrmOp ) → ( 𝑈 −op 𝑇 ) ∈ HrmOp )
3 2 ancoms ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑈 −op 𝑇 ) ∈ HrmOp )
4 3 3adant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑈 −op 𝑇 ) ∈ HrmOp )
5 leopmuli ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝑈 −op 𝑇 ) ∈ HrmOp ) ∧ ( 0 ≤ 𝐴 ∧ 0hop ≤op ( 𝑈 −op 𝑇 ) ) ) → 0hop ≤op ( 𝐴 ·op ( 𝑈 −op 𝑇 ) ) )
6 5 exp32 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑈 −op 𝑇 ) ∈ HrmOp ) → ( 0 ≤ 𝐴 → ( 0hop ≤op ( 𝑈 −op 𝑇 ) → 0hop ≤op ( 𝐴 ·op ( 𝑈 −op 𝑇 ) ) ) ) )
7 1 4 6 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 0 ≤ 𝐴 → ( 0hop ≤op ( 𝑈 −op 𝑇 ) → 0hop ≤op ( 𝐴 ·op ( 𝑈 −op 𝑇 ) ) ) ) )
8 7 imp ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ 0 ≤ 𝐴 ) → ( 0hop ≤op ( 𝑈 −op 𝑇 ) → 0hop ≤op ( 𝐴 ·op ( 𝑈 −op 𝑇 ) ) ) )
9 leop3 ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 ≤op 𝑈 ↔ 0hop ≤op ( 𝑈 −op 𝑇 ) ) )
10 9 3adant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 ≤op 𝑈 ↔ 0hop ≤op ( 𝑈 −op 𝑇 ) ) )
11 10 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ 0 ≤ 𝐴 ) → ( 𝑇 ≤op 𝑈 ↔ 0hop ≤op ( 𝑈 −op 𝑇 ) ) )
12 hmopm ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ) → ( 𝐴 ·op 𝑇 ) ∈ HrmOp )
13 hmopm ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑈 ∈ HrmOp ) → ( 𝐴 ·op 𝑈 ) ∈ HrmOp )
14 leop3 ⊢ ( ( ( 𝐴 ·op 𝑇 ) ∈ HrmOp ∧ ( 𝐴 ·op 𝑈 ) ∈ HrmOp ) → ( ( 𝐴 ·op 𝑇 ) ≤op ( 𝐴 ·op 𝑈 ) ↔ 0hop ≤op ( ( 𝐴 ·op 𝑈 ) −op ( 𝐴 ·op 𝑇 ) ) ) )
15 12 13 14 syl2an ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ) ∧ ( 𝐴 ∈ ℝ ∧ 𝑈 ∈ HrmOp ) ) → ( ( 𝐴 ·op 𝑇 ) ≤op ( 𝐴 ·op 𝑈 ) ↔ 0hop ≤op ( ( 𝐴 ·op 𝑈 ) −op ( 𝐴 ·op 𝑇 ) ) ) )
16 15 3impdi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( ( 𝐴 ·op 𝑇 ) ≤op ( 𝐴 ·op 𝑈 ) ↔ 0hop ≤op ( ( 𝐴 ·op 𝑈 ) −op ( 𝐴 ·op 𝑇 ) ) ) )
17 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
18 hmopf ⊢ ( 𝑈 ∈ HrmOp → 𝑈 : ℋ ⟶ ℋ )
19 hmopf ⊢ ( 𝑇 ∈ HrmOp → 𝑇 : ℋ ⟶ ℋ )
20 hosubdi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑈 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝐴 ·op ( 𝑈 −op 𝑇 ) ) = ( ( 𝐴 ·op 𝑈 ) −op ( 𝐴 ·op 𝑇 ) ) )
21 17 18 19 20 syl3an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑈 ∈ HrmOp ∧ 𝑇 ∈ HrmOp ) → ( 𝐴 ·op ( 𝑈 −op 𝑇 ) ) = ( ( 𝐴 ·op 𝑈 ) −op ( 𝐴 ·op 𝑇 ) ) )
22 21 3com23 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝐴 ·op ( 𝑈 −op 𝑇 ) ) = ( ( 𝐴 ·op 𝑈 ) −op ( 𝐴 ·op 𝑇 ) ) )
23 22 breq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 0hop ≤op ( 𝐴 ·op ( 𝑈 −op 𝑇 ) ) ↔ 0hop ≤op ( ( 𝐴 ·op 𝑈 ) −op ( 𝐴 ·op 𝑇 ) ) ) )
24 16 23 bitr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( ( 𝐴 ·op 𝑇 ) ≤op ( 𝐴 ·op 𝑈 ) ↔ 0hop ≤op ( 𝐴 ·op ( 𝑈 −op 𝑇 ) ) ) )
25 24 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ 0 ≤ 𝐴 ) → ( ( 𝐴 ·op 𝑇 ) ≤op ( 𝐴 ·op 𝑈 ) ↔ 0hop ≤op ( 𝐴 ·op ( 𝑈 −op 𝑇 ) ) ) )
26 8 11 25 3imtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ 0 ≤ 𝐴 ) → ( 𝑇 ≤op 𝑈 → ( 𝐴 ·op 𝑇 ) ≤op ( 𝐴 ·op 𝑈 ) ) )
27 26 impr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ ( 0 ≤ 𝐴 ∧ 𝑇 ≤op 𝑈 ) ) → ( 𝐴 ·op 𝑇 ) ≤op ( 𝐴 ·op 𝑈 ) )