Step |
Hyp |
Ref |
Expression |
1 |
|
fveq1 |
⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( 𝑇 ‘ 𝑣 ) = ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑣 ) ) |
2 |
1
|
eqeq1d |
⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ( 𝑇 ‘ 𝑣 ) = ( 𝑣 ·ih 𝑤 ) ↔ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑣 ) = ( 𝑣 ·ih 𝑤 ) ) ) |
3 |
2
|
ralbidv |
⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ∀ 𝑣 ∈ ℋ ( 𝑇 ‘ 𝑣 ) = ( 𝑣 ·ih 𝑤 ) ↔ ∀ 𝑣 ∈ ℋ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑣 ) = ( 𝑣 ·ih 𝑤 ) ) ) |
4 |
3
|
reubidv |
⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ∃! 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( 𝑇 ‘ 𝑣 ) = ( 𝑣 ·ih 𝑤 ) ↔ ∃! 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑣 ) = ( 𝑣 ·ih 𝑤 ) ) ) |
5 |
|
inss1 |
⊢ ( LinFn ∩ ContFn ) ⊆ LinFn |
6 |
|
0lnfn |
⊢ ( ℋ × { 0 } ) ∈ LinFn |
7 |
|
0cnfn |
⊢ ( ℋ × { 0 } ) ∈ ContFn |
8 |
|
elin |
⊢ ( ( ℋ × { 0 } ) ∈ ( LinFn ∩ ContFn ) ↔ ( ( ℋ × { 0 } ) ∈ LinFn ∧ ( ℋ × { 0 } ) ∈ ContFn ) ) |
9 |
6 7 8
|
mpbir2an |
⊢ ( ℋ × { 0 } ) ∈ ( LinFn ∩ ContFn ) |
10 |
9
|
elimel |
⊢ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ ( LinFn ∩ ContFn ) |
11 |
5 10
|
sselii |
⊢ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ LinFn |
12 |
|
inss2 |
⊢ ( LinFn ∩ ContFn ) ⊆ ContFn |
13 |
12 10
|
sselii |
⊢ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ ContFn |
14 |
11 13
|
riesz4i |
⊢ ∃! 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑣 ) = ( 𝑣 ·ih 𝑤 ) |
15 |
4 14
|
dedth |
⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ∃! 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( 𝑇 ‘ 𝑣 ) = ( 𝑣 ·ih 𝑤 ) ) |