1 ax-hv0cl 21638 . . 3 ⊢ 0ℎ ∈ ℋ
2 nlelch.1 . . . . . . 7 ⊢ 𝑇 ∈ LinFn
3 2 lnfnfi 22676 . . . . . 6 ⊢ 𝑇: ℋ⟶ℂ
4 fveq2 5563 . . . . . . . . 9 ⊢ ((⊥‘(null‘𝑇)) = 0ℋ → (⊥‘(⊥‘(null‘𝑇))) = (⊥‘0ℋ))
5 nlelch.2 . . . . . . . . . . 11 ⊢ 𝑇 ∈ ConFn
6 2, 5 nlelchi 22696 . . . . . . . . . 10 ⊢ (null‘𝑇) ∈ Cℋ
7 6 ococi 22039 . . . . . . . . 9 ⊢ (⊥‘(⊥‘(null‘𝑇))) = (null‘𝑇)
8 choc0 21960 . . . . . . . . 9 ⊢ (⊥‘0ℋ) = ℋ
9 4, 7, 8 3eqtr3g 2371 . . . . . . . 8 ⊢ ((⊥‘(null‘𝑇)) = 0ℋ → (null‘𝑇) = ℋ)
10 9 eleq2d 2383 . . . . . . 7 ⊢ ((⊥‘(null‘𝑇)) = 0ℋ → (𝑣 ∈ (null‘𝑇) ↔ 𝑣 ∈ ℋ))