Step | Hyp | Ref
| Expression |
1 | | nlfnval 28124 |
. . . . . 6
⊢ (𝑇: ℋ⟶ℂ →
(null‘𝑇) = (◡𝑇 “ {0})) |
2 | | cnvimass 5404 |
. . . . . 6
⊢ (◡𝑇 “ {0}) ⊆ dom 𝑇 |
3 | 1, 2 | syl6eqss 3618 |
. . . . 5
⊢ (𝑇: ℋ⟶ℂ →
(null‘𝑇) ⊆ dom
𝑇) |
4 | | fdm 5964 |
. . . . 5
⊢ (𝑇: ℋ⟶ℂ →
dom 𝑇 =
ℋ) |
5 | 3, 4 | sseqtrd 3604 |
. . . 4
⊢ (𝑇: ℋ⟶ℂ →
(null‘𝑇) ⊆
ℋ) |
6 | 5 | sseld 3567 |
. . 3
⊢ (𝑇: ℋ⟶ℂ →
(𝐴 ∈ (null‘𝑇) → 𝐴 ∈ ℋ)) |
7 | 6 | pm4.71rd 665 |
. 2
⊢ (𝑇: ℋ⟶ℂ →
(𝐴 ∈ (null‘𝑇) ↔ (𝐴 ∈ ℋ ∧ 𝐴 ∈ (null‘𝑇)))) |
8 | 1 | eleq2d 2673 |
. . . . 5
⊢ (𝑇: ℋ⟶ℂ →
(𝐴 ∈ (null‘𝑇) ↔ 𝐴 ∈ (◡𝑇 “ {0}))) |
9 | 8 | adantr 480 |
. . . 4
⊢ ((𝑇: ℋ⟶ℂ ∧
𝐴 ∈ ℋ) →
(𝐴 ∈ (null‘𝑇) ↔ 𝐴 ∈ (◡𝑇 “ {0}))) |
10 | | ffn 5958 |
. . . . 5
⊢ (𝑇: ℋ⟶ℂ →
𝑇 Fn
ℋ) |
11 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑥 ∈ (◡𝑇 “ {0}) ↔ 𝐴 ∈ (◡𝑇 “ {0}))) |
12 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝑇‘𝑥) = (𝑇‘𝐴)) |
13 | 12 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → ((𝑇‘𝑥) = 0 ↔ (𝑇‘𝐴) = 0)) |
14 | 11, 13 | bibi12d 334 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝑥 ∈ (◡𝑇 “ {0}) ↔ (𝑇‘𝑥) = 0) ↔ (𝐴 ∈ (◡𝑇 “ {0}) ↔ (𝑇‘𝐴) = 0))) |
15 | 14 | imbi2d 329 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑇 Fn ℋ → (𝑥 ∈ (◡𝑇 “ {0}) ↔ (𝑇‘𝑥) = 0)) ↔ (𝑇 Fn ℋ → (𝐴 ∈ (◡𝑇 “ {0}) ↔ (𝑇‘𝐴) = 0)))) |
16 | | fnbrfvb 6146 |
. . . . . . . 8
⊢ ((𝑇 Fn ℋ ∧ 𝑥 ∈ ℋ) → ((𝑇‘𝑥) = 0 ↔ 𝑥𝑇0)) |
17 | | 0cn 9911 |
. . . . . . . . 9
⊢ 0 ∈
ℂ |
18 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
19 | 18 | eliniseg 5413 |
. . . . . . . . 9
⊢ (0 ∈
ℂ → (𝑥 ∈
(◡𝑇 “ {0}) ↔ 𝑥𝑇0)) |
20 | 17, 19 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑥 ∈ (◡𝑇 “ {0}) ↔ 𝑥𝑇0) |
21 | 16, 20 | syl6rbbr 278 |
. . . . . . 7
⊢ ((𝑇 Fn ℋ ∧ 𝑥 ∈ ℋ) → (𝑥 ∈ (◡𝑇 “ {0}) ↔ (𝑇‘𝑥) = 0)) |
22 | 21 | expcom 450 |
. . . . . 6
⊢ (𝑥 ∈ ℋ → (𝑇 Fn ℋ → (𝑥 ∈ (◡𝑇 “ {0}) ↔ (𝑇‘𝑥) = 0))) |
23 | 15, 22 | vtoclga 3245 |
. . . . 5
⊢ (𝐴 ∈ ℋ → (𝑇 Fn ℋ → (𝐴 ∈ (◡𝑇 “ {0}) ↔ (𝑇‘𝐴) = 0))) |
24 | 10, 23 | mpan9 485 |
. . . 4
⊢ ((𝑇: ℋ⟶ℂ ∧
𝐴 ∈ ℋ) →
(𝐴 ∈ (◡𝑇 “ {0}) ↔ (𝑇‘𝐴) = 0)) |
25 | 9, 24 | bitrd 267 |
. . 3
⊢ ((𝑇: ℋ⟶ℂ ∧
𝐴 ∈ ℋ) →
(𝐴 ∈ (null‘𝑇) ↔ (𝑇‘𝐴) = 0)) |
26 | 25 | pm5.32da 671 |
. 2
⊢ (𝑇: ℋ⟶ℂ →
((𝐴 ∈ ℋ ∧
𝐴 ∈ (null‘𝑇)) ↔ (𝐴 ∈ ℋ ∧ (𝑇‘𝐴) = 0))) |
27 | 7, 26 | bitrd 267 |
1
⊢ (𝑇: ℋ⟶ℂ →
(𝐴 ∈ (null‘𝑇) ↔ (𝐴 ∈ ℋ ∧ (𝑇‘𝐴) = 0))) |