Proof of Theorem nmbdfnlb
Step | Hyp | Ref
| Expression |
1 | | fveq1 6773 |
. . . . . 6
⊢ (𝑇 = if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0})) → (𝑇‘𝐴) = (if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0}))‘𝐴)) |
2 | 1 | fveq2d 6778 |
. . . . 5
⊢ (𝑇 = if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0})) → (abs‘(𝑇‘𝐴)) = (abs‘(if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0}))‘𝐴))) |
3 | | fveq2 6774 |
. . . . . 6
⊢ (𝑇 = if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0})) → (normfn‘𝑇) = (normfn‘if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0})))) |
4 | 3 | oveq1d 7290 |
. . . . 5
⊢ (𝑇 = if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0})) → ((normfn‘𝑇) ·
(normℎ‘𝐴)) = ((normfn‘if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0}))) · (normℎ‘𝐴))) |
5 | 2, 4 | breq12d 5087 |
. . . 4
⊢ (𝑇 = if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0})) → ((abs‘(𝑇‘𝐴)) ≤ ((normfn‘𝑇) ·
(normℎ‘𝐴)) ↔ (abs‘(if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0}))‘𝐴)) ≤ ((normfn‘if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0}))) · (normℎ‘𝐴)))) |
6 | 5 | imbi2d 341 |
. . 3
⊢ (𝑇 = if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0})) → ((𝐴 ∈ ℋ → (abs‘(𝑇‘𝐴)) ≤ ((normfn‘𝑇) ·
(normℎ‘𝐴))) ↔ (𝐴 ∈ ℋ → (abs‘(if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0}))‘𝐴)) ≤ ((normfn‘if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0}))) · (normℎ‘𝐴))))) |
7 | | eleq1 2826 |
. . . . . 6
⊢ (𝑇 = if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0})) → (𝑇 ∈ LinFn ↔ if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0})) ∈ LinFn)) |
8 | 3 | eleq1d 2823 |
. . . . . 6
⊢ (𝑇 = if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0})) → ((normfn‘𝑇) ∈ ℝ ↔
(normfn‘if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0}))) ∈ ℝ)) |
9 | 7, 8 | anbi12d 631 |
. . . . 5
⊢ (𝑇 = if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0})) → ((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ) ↔ (if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0})) ∈ LinFn ∧ (normfn‘if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0}))) ∈ ℝ))) |
10 | | eleq1 2826 |
. . . . . 6
⊢ ((
ℋ × {0}) = if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0})) → (( ℋ × {0}) ∈ LinFn ↔
if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0})) ∈ LinFn)) |
11 | | fveq2 6774 |
. . . . . . 7
⊢ ((
ℋ × {0}) = if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0})) → (normfn‘( ℋ × {0})) =
(normfn‘if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0})))) |
12 | 11 | eleq1d 2823 |
. . . . . 6
⊢ ((
ℋ × {0}) = if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0})) → ((normfn‘( ℋ × {0}))
∈ ℝ ↔ (normfn‘if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0}))) ∈ ℝ)) |
13 | 10, 12 | anbi12d 631 |
. . . . 5
⊢ ((
ℋ × {0}) = if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0})) → ((( ℋ × {0}) ∈ LinFn ∧
(normfn‘( ℋ × {0})) ∈ ℝ) ↔
(if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0})) ∈ LinFn ∧ (normfn‘if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0}))) ∈ ℝ))) |
14 | | 0lnfn 30347 |
. . . . . 6
⊢ ( ℋ
× {0}) ∈ LinFn |
15 | | nmfn0 30349 |
. . . . . . 7
⊢
(normfn‘( ℋ × {0})) = 0 |
16 | | 0re 10977 |
. . . . . . 7
⊢ 0 ∈
ℝ |
17 | 15, 16 | eqeltri 2835 |
. . . . . 6
⊢
(normfn‘( ℋ × {0})) ∈
ℝ |
18 | 14, 17 | pm3.2i 471 |
. . . . 5
⊢ ((
ℋ × {0}) ∈ LinFn ∧ (normfn‘( ℋ
× {0})) ∈ ℝ) |
19 | 9, 13, 18 | elimhyp 4524 |
. . . 4
⊢
(if((𝑇 ∈ LinFn
∧ (normfn‘𝑇) ∈ ℝ), 𝑇, ( ℋ × {0})) ∈ LinFn ∧
(normfn‘if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0}))) ∈ ℝ) |
20 | 19 | nmbdfnlbi 30411 |
. . 3
⊢ (𝐴 ∈ ℋ →
(abs‘(if((𝑇 ∈
LinFn ∧ (normfn‘𝑇) ∈ ℝ), 𝑇, ( ℋ × {0}))‘𝐴)) ≤
((normfn‘if((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ), 𝑇, (
ℋ × {0}))) · (normℎ‘𝐴))) |
21 | 6, 20 | dedth 4517 |
. 2
⊢ ((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ) → (𝐴
∈ ℋ → (abs‘(𝑇‘𝐴)) ≤ ((normfn‘𝑇) ·
(normℎ‘𝐴)))) |
22 | 21 | 3impia 1116 |
1
⊢ ((𝑇 ∈ LinFn ∧
(normfn‘𝑇)
∈ ℝ ∧ 𝐴
∈ ℋ) → (abs‘(𝑇‘𝐴)) ≤ ((normfn‘𝑇) ·
(normℎ‘𝐴))) |