Proof of Theorem unierri
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | unierr.1 | . . . . . . . 8
⊢ 𝐹 ∈ UniOp | 
| 2 |  | unopbd 32034 | . . . . . . . 8
⊢ (𝐹 ∈ UniOp → 𝐹 ∈
BndLinOp) | 
| 3 | 1, 2 | ax-mp 5 | . . . . . . 7
⊢ 𝐹 ∈
BndLinOp | 
| 4 |  | bdopf 31881 | . . . . . . 7
⊢ (𝐹 ∈ BndLinOp → 𝐹: ℋ⟶
ℋ) | 
| 5 | 3, 4 | ax-mp 5 | . . . . . 6
⊢ 𝐹: ℋ⟶
ℋ | 
| 6 |  | unierr.2 | . . . . . . . 8
⊢ 𝐺 ∈ UniOp | 
| 7 |  | unopbd 32034 | . . . . . . . 8
⊢ (𝐺 ∈ UniOp → 𝐺 ∈
BndLinOp) | 
| 8 | 6, 7 | ax-mp 5 | . . . . . . 7
⊢ 𝐺 ∈
BndLinOp | 
| 9 |  | bdopf 31881 | . . . . . . 7
⊢ (𝐺 ∈ BndLinOp → 𝐺: ℋ⟶
ℋ) | 
| 10 | 8, 9 | ax-mp 5 | . . . . . 6
⊢ 𝐺: ℋ⟶
ℋ | 
| 11 | 5, 10 | hocofi 31785 | . . . . 5
⊢ (𝐹 ∘ 𝐺): ℋ⟶ ℋ | 
| 12 |  | unierr.3 | . . . . . . . 8
⊢ 𝑆 ∈ UniOp | 
| 13 |  | unopbd 32034 | . . . . . . . 8
⊢ (𝑆 ∈ UniOp → 𝑆 ∈
BndLinOp) | 
| 14 | 12, 13 | ax-mp 5 | . . . . . . 7
⊢ 𝑆 ∈
BndLinOp | 
| 15 |  | bdopf 31881 | . . . . . . 7
⊢ (𝑆 ∈ BndLinOp → 𝑆: ℋ⟶
ℋ) | 
| 16 | 14, 15 | ax-mp 5 | . . . . . 6
⊢ 𝑆: ℋ⟶
ℋ | 
| 17 |  | unierr.4 | . . . . . . . 8
⊢ 𝑇 ∈ UniOp | 
| 18 |  | unopbd 32034 | . . . . . . . 8
⊢ (𝑇 ∈ UniOp → 𝑇 ∈
BndLinOp) | 
| 19 | 17, 18 | ax-mp 5 | . . . . . . 7
⊢ 𝑇 ∈
BndLinOp | 
| 20 |  | bdopf 31881 | . . . . . . 7
⊢ (𝑇 ∈ BndLinOp → 𝑇: ℋ⟶
ℋ) | 
| 21 | 19, 20 | ax-mp 5 | . . . . . 6
⊢ 𝑇: ℋ⟶
ℋ | 
| 22 | 16, 21 | hocofi 31785 | . . . . 5
⊢ (𝑆 ∘ 𝑇): ℋ⟶ ℋ | 
| 23 | 11, 22 | hosubcli 31788 | . . . 4
⊢ ((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝑇)): ℋ⟶ ℋ | 
| 24 |  | nmop0h 32010 | . . . 4
⊢ ((
ℋ = 0ℋ ∧ ((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝑇)): ℋ⟶ ℋ) →
(normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝑇))) = 0) | 
| 25 | 23, 24 | mpan2 691 | . . 3
⊢ ( ℋ
= 0ℋ → (normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝑇))) = 0) | 
| 26 |  | 0le0 12367 | . . . . 5
⊢ 0 ≤
0 | 
| 27 |  | 00id 11436 | . . . . 5
⊢ (0 + 0) =
0 | 
| 28 | 26, 27 | breqtrri 5170 | . . . 4
⊢ 0 ≤ (0
+ 0) | 
| 29 | 5, 16 | hosubcli 31788 | . . . . . 6
⊢ (𝐹 −op 𝑆): ℋ⟶
ℋ | 
| 30 |  | nmop0h 32010 | . . . . . 6
⊢ ((
ℋ = 0ℋ ∧ (𝐹 −op 𝑆): ℋ⟶ ℋ) →
(normop‘(𝐹
−op 𝑆)) =
0) | 
| 31 | 29, 30 | mpan2 691 | . . . . 5
⊢ ( ℋ
= 0ℋ → (normop‘(𝐹 −op 𝑆)) = 0) | 
| 32 | 10, 21 | hosubcli 31788 | . . . . . 6
⊢ (𝐺 −op 𝑇): ℋ⟶
ℋ | 
| 33 |  | nmop0h 32010 | . . . . . 6
⊢ ((
ℋ = 0ℋ ∧ (𝐺 −op 𝑇): ℋ⟶ ℋ) →
(normop‘(𝐺
−op 𝑇)) =
0) | 
| 34 | 32, 33 | mpan2 691 | . . . . 5
⊢ ( ℋ
= 0ℋ → (normop‘(𝐺 −op 𝑇)) = 0) | 
| 35 | 31, 34 | oveq12d 7449 | . . . 4
⊢ ( ℋ
= 0ℋ → ((normop‘(𝐹 −op 𝑆)) + (normop‘(𝐺 −op 𝑇))) = (0 + 0)) | 
| 36 | 28, 35 | breqtrrid 5181 | . . 3
⊢ ( ℋ
= 0ℋ → 0 ≤ ((normop‘(𝐹 −op 𝑆)) +
(normop‘(𝐺
−op 𝑇)))) | 
| 37 | 25, 36 | eqbrtrd 5165 | . 2
⊢ ( ℋ
= 0ℋ → (normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝑇))) ≤ ((normop‘(𝐹 −op 𝑆)) +
(normop‘(𝐺
−op 𝑇)))) | 
| 38 | 16, 10 | hocofi 31785 | . . . . . 6
⊢ (𝑆 ∘ 𝐺): ℋ⟶ ℋ | 
| 39 | 11, 38, 22 | honpncani 31846 | . . . . 5
⊢ (((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺)) +op ((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇))) = ((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝑇)) | 
| 40 | 39 | fveq2i 6909 | . . . 4
⊢
(normop‘(((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺)) +op ((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇)))) = (normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝑇))) | 
| 41 | 3, 8 | bdopcoi 32117 | . . . . . . 7
⊢ (𝐹 ∘ 𝐺) ∈ BndLinOp | 
| 42 | 14, 8 | bdopcoi 32117 | . . . . . . 7
⊢ (𝑆 ∘ 𝐺) ∈ BndLinOp | 
| 43 | 41, 42 | bdophdi 32116 | . . . . . 6
⊢ ((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺)) ∈ BndLinOp | 
| 44 | 14, 19 | bdopcoi 32117 | . . . . . . 7
⊢ (𝑆 ∘ 𝑇) ∈ BndLinOp | 
| 45 | 42, 44 | bdophdi 32116 | . . . . . 6
⊢ ((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇)) ∈ BndLinOp | 
| 46 | 43, 45 | nmoptrii 32113 | . . . . 5
⊢
(normop‘(((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺)) +op ((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇)))) ≤ ((normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺))) + (normop‘((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇)))) | 
| 47 | 5, 16, 10 | hocsubdiri 31799 | . . . . . . . 8
⊢ ((𝐹 −op 𝑆) ∘ 𝐺) = ((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺)) | 
| 48 | 47 | fveq2i 6909 | . . . . . . 7
⊢
(normop‘((𝐹 −op 𝑆) ∘ 𝐺)) = (normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺))) | 
| 49 | 3, 14 | bdophdi 32116 | . . . . . . . 8
⊢ (𝐹 −op 𝑆) ∈
BndLinOp | 
| 50 | 49, 8 | nmopcoi 32114 | . . . . . . 7
⊢
(normop‘((𝐹 −op 𝑆) ∘ 𝐺)) ≤ ((normop‘(𝐹 −op 𝑆)) ·
(normop‘𝐺)) | 
| 51 | 48, 50 | eqbrtrri 5166 | . . . . . 6
⊢
(normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺))) ≤ ((normop‘(𝐹 −op 𝑆)) ·
(normop‘𝐺)) | 
| 52 |  | bdopln 31880 | . . . . . . . . . 10
⊢ (𝑆 ∈ BndLinOp → 𝑆 ∈ LinOp) | 
| 53 | 14, 52 | ax-mp 5 | . . . . . . . . 9
⊢ 𝑆 ∈ LinOp | 
| 54 | 53, 10, 21 | hoddii 32008 | . . . . . . . 8
⊢ (𝑆 ∘ (𝐺 −op 𝑇)) = ((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇)) | 
| 55 | 54 | fveq2i 6909 | . . . . . . 7
⊢
(normop‘(𝑆 ∘ (𝐺 −op 𝑇))) = (normop‘((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇))) | 
| 56 | 8, 19 | bdophdi 32116 | . . . . . . . 8
⊢ (𝐺 −op 𝑇) ∈
BndLinOp | 
| 57 | 14, 56 | nmopcoi 32114 | . . . . . . 7
⊢
(normop‘(𝑆 ∘ (𝐺 −op 𝑇))) ≤ ((normop‘𝑆) ·
(normop‘(𝐺
−op 𝑇))) | 
| 58 | 55, 57 | eqbrtrri 5166 | . . . . . 6
⊢
(normop‘((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇))) ≤ ((normop‘𝑆) ·
(normop‘(𝐺
−op 𝑇))) | 
| 59 |  | nmopre 31889 | . . . . . . . 8
⊢ (((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺)) ∈ BndLinOp →
(normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺))) ∈ ℝ) | 
| 60 | 43, 59 | ax-mp 5 | . . . . . . 7
⊢
(normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺))) ∈ ℝ | 
| 61 |  | nmopre 31889 | . . . . . . . 8
⊢ (((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇)) ∈ BndLinOp →
(normop‘((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇))) ∈ ℝ) | 
| 62 | 45, 61 | ax-mp 5 | . . . . . . 7
⊢
(normop‘((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇))) ∈ ℝ | 
| 63 |  | nmopre 31889 | . . . . . . . . 9
⊢ ((𝐹 −op 𝑆) ∈ BndLinOp →
(normop‘(𝐹
−op 𝑆))
∈ ℝ) | 
| 64 | 49, 63 | ax-mp 5 | . . . . . . . 8
⊢
(normop‘(𝐹 −op 𝑆)) ∈ ℝ | 
| 65 |  | nmopre 31889 | . . . . . . . . 9
⊢ (𝐺 ∈ BndLinOp →
(normop‘𝐺)
∈ ℝ) | 
| 66 | 8, 65 | ax-mp 5 | . . . . . . . 8
⊢
(normop‘𝐺) ∈ ℝ | 
| 67 | 64, 66 | remulcli 11277 | . . . . . . 7
⊢
((normop‘(𝐹 −op 𝑆)) · (normop‘𝐺)) ∈
ℝ | 
| 68 |  | nmopre 31889 | . . . . . . . . 9
⊢ (𝑆 ∈ BndLinOp →
(normop‘𝑆)
∈ ℝ) | 
| 69 | 14, 68 | ax-mp 5 | . . . . . . . 8
⊢
(normop‘𝑆) ∈ ℝ | 
| 70 |  | nmopre 31889 | . . . . . . . . 9
⊢ ((𝐺 −op 𝑇) ∈ BndLinOp →
(normop‘(𝐺
−op 𝑇))
∈ ℝ) | 
| 71 | 56, 70 | ax-mp 5 | . . . . . . . 8
⊢
(normop‘(𝐺 −op 𝑇)) ∈ ℝ | 
| 72 | 69, 71 | remulcli 11277 | . . . . . . 7
⊢
((normop‘𝑆) · (normop‘(𝐺 −op 𝑇))) ∈
ℝ | 
| 73 | 60, 62, 67, 72 | le2addi 11826 | . . . . . 6
⊢
(((normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺))) ≤ ((normop‘(𝐹 −op 𝑆)) ·
(normop‘𝐺)) ∧ (normop‘((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇))) ≤ ((normop‘𝑆) ·
(normop‘(𝐺
−op 𝑇))))
→ ((normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺))) + (normop‘((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇)))) ≤ (((normop‘(𝐹 −op 𝑆)) ·
(normop‘𝐺)) + ((normop‘𝑆) ·
(normop‘(𝐺
−op 𝑇))))) | 
| 74 | 51, 58, 73 | mp2an 692 | . . . . 5
⊢
((normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺))) + (normop‘((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇)))) ≤ (((normop‘(𝐹 −op 𝑆)) ·
(normop‘𝐺)) + ((normop‘𝑆) ·
(normop‘(𝐺
−op 𝑇)))) | 
| 75 | 43, 45 | bdophsi 32115 | . . . . . . 7
⊢ (((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺)) +op ((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇))) ∈ BndLinOp | 
| 76 |  | nmopre 31889 | . . . . . . 7
⊢ ((((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺)) +op ((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇))) ∈ BndLinOp →
(normop‘(((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺)) +op ((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇)))) ∈ ℝ) | 
| 77 | 75, 76 | ax-mp 5 | . . . . . 6
⊢
(normop‘(((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺)) +op ((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇)))) ∈ ℝ | 
| 78 | 60, 62 | readdcli 11276 | . . . . . 6
⊢
((normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺))) + (normop‘((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇)))) ∈ ℝ | 
| 79 | 67, 72 | readdcli 11276 | . . . . . 6
⊢
(((normop‘(𝐹 −op 𝑆)) · (normop‘𝐺)) +
((normop‘𝑆) · (normop‘(𝐺 −op 𝑇)))) ∈
ℝ | 
| 80 | 77, 78, 79 | letri 11390 | . . . . 5
⊢
(((normop‘(((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺)) +op ((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇)))) ≤ ((normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺))) + (normop‘((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇)))) ∧ ((normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺))) + (normop‘((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇)))) ≤ (((normop‘(𝐹 −op 𝑆)) ·
(normop‘𝐺)) + ((normop‘𝑆) ·
(normop‘(𝐺
−op 𝑇)))))
→ (normop‘(((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺)) +op ((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇)))) ≤ (((normop‘(𝐹 −op 𝑆)) ·
(normop‘𝐺)) + ((normop‘𝑆) ·
(normop‘(𝐺
−op 𝑇))))) | 
| 81 | 46, 74, 80 | mp2an 692 | . . . 4
⊢
(normop‘(((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝐺)) +op ((𝑆 ∘ 𝐺) −op (𝑆 ∘ 𝑇)))) ≤ (((normop‘(𝐹 −op 𝑆)) ·
(normop‘𝐺)) + ((normop‘𝑆) ·
(normop‘(𝐺
−op 𝑇)))) | 
| 82 | 40, 81 | eqbrtrri 5166 | . . 3
⊢
(normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝑇))) ≤ (((normop‘(𝐹 −op 𝑆)) ·
(normop‘𝐺)) + ((normop‘𝑆) ·
(normop‘(𝐺
−op 𝑇)))) | 
| 83 |  | nmopun 32033 | . . . . . . 7
⊢ ((
ℋ ≠ 0ℋ ∧ 𝐺 ∈ UniOp) →
(normop‘𝐺)
= 1) | 
| 84 | 6, 83 | mpan2 691 | . . . . . 6
⊢ ( ℋ
≠ 0ℋ → (normop‘𝐺) = 1) | 
| 85 | 84 | oveq2d 7447 | . . . . 5
⊢ ( ℋ
≠ 0ℋ → ((normop‘(𝐹 −op 𝑆)) · (normop‘𝐺)) =
((normop‘(𝐹 −op 𝑆)) · 1)) | 
| 86 | 64 | recni 11275 | . . . . . 6
⊢
(normop‘(𝐹 −op 𝑆)) ∈ ℂ | 
| 87 | 86 | mulridi 11265 | . . . . 5
⊢
((normop‘(𝐹 −op 𝑆)) · 1) =
(normop‘(𝐹
−op 𝑆)) | 
| 88 | 85, 87 | eqtrdi 2793 | . . . 4
⊢ ( ℋ
≠ 0ℋ → ((normop‘(𝐹 −op 𝑆)) · (normop‘𝐺)) =
(normop‘(𝐹
−op 𝑆))) | 
| 89 |  | nmopun 32033 | . . . . . . 7
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑆 ∈ UniOp) →
(normop‘𝑆)
= 1) | 
| 90 | 12, 89 | mpan2 691 | . . . . . 6
⊢ ( ℋ
≠ 0ℋ → (normop‘𝑆) = 1) | 
| 91 | 90 | oveq1d 7446 | . . . . 5
⊢ ( ℋ
≠ 0ℋ → ((normop‘𝑆) · (normop‘(𝐺 −op 𝑇))) = (1 ·
(normop‘(𝐺
−op 𝑇)))) | 
| 92 | 71 | recni 11275 | . . . . . 6
⊢
(normop‘(𝐺 −op 𝑇)) ∈ ℂ | 
| 93 | 92 | mullidi 11266 | . . . . 5
⊢ (1
· (normop‘(𝐺 −op 𝑇))) = (normop‘(𝐺 −op 𝑇)) | 
| 94 | 91, 93 | eqtrdi 2793 | . . . 4
⊢ ( ℋ
≠ 0ℋ → ((normop‘𝑆) · (normop‘(𝐺 −op 𝑇))) =
(normop‘(𝐺
−op 𝑇))) | 
| 95 | 88, 94 | oveq12d 7449 | . . 3
⊢ ( ℋ
≠ 0ℋ → (((normop‘(𝐹 −op 𝑆)) · (normop‘𝐺)) +
((normop‘𝑆) · (normop‘(𝐺 −op 𝑇)))) =
((normop‘(𝐹 −op 𝑆)) + (normop‘(𝐺 −op 𝑇)))) | 
| 96 | 82, 95 | breqtrid 5180 | . 2
⊢ ( ℋ
≠ 0ℋ → (normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝑇))) ≤ ((normop‘(𝐹 −op 𝑆)) +
(normop‘(𝐺
−op 𝑇)))) | 
| 97 | 37, 96 | pm2.61ine 3025 | 1
⊢
(normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝑇))) ≤ ((normop‘(𝐹 −op 𝑆)) +
(normop‘(𝐺
−op 𝑇))) |