Step |
Hyp |
Ref |
Expression |
1 |
|
lnfncnbd |
⊢ ( 𝑇 ∈ LinFn → ( 𝑇 ∈ ContFn ↔ ( normfn ‘ 𝑇 ) ∈ ℝ ) ) |
2 |
|
elin |
⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) ↔ ( 𝑇 ∈ LinFn ∧ 𝑇 ∈ ContFn ) ) |
3 |
|
fveq1 |
⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( 𝑇 ‘ 𝑥 ) = ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑥 ) ) |
4 |
3
|
eqeq1d |
⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ↔ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) |
5 |
4
|
rexralbidv |
⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ↔ ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) |
6 |
|
inss1 |
⊢ ( LinFn ∩ ContFn ) ⊆ LinFn |
7 |
|
0lnfn |
⊢ ( ℋ × { 0 } ) ∈ LinFn |
8 |
|
0cnfn |
⊢ ( ℋ × { 0 } ) ∈ ContFn |
9 |
|
elin |
⊢ ( ( ℋ × { 0 } ) ∈ ( LinFn ∩ ContFn ) ↔ ( ( ℋ × { 0 } ) ∈ LinFn ∧ ( ℋ × { 0 } ) ∈ ContFn ) ) |
10 |
7 8 9
|
mpbir2an |
⊢ ( ℋ × { 0 } ) ∈ ( LinFn ∩ ContFn ) |
11 |
10
|
elimel |
⊢ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ ( LinFn ∩ ContFn ) |
12 |
6 11
|
sselii |
⊢ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ LinFn |
13 |
|
inss2 |
⊢ ( LinFn ∩ ContFn ) ⊆ ContFn |
14 |
13 11
|
sselii |
⊢ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ ContFn |
15 |
12 14
|
riesz3i |
⊢ ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) |
16 |
5 15
|
dedth |
⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) |
17 |
2 16
|
sylbir |
⊢ ( ( 𝑇 ∈ LinFn ∧ 𝑇 ∈ ContFn ) → ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) |
18 |
17
|
ex |
⊢ ( 𝑇 ∈ LinFn → ( 𝑇 ∈ ContFn → ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) |
19 |
|
normcl |
⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ 𝑦 ) ∈ ℝ ) |
20 |
19
|
adantl |
⊢ ( ( 𝑇 ∈ LinFn ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ 𝑦 ) ∈ ℝ ) |
21 |
|
fveq2 |
⊢ ( ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) → ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) = ( abs ‘ ( 𝑥 ·ih 𝑦 ) ) ) |
22 |
21
|
adantl |
⊢ ( ( ( ( 𝑇 ∈ LinFn ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) → ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) = ( abs ‘ ( 𝑥 ·ih 𝑦 ) ) ) |
23 |
|
bcs |
⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( abs ‘ ( 𝑥 ·ih 𝑦 ) ) ≤ ( ( normℎ ‘ 𝑥 ) · ( normℎ ‘ 𝑦 ) ) ) |
24 |
|
normcl |
⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ 𝑥 ) ∈ ℝ ) |
25 |
|
recn |
⊢ ( ( normℎ ‘ 𝑥 ) ∈ ℝ → ( normℎ ‘ 𝑥 ) ∈ ℂ ) |
26 |
|
recn |
⊢ ( ( normℎ ‘ 𝑦 ) ∈ ℝ → ( normℎ ‘ 𝑦 ) ∈ ℂ ) |
27 |
|
mulcom |
⊢ ( ( ( normℎ ‘ 𝑥 ) ∈ ℂ ∧ ( normℎ ‘ 𝑦 ) ∈ ℂ ) → ( ( normℎ ‘ 𝑥 ) · ( normℎ ‘ 𝑦 ) ) = ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) |
28 |
25 26 27
|
syl2an |
⊢ ( ( ( normℎ ‘ 𝑥 ) ∈ ℝ ∧ ( normℎ ‘ 𝑦 ) ∈ ℝ ) → ( ( normℎ ‘ 𝑥 ) · ( normℎ ‘ 𝑦 ) ) = ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) |
29 |
24 19 28
|
syl2an |
⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( normℎ ‘ 𝑥 ) · ( normℎ ‘ 𝑦 ) ) = ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) |
30 |
23 29
|
breqtrd |
⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( abs ‘ ( 𝑥 ·ih 𝑦 ) ) ≤ ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) |
31 |
30
|
adantll |
⊢ ( ( ( 𝑇 ∈ LinFn ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) → ( abs ‘ ( 𝑥 ·ih 𝑦 ) ) ≤ ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) |
32 |
31
|
adantr |
⊢ ( ( ( ( 𝑇 ∈ LinFn ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) → ( abs ‘ ( 𝑥 ·ih 𝑦 ) ) ≤ ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) |
33 |
22 32
|
eqbrtrd |
⊢ ( ( ( ( 𝑇 ∈ LinFn ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) → ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) |
34 |
33
|
ex |
⊢ ( ( ( 𝑇 ∈ LinFn ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) → ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) ) |
35 |
34
|
an32s |
⊢ ( ( ( 𝑇 ∈ LinFn ∧ 𝑦 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) → ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) ) |
36 |
35
|
ralimdva |
⊢ ( ( 𝑇 ∈ LinFn ∧ 𝑦 ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) → ∀ 𝑥 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) ) |
37 |
|
oveq1 |
⊢ ( 𝑧 = ( normℎ ‘ 𝑦 ) → ( 𝑧 · ( normℎ ‘ 𝑥 ) ) = ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) |
38 |
37
|
breq2d |
⊢ ( 𝑧 = ( normℎ ‘ 𝑦 ) → ( ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝑧 · ( normℎ ‘ 𝑥 ) ) ↔ ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) ) |
39 |
38
|
ralbidv |
⊢ ( 𝑧 = ( normℎ ‘ 𝑦 ) → ( ∀ 𝑥 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝑧 · ( normℎ ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) ) |
40 |
39
|
rspcev |
⊢ ( ( ( normℎ ‘ 𝑦 ) ∈ ℝ ∧ ∀ 𝑥 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝑧 · ( normℎ ‘ 𝑥 ) ) ) |
41 |
20 36 40
|
syl6an |
⊢ ( ( 𝑇 ∈ LinFn ∧ 𝑦 ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝑧 · ( normℎ ‘ 𝑥 ) ) ) ) |
42 |
41
|
rexlimdva |
⊢ ( 𝑇 ∈ LinFn → ( ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝑧 · ( normℎ ‘ 𝑥 ) ) ) ) |
43 |
|
lnfncon |
⊢ ( 𝑇 ∈ LinFn → ( 𝑇 ∈ ContFn ↔ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝑧 · ( normℎ ‘ 𝑥 ) ) ) ) |
44 |
42 43
|
sylibrd |
⊢ ( 𝑇 ∈ LinFn → ( ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) → 𝑇 ∈ ContFn ) ) |
45 |
18 44
|
impbid |
⊢ ( 𝑇 ∈ LinFn → ( 𝑇 ∈ ContFn ↔ ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) |
46 |
1 45
|
bitr3d |
⊢ ( 𝑇 ∈ LinFn → ( ( normfn ‘ 𝑇 ) ∈ ℝ ↔ ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) |