Metamath Proof Explorer

Theorem lnfncon

Description: A condition equivalent to " T is continuous" when T is linear. Theorem 3.5(iii) of Beran p. 99. (Contributed by NM, 16-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion lnfncon ⊢ T ∈ LinFn → T ∈ ContFn ↔ ∃ x ∈ ℝ ∀ y ∈ ℋ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ T = if T ∈ LinFn T ℋ × 0 → T ∈ ContFn ↔ if T ∈ LinFn T ℋ × 0 ∈ ContFn
2 fveq1 ⊢ T = if T ∈ LinFn T ℋ × 0 → T ⁡ y = if T ∈ LinFn T ℋ × 0 ⁡ y
3 2 fveq2d ⊢ T = if T ∈ LinFn T ℋ × 0 → T ⁡ y = if T ∈ LinFn T ℋ × 0 ⁡ y
4 3 breq1d ⊢ T = if T ∈ LinFn T ℋ × 0 → T ⁡ y ≤ x ⁢ norm ℎ ⁡ y ↔ if T ∈ LinFn T ℋ × 0 ⁡ y ≤ x ⁢ norm ℎ ⁡ y
5 4 rexralbidv ⊢ T = if T ∈ LinFn T ℋ × 0 → ∃ x ∈ ℝ ∀ y ∈ ℋ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y ↔ ∃ x ∈ ℝ ∀ y ∈ ℋ if T ∈ LinFn T ℋ × 0 ⁡ y ≤ x ⁢ norm ℎ ⁡ y
6 1 5 bibi12d ⊢ T = if T ∈ LinFn T ℋ × 0 → T ∈ ContFn ↔ ∃ x ∈ ℝ ∀ y ∈ ℋ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y ↔ if T ∈ LinFn T ℋ × 0 ∈ ContFn ↔ ∃ x ∈ ℝ ∀ y ∈ ℋ if T ∈ LinFn T ℋ × 0 ⁡ y ≤ x ⁢ norm ℎ ⁡ y
7 0lnfn ⊢ ℋ × 0 ∈ LinFn
8 7 elimel ⊢ if T ∈ LinFn T ℋ × 0 ∈ LinFn
9 8 lnfnconi ⊢ if T ∈ LinFn T ℋ × 0 ∈ ContFn ↔ ∃ x ∈ ℝ ∀ y ∈ ℋ if T ∈ LinFn T ℋ × 0 ⁡ y ≤ x ⁢ norm ℎ ⁡ y
10 6 9 dedth ⊢ T ∈ LinFn → T ∈ ContFn ↔ ∃ x ∈ ℝ ∀ y ∈ ℋ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y