Metamath Proof Explorer

Theorem lnopeq0i

Description: A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01i for arbitrary operators, when the operator is linear we need to consider only the values of the quadratic form ( Tx ) .ih x ) . (Contributed by NM, 26-Jul-2006) (New usage is discouraged.)

Ref Expression
Hypothesis lnopeq0.1 ⊢ 𝑇 ∈ LinOp
Assertion lnopeq0i ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ↔ 𝑇 = 0hop )

Proof

Step Hyp Ref Expression
1 lnopeq0.1 ⊢ 𝑇 ∈ LinOp
2 1 lnopeq0lem2 ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑧 ) = ( ( ( ( ( 𝑇 ‘ ( 𝑦 +ℎ 𝑧 ) ) ·ih ( 𝑦 +ℎ 𝑧 ) ) − ( ( 𝑇 ‘ ( 𝑦 −ℎ 𝑧 ) ) ·ih ( 𝑦 −ℎ 𝑧 ) ) ) + ( i · ( ( ( 𝑇 ‘ ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) − ( ( 𝑇 ‘ ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ) ) ) / 4 ) )
3 2 adantl ⊢ ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑧 ) = ( ( ( ( ( 𝑇 ‘ ( 𝑦 +ℎ 𝑧 ) ) ·ih ( 𝑦 +ℎ 𝑧 ) ) − ( ( 𝑇 ‘ ( 𝑦 −ℎ 𝑧 ) ) ·ih ( 𝑦 −ℎ 𝑧 ) ) ) + ( i · ( ( ( 𝑇 ‘ ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) − ( ( 𝑇 ‘ ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ) ) ) / 4 ) )
4 hvaddcl ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑦 +ℎ 𝑧 ) ∈ ℋ )
5 fveq2 ⊢ ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ ( 𝑦 +ℎ 𝑧 ) ) )
6 id ⊢ ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 = ( 𝑦 +ℎ 𝑧 ) )
7 5 6 oveq12d ⊢ ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑇 ‘ ( 𝑦 +ℎ 𝑧 ) ) ·ih ( 𝑦 +ℎ 𝑧 ) ) )
8 7 eqeq1d ⊢ ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ↔ ( ( 𝑇 ‘ ( 𝑦 +ℎ 𝑧 ) ) ·ih ( 𝑦 +ℎ 𝑧 ) ) = 0 ) )
9 8 rspccva ⊢ ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ∧ ( 𝑦 +ℎ 𝑧 ) ∈ ℋ ) → ( ( 𝑇 ‘ ( 𝑦 +ℎ 𝑧 ) ) ·ih ( 𝑦 +ℎ 𝑧 ) ) = 0 )
10 4 9 sylan2 ⊢ ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( ( 𝑇 ‘ ( 𝑦 +ℎ 𝑧 ) ) ·ih ( 𝑦 +ℎ 𝑧 ) ) = 0 )
11 hvsubcl ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑦 −ℎ 𝑧 ) ∈ ℋ )
12 fveq2 ⊢ ( 𝑥 = ( 𝑦 −ℎ 𝑧 ) → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ ( 𝑦 −ℎ 𝑧 ) ) )
13 id ⊢ ( 𝑥 = ( 𝑦 −ℎ 𝑧 ) → 𝑥 = ( 𝑦 −ℎ 𝑧 ) )
14 12 13 oveq12d ⊢ ( 𝑥 = ( 𝑦 −ℎ 𝑧 ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑇 ‘ ( 𝑦 −ℎ 𝑧 ) ) ·ih ( 𝑦 −ℎ 𝑧 ) ) )
15 14 eqeq1d ⊢ ( 𝑥 = ( 𝑦 −ℎ 𝑧 ) → ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ↔ ( ( 𝑇 ‘ ( 𝑦 −ℎ 𝑧 ) ) ·ih ( 𝑦 −ℎ 𝑧 ) ) = 0 ) )
16 15 rspccva ⊢ ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ∧ ( 𝑦 −ℎ 𝑧 ) ∈ ℋ ) → ( ( 𝑇 ‘ ( 𝑦 −ℎ 𝑧 ) ) ·ih ( 𝑦 −ℎ 𝑧 ) ) = 0 )
17 11 16 sylan2 ⊢ ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( ( 𝑇 ‘ ( 𝑦 −ℎ 𝑧 ) ) ·ih ( 𝑦 −ℎ 𝑧 ) ) = 0 )
18 10 17 oveq12d ⊢ ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( ( ( 𝑇 ‘ ( 𝑦 +ℎ 𝑧 ) ) ·ih ( 𝑦 +ℎ 𝑧 ) ) − ( ( 𝑇 ‘ ( 𝑦 −ℎ 𝑧 ) ) ·ih ( 𝑦 −ℎ 𝑧 ) ) ) = ( 0 − 0 ) )
19 0m0e0 ⊢ ( 0 − 0 ) = 0
20 18 19 eqtrdi ⊢ ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( ( ( 𝑇 ‘ ( 𝑦 +ℎ 𝑧 ) ) ·ih ( 𝑦 +ℎ 𝑧 ) ) − ( ( 𝑇 ‘ ( 𝑦 −ℎ 𝑧 ) ) ·ih ( 𝑦 −ℎ 𝑧 ) ) ) = 0 )
21 ax-icn ⊢ i ∈ ℂ
22 hvmulcl ⊢ ( ( i ∈ ℂ ∧ 𝑧 ∈ ℋ ) → ( i ·ℎ 𝑧 ) ∈ ℋ )
23 21 22 mpan ⊢ ( 𝑧 ∈ ℋ → ( i ·ℎ 𝑧 ) ∈ ℋ )
24 hvaddcl ⊢ ( ( 𝑦 ∈ ℋ ∧ ( i ·ℎ 𝑧 ) ∈ ℋ ) → ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ∈ ℋ )
25 23 24 sylan2 ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ∈ ℋ )
26 fveq2 ⊢ ( 𝑥 = ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) )
27 id ⊢ ( 𝑥 = ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) → 𝑥 = ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) )
28 26 27 oveq12d ⊢ ( 𝑥 = ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑇 ‘ ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) )
29 28 eqeq1d ⊢ ( 𝑥 = ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) → ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ↔ ( ( 𝑇 ‘ ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) = 0 ) )
30 29 rspccva ⊢ ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ∧ ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ∈ ℋ ) → ( ( 𝑇 ‘ ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) = 0 )
31 25 30 sylan2 ⊢ ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( ( 𝑇 ‘ ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) = 0 )
32 hvsubcl ⊢ ( ( 𝑦 ∈ ℋ ∧ ( i ·ℎ 𝑧 ) ∈ ℋ ) → ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ∈ ℋ )
33 23 32 sylan2 ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ∈ ℋ )
34 fveq2 ⊢ ( 𝑥 = ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) )
35 id ⊢ ( 𝑥 = ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) → 𝑥 = ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) )
36 34 35 oveq12d ⊢ ( 𝑥 = ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑇 ‘ ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) )
37 36 eqeq1d ⊢ ( 𝑥 = ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) → ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ↔ ( ( 𝑇 ‘ ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) = 0 ) )
38 37 rspccva ⊢ ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ∧ ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ∈ ℋ ) → ( ( 𝑇 ‘ ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) = 0 )
39 33 38 sylan2 ⊢ ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( ( 𝑇 ‘ ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) = 0 )
40 31 39 oveq12d ⊢ ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( ( ( 𝑇 ‘ ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) − ( ( 𝑇 ‘ ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ) = ( 0 − 0 ) )
41 40 19 eqtrdi ⊢ ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( ( ( 𝑇 ‘ ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) − ( ( 𝑇 ‘ ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ) = 0 )
42 41 oveq2d ⊢ ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( i · ( ( ( 𝑇 ‘ ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) − ( ( 𝑇 ‘ ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ) ) = ( i · 0 ) )
43 it0e0 ⊢ ( i · 0 ) = 0
44 42 43 eqtrdi ⊢ ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( i · ( ( ( 𝑇 ‘ ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) − ( ( 𝑇 ‘ ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ) ) = 0 )
45 20 44 oveq12d ⊢ ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( ( ( ( 𝑇 ‘ ( 𝑦 +ℎ 𝑧 ) ) ·ih ( 𝑦 +ℎ 𝑧 ) ) − ( ( 𝑇 ‘ ( 𝑦 −ℎ 𝑧 ) ) ·ih ( 𝑦 −ℎ 𝑧 ) ) ) + ( i · ( ( ( 𝑇 ‘ ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) − ( ( 𝑇 ‘ ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ) ) ) = ( 0 + 0 ) )
46 00id ⊢ ( 0 + 0 ) = 0
47 45 46 eqtrdi ⊢ ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( ( ( ( 𝑇 ‘ ( 𝑦 +ℎ 𝑧 ) ) ·ih ( 𝑦 +ℎ 𝑧 ) ) − ( ( 𝑇 ‘ ( 𝑦 −ℎ 𝑧 ) ) ·ih ( 𝑦 −ℎ 𝑧 ) ) ) + ( i · ( ( ( 𝑇 ‘ ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) − ( ( 𝑇 ‘ ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ) ) ) = 0 )
48 47 oveq1d ⊢ ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( ( ( ( ( 𝑇 ‘ ( 𝑦 +ℎ 𝑧 ) ) ·ih ( 𝑦 +ℎ 𝑧 ) ) − ( ( 𝑇 ‘ ( 𝑦 −ℎ 𝑧 ) ) ·ih ( 𝑦 −ℎ 𝑧 ) ) ) + ( i · ( ( ( 𝑇 ‘ ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) − ( ( 𝑇 ‘ ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ) ) ) / 4 ) = ( 0 / 4 ) )
49 4cn ⊢ 4 ∈ ℂ
50 4ne0 ⊢ 4 ≠ 0
51 49 50 div0i ⊢ ( 0 / 4 ) = 0
52 48 51 eqtrdi ⊢ ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( ( ( ( ( 𝑇 ‘ ( 𝑦 +ℎ 𝑧 ) ) ·ih ( 𝑦 +ℎ 𝑧 ) ) − ( ( 𝑇 ‘ ( 𝑦 −ℎ 𝑧 ) ) ·ih ( 𝑦 −ℎ 𝑧 ) ) ) + ( i · ( ( ( 𝑇 ‘ ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 +ℎ ( i ·ℎ 𝑧 ) ) ) − ( ( 𝑇 ‘ ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ·ih ( 𝑦 −ℎ ( i ·ℎ 𝑧 ) ) ) ) ) ) / 4 ) = 0 )
53 3 52 eqtrd ⊢ ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑧 ) = 0 )
54 53 ralrimivva ⊢ ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 → ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑧 ) = 0 )
55 1 lnopfi ⊢ 𝑇 : ℋ ⟶ ℋ
56 55 ho01i ⊢ ( ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑧 ) = 0 ↔ 𝑇 = 0hop )
57 54 56 sylib ⊢ ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 → 𝑇 = 0hop )
58 fveq1 ⊢ ( 𝑇 = 0hop → ( 𝑇 ‘ 𝑥 ) = ( 0hop ‘ 𝑥 ) )
59 ho0val ⊢ ( 𝑥 ∈ ℋ → ( 0hop ‘ 𝑥 ) = 0ℎ )
60 58 59 sylan9eq ⊢ ( ( 𝑇 = 0hop ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ 𝑥 ) = 0ℎ )
61 60 oveq1d ⊢ ( ( 𝑇 = 0hop ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = ( 0ℎ ·ih 𝑥 ) )
62 hi01 ⊢ ( 𝑥 ∈ ℋ → ( 0ℎ ·ih 𝑥 ) = 0 )
63 62 adantl ⊢ ( ( 𝑇 = 0hop ∧ 𝑥 ∈ ℋ ) → ( 0ℎ ·ih 𝑥 ) = 0 )
64 61 63 eqtrd ⊢ ( ( 𝑇 = 0hop ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 )
65 64 ralrimiva ⊢ ( 𝑇 = 0hop → ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 )
66 57 65 impbii ⊢ ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = 0 ↔ 𝑇 = 0hop )