| Step | Hyp | Ref
| Expression |
| 1 | | ax-hv0cl 31022 |
. . 3
⊢
0ℎ ∈ ℋ |
| 2 | | nlelsh.1 |
. . . 4
⊢ 𝑇 ∈ LinFn |
| 3 | 2 | lnfn0i 32061 |
. . 3
⊢ (𝑇‘0ℎ) =
0 |
| 4 | 2 | lnfnfi 32060 |
. . . 4
⊢ 𝑇:
ℋ⟶ℂ |
| 5 | | elnlfn 31947 |
. . . 4
⊢ (𝑇: ℋ⟶ℂ →
(0ℎ ∈ (null‘𝑇) ↔ (0ℎ ∈
ℋ ∧ (𝑇‘0ℎ) =
0))) |
| 6 | 4, 5 | ax-mp 5 |
. . 3
⊢
(0ℎ ∈ (null‘𝑇) ↔ (0ℎ ∈
ℋ ∧ (𝑇‘0ℎ) =
0)) |
| 7 | 1, 3, 6 | mpbir2an 711 |
. 2
⊢
0ℎ ∈ (null‘𝑇) |
| 8 | | nlfnval 31900 |
. . . . . . . . . 10
⊢ (𝑇: ℋ⟶ℂ →
(null‘𝑇) = (◡𝑇 “ {0})) |
| 9 | 4, 8 | ax-mp 5 |
. . . . . . . . 9
⊢
(null‘𝑇) =
(◡𝑇 “ {0}) |
| 10 | | cnvimass 6100 |
. . . . . . . . 9
⊢ (◡𝑇 “ {0}) ⊆ dom 𝑇 |
| 11 | 9, 10 | eqsstri 4030 |
. . . . . . . 8
⊢
(null‘𝑇)
⊆ dom 𝑇 |
| 12 | 4 | fdmi 6747 |
. . . . . . . 8
⊢ dom 𝑇 = ℋ |
| 13 | 11, 12 | sseqtri 4032 |
. . . . . . 7
⊢
(null‘𝑇)
⊆ ℋ |
| 14 | 13 | sseli 3979 |
. . . . . 6
⊢ (𝑥 ∈ (null‘𝑇) → 𝑥 ∈ ℋ) |
| 15 | 13 | sseli 3979 |
. . . . . 6
⊢ (𝑦 ∈ (null‘𝑇) → 𝑦 ∈ ℋ) |
| 16 | | hvaddcl 31031 |
. . . . . 6
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥 +ℎ 𝑦) ∈
ℋ) |
| 17 | 14, 15, 16 | syl2an 596 |
. . . . 5
⊢ ((𝑥 ∈ (null‘𝑇) ∧ 𝑦 ∈ (null‘𝑇)) → (𝑥 +ℎ 𝑦) ∈ ℋ) |
| 18 | 2 | lnfnaddi 32062 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑇‘(𝑥 +ℎ 𝑦)) = ((𝑇‘𝑥) + (𝑇‘𝑦))) |
| 19 | 14, 15, 18 | syl2an 596 |
. . . . . . 7
⊢ ((𝑥 ∈ (null‘𝑇) ∧ 𝑦 ∈ (null‘𝑇)) → (𝑇‘(𝑥 +ℎ 𝑦)) = ((𝑇‘𝑥) + (𝑇‘𝑦))) |
| 20 | | elnlfn 31947 |
. . . . . . . . . 10
⊢ (𝑇: ℋ⟶ℂ →
(𝑥 ∈ (null‘𝑇) ↔ (𝑥 ∈ ℋ ∧ (𝑇‘𝑥) = 0))) |
| 21 | 4, 20 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑥 ∈ (null‘𝑇) ↔ (𝑥 ∈ ℋ ∧ (𝑇‘𝑥) = 0)) |
| 22 | 21 | simprbi 496 |
. . . . . . . 8
⊢ (𝑥 ∈ (null‘𝑇) → (𝑇‘𝑥) = 0) |
| 23 | | elnlfn 31947 |
. . . . . . . . . 10
⊢ (𝑇: ℋ⟶ℂ →
(𝑦 ∈ (null‘𝑇) ↔ (𝑦 ∈ ℋ ∧ (𝑇‘𝑦) = 0))) |
| 24 | 4, 23 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑦 ∈ (null‘𝑇) ↔ (𝑦 ∈ ℋ ∧ (𝑇‘𝑦) = 0)) |
| 25 | 24 | simprbi 496 |
. . . . . . . 8
⊢ (𝑦 ∈ (null‘𝑇) → (𝑇‘𝑦) = 0) |
| 26 | 22, 25 | oveqan12d 7450 |
. . . . . . 7
⊢ ((𝑥 ∈ (null‘𝑇) ∧ 𝑦 ∈ (null‘𝑇)) → ((𝑇‘𝑥) + (𝑇‘𝑦)) = (0 + 0)) |
| 27 | 19, 26 | eqtrd 2777 |
. . . . . 6
⊢ ((𝑥 ∈ (null‘𝑇) ∧ 𝑦 ∈ (null‘𝑇)) → (𝑇‘(𝑥 +ℎ 𝑦)) = (0 + 0)) |
| 28 | | 00id 11436 |
. . . . . 6
⊢ (0 + 0) =
0 |
| 29 | 27, 28 | eqtrdi 2793 |
. . . . 5
⊢ ((𝑥 ∈ (null‘𝑇) ∧ 𝑦 ∈ (null‘𝑇)) → (𝑇‘(𝑥 +ℎ 𝑦)) = 0) |
| 30 | | elnlfn 31947 |
. . . . . 6
⊢ (𝑇: ℋ⟶ℂ →
((𝑥 +ℎ
𝑦) ∈ (null‘𝑇) ↔ ((𝑥 +ℎ 𝑦) ∈ ℋ ∧ (𝑇‘(𝑥 +ℎ 𝑦)) = 0))) |
| 31 | 4, 30 | ax-mp 5 |
. . . . 5
⊢ ((𝑥 +ℎ 𝑦) ∈ (null‘𝑇) ↔ ((𝑥 +ℎ 𝑦) ∈ ℋ ∧ (𝑇‘(𝑥 +ℎ 𝑦)) = 0)) |
| 32 | 17, 29, 31 | sylanbrc 583 |
. . . 4
⊢ ((𝑥 ∈ (null‘𝑇) ∧ 𝑦 ∈ (null‘𝑇)) → (𝑥 +ℎ 𝑦) ∈ (null‘𝑇)) |
| 33 | 32 | rgen2 3199 |
. . 3
⊢
∀𝑥 ∈
(null‘𝑇)∀𝑦 ∈ (null‘𝑇)(𝑥 +ℎ 𝑦) ∈ (null‘𝑇) |
| 34 | | hvmulcl 31032 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑥
·ℎ 𝑦) ∈ ℋ) |
| 35 | 15, 34 | sylan2 593 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ (null‘𝑇)) → (𝑥 ·ℎ 𝑦) ∈
ℋ) |
| 36 | 2 | lnfnmuli 32063 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑇‘(𝑥 ·ℎ 𝑦)) = (𝑥 · (𝑇‘𝑦))) |
| 37 | 15, 36 | sylan2 593 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ (null‘𝑇)) → (𝑇‘(𝑥 ·ℎ 𝑦)) = (𝑥 · (𝑇‘𝑦))) |
| 38 | 25 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑦 ∈ (null‘𝑇) → (𝑥 · (𝑇‘𝑦)) = (𝑥 · 0)) |
| 39 | | mul01 11440 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ → (𝑥 · 0) =
0) |
| 40 | 38, 39 | sylan9eqr 2799 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ (null‘𝑇)) → (𝑥 · (𝑇‘𝑦)) = 0) |
| 41 | 37, 40 | eqtrd 2777 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ (null‘𝑇)) → (𝑇‘(𝑥 ·ℎ 𝑦)) = 0) |
| 42 | | elnlfn 31947 |
. . . . . 6
⊢ (𝑇: ℋ⟶ℂ →
((𝑥
·ℎ 𝑦) ∈ (null‘𝑇) ↔ ((𝑥 ·ℎ 𝑦) ∈ ℋ ∧ (𝑇‘(𝑥 ·ℎ 𝑦)) = 0))) |
| 43 | 4, 42 | ax-mp 5 |
. . . . 5
⊢ ((𝑥
·ℎ 𝑦) ∈ (null‘𝑇) ↔ ((𝑥 ·ℎ 𝑦) ∈ ℋ ∧ (𝑇‘(𝑥 ·ℎ 𝑦)) = 0)) |
| 44 | 35, 41, 43 | sylanbrc 583 |
. . . 4
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ (null‘𝑇)) → (𝑥 ·ℎ 𝑦) ∈ (null‘𝑇)) |
| 45 | 44 | rgen2 3199 |
. . 3
⊢
∀𝑥 ∈
ℂ ∀𝑦 ∈
(null‘𝑇)(𝑥
·ℎ 𝑦) ∈ (null‘𝑇) |
| 46 | 33, 45 | pm3.2i 470 |
. 2
⊢
(∀𝑥 ∈
(null‘𝑇)∀𝑦 ∈ (null‘𝑇)(𝑥 +ℎ 𝑦) ∈ (null‘𝑇) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (null‘𝑇)(𝑥 ·ℎ 𝑦) ∈ (null‘𝑇)) |
| 47 | | issh3 31238 |
. . 3
⊢
((null‘𝑇)
⊆ ℋ → ((null‘𝑇) ∈ Sℋ
↔ (0ℎ ∈ (null‘𝑇) ∧ (∀𝑥 ∈ (null‘𝑇)∀𝑦 ∈ (null‘𝑇)(𝑥 +ℎ 𝑦) ∈ (null‘𝑇) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (null‘𝑇)(𝑥 ·ℎ 𝑦) ∈ (null‘𝑇))))) |
| 48 | 13, 47 | ax-mp 5 |
. 2
⊢
((null‘𝑇)
∈ Sℋ ↔ (0ℎ ∈
(null‘𝑇) ∧
(∀𝑥 ∈
(null‘𝑇)∀𝑦 ∈ (null‘𝑇)(𝑥 +ℎ 𝑦) ∈ (null‘𝑇) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (null‘𝑇)(𝑥 ·ℎ 𝑦) ∈ (null‘𝑇)))) |
| 49 | 7, 46, 48 | mpbir2an 711 |
1
⊢
(null‘𝑇)
∈ Sℋ |