Metamath Proof Explorer

Theorem eigorth

Description: A necessary and sufficient condition (that holds when T is a Hermitian operator) for two eigenvectors A and B to be orthogonal. Generalization of Equation 1.31 of Hughes p. 49. (Contributed by NM, 23-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion eigorth ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) ∧ ( ( ( 𝑇 ‘ 𝐴 ) = ( 𝐶 ·ℎ 𝐴 ) ∧ ( 𝑇 ‘ 𝐵 ) = ( 𝐷 ·ℎ 𝐵 ) ) ∧ 𝐶 ≠ ( ∗ ‘ 𝐷 ) ) ) → ( ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) ↔ ( 𝐴 ·ih 𝐵 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( 𝑇 ‘ 𝐴 ) = ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) )
2 oveq2 ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( 𝐶 ·ℎ 𝐴 ) = ( 𝐶 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) )
3 1 2 eqeq12d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( 𝑇 ‘ 𝐴 ) = ( 𝐶 ·ℎ 𝐴 ) ↔ ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( 𝐶 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ) )
4 3 anbi1d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( ( 𝑇 ‘ 𝐴 ) = ( 𝐶 ·ℎ 𝐴 ) ∧ ( 𝑇 ‘ 𝐵 ) = ( 𝐷 ·ℎ 𝐵 ) ) ↔ ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( 𝐶 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ 𝐵 ) = ( 𝐷 ·ℎ 𝐵 ) ) ) )
5 4 anbi1d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( ( ( 𝑇 ‘ 𝐴 ) = ( 𝐶 ·ℎ 𝐴 ) ∧ ( 𝑇 ‘ 𝐵 ) = ( 𝐷 ·ℎ 𝐵 ) ) ∧ 𝐶 ≠ ( ∗ ‘ 𝐷 ) ) ↔ ( ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( 𝐶 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ 𝐵 ) = ( 𝐷 ·ℎ 𝐵 ) ) ∧ 𝐶 ≠ ( ∗ ‘ 𝐷 ) ) ) )
6 oveq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih ( 𝑇 ‘ 𝐵 ) ) )
7 1 oveq1d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) = ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ·ih 𝐵 ) )
8 6 7 eqeq12d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ·ih 𝐵 ) ) )
9 oveq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( 𝐴 ·ih 𝐵 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih 𝐵 ) )
10 9 eqeq1d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( 𝐴 ·ih 𝐵 ) = 0 ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih 𝐵 ) = 0 ) )
11 8 10 bibi12d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) ↔ ( 𝐴 ·ih 𝐵 ) = 0 ) ↔ ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ·ih 𝐵 ) ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih 𝐵 ) = 0 ) ) )
12 5 11 imbi12d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( ( ( ( 𝑇 ‘ 𝐴 ) = ( 𝐶 ·ℎ 𝐴 ) ∧ ( 𝑇 ‘ 𝐵 ) = ( 𝐷 ·ℎ 𝐵 ) ) ∧ 𝐶 ≠ ( ∗ ‘ 𝐷 ) ) → ( ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) ↔ ( 𝐴 ·ih 𝐵 ) = 0 ) ) ↔ ( ( ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( 𝐶 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ 𝐵 ) = ( 𝐷 ·ℎ 𝐵 ) ) ∧ 𝐶 ≠ ( ∗ ‘ 𝐷 ) ) → ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ·ih 𝐵 ) ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih 𝐵 ) = 0 ) ) ) )
13 fveq2 ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( 𝑇 ‘ 𝐵 ) = ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) )
14 oveq2 ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( 𝐷 ·ℎ 𝐵 ) = ( 𝐷 ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) )
15 13 14 eqeq12d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( 𝑇 ‘ 𝐵 ) = ( 𝐷 ·ℎ 𝐵 ) ↔ ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = ( 𝐷 ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) )
16 15 anbi2d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( 𝐶 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ 𝐵 ) = ( 𝐷 ·ℎ 𝐵 ) ) ↔ ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( 𝐶 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = ( 𝐷 ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) ) )
17 16 anbi1d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( 𝐶 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ 𝐵 ) = ( 𝐷 ·ℎ 𝐵 ) ) ∧ 𝐶 ≠ ( ∗ ‘ 𝐷 ) ) ↔ ( ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( 𝐶 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = ( 𝐷 ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) ∧ 𝐶 ≠ ( ∗ ‘ 𝐷 ) ) ) )
18 13 oveq2d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih ( 𝑇 ‘ 𝐵 ) ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) )
19 oveq2 ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ·ih 𝐵 ) = ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) )
20 18 19 eqeq12d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ·ih 𝐵 ) ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) = ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) )
21 oveq2 ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih 𝐵 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) )
22 21 eqeq1d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih 𝐵 ) = 0 ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = 0 ) )
23 20 22 bibi12d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ·ih 𝐵 ) ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih 𝐵 ) = 0 ) ↔ ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) = ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = 0 ) ) )
24 17 23 imbi12d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( ( ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( 𝐶 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ 𝐵 ) = ( 𝐷 ·ℎ 𝐵 ) ) ∧ 𝐶 ≠ ( ∗ ‘ 𝐷 ) ) → ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ·ih 𝐵 ) ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih 𝐵 ) = 0 ) ) ↔ ( ( ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( 𝐶 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = ( 𝐷 ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) ∧ 𝐶 ≠ ( ∗ ‘ 𝐷 ) ) → ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) = ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = 0 ) ) ) )
25 oveq1 ⊢ ( 𝐶 = if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) → ( 𝐶 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) )
26 25 eqeq2d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) → ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( 𝐶 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ↔ ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ) )
27 26 anbi1d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) → ( ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( 𝐶 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = ( 𝐷 ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) ↔ ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = ( 𝐷 ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) ) )
28 neeq1 ⊢ ( 𝐶 = if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) → ( 𝐶 ≠ ( ∗ ‘ 𝐷 ) ↔ if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ≠ ( ∗ ‘ 𝐷 ) ) )
29 27 28 anbi12d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) → ( ( ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( 𝐶 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = ( 𝐷 ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) ∧ 𝐶 ≠ ( ∗ ‘ 𝐷 ) ) ↔ ( ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = ( 𝐷 ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) ∧ if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ≠ ( ∗ ‘ 𝐷 ) ) ) )
30 29 imbi1d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) → ( ( ( ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( 𝐶 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = ( 𝐷 ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) ∧ 𝐶 ≠ ( ∗ ‘ 𝐷 ) ) → ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) = ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = 0 ) ) ↔ ( ( ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = ( 𝐷 ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) ∧ if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ≠ ( ∗ ‘ 𝐷 ) ) → ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) = ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = 0 ) ) ) )
31 oveq1 ⊢ ( 𝐷 = if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) → ( 𝐷 ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = ( if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) )
32 31 eqeq2d ⊢ ( 𝐷 = if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) → ( ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = ( 𝐷 ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ↔ ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = ( if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) )
33 32 anbi2d ⊢ ( 𝐷 = if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) → ( ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = ( 𝐷 ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) ↔ ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = ( if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) ) )
34 fveq2 ⊢ ( 𝐷 = if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) → ( ∗ ‘ 𝐷 ) = ( ∗ ‘ if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) )
35 34 neeq2d ⊢ ( 𝐷 = if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) → ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ≠ ( ∗ ‘ 𝐷 ) ↔ if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ≠ ( ∗ ‘ if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) ) )
36 33 35 anbi12d ⊢ ( 𝐷 = if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) → ( ( ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = ( 𝐷 ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) ∧ if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ≠ ( ∗ ‘ 𝐷 ) ) ↔ ( ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = ( if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) ∧ if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ≠ ( ∗ ‘ if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) ) ) )
37 36 imbi1d ⊢ ( 𝐷 = if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) → ( ( ( ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = ( 𝐷 ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) ∧ if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ≠ ( ∗ ‘ 𝐷 ) ) → ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) = ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = 0 ) ) ↔ ( ( ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = ( if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) ∧ if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ≠ ( ∗ ‘ if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) ) → ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) = ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = 0 ) ) ) )
38 ifhvhv0 ⊢ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ∈ ℋ
39 ifhvhv0 ⊢ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ∈ ℋ
40 0cn ⊢ 0 ∈ ℂ
41 40 elimel ⊢ if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ∈ ℂ
42 40 elimel ⊢ if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ∈ ℂ
43 38 39 41 42 eigorthi ⊢ ( ( ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ∧ ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = ( if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ·ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) ∧ if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ≠ ( ∗ ‘ if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) ) → ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih ( 𝑇 ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) = ( ( 𝑇 ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) = 0 ) )
44 12 24 30 37 43 dedth4h ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( ( 𝑇 ‘ 𝐴 ) = ( 𝐶 ·ℎ 𝐴 ) ∧ ( 𝑇 ‘ 𝐵 ) = ( 𝐷 ·ℎ 𝐵 ) ) ∧ 𝐶 ≠ ( ∗ ‘ 𝐷 ) ) → ( ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) ↔ ( 𝐴 ·ih 𝐵 ) = 0 ) ) )
45 44 imp ⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) ∧ ( ( ( 𝑇 ‘ 𝐴 ) = ( 𝐶 ·ℎ 𝐴 ) ∧ ( 𝑇 ‘ 𝐵 ) = ( 𝐷 ·ℎ 𝐵 ) ) ∧ 𝐶 ≠ ( ∗ ‘ 𝐷 ) ) ) → ( ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) ↔ ( 𝐴 ·ih 𝐵 ) = 0 ) )