Metamath Proof Explorer

Theorem lnopeq0lem2

Description: Lemma for lnopeq0i . (Contributed by NM, 26-Jul-2006) (New usage is discouraged.)

Ref Expression
Hypothesis lnopeq0.1 ⊢ T ∈ LinOp
Assertion lnopeq0lem2 ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A ⋅ ih B = T ⁡ A + ℎ B ⋅ ih A + ℎ B - T ⁡ A - ℎ B ⋅ ih A - ℎ B + i ⁢ T ⁡ A + ℎ i ⋅ ℎ B ⋅ ih A + ℎ i ⋅ ℎ B − T ⁡ A - ℎ i ⋅ ℎ B ⋅ ih A - ℎ i ⋅ ℎ B 4

Proof

Step Hyp Ref Expression
1 lnopeq0.1 ⊢ T ∈ LinOp
2 fveq2 ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A = T ⁡ if A ∈ ℋ A 0 ℎ
3 2 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A ⋅ ih B = T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih B
4 fvoveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A + ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ + ℎ B
5 oveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A + ℎ B = if A ∈ ℋ A 0 ℎ + ℎ B
6 4 5 oveq12d ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A + ℎ B ⋅ ih A + ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ + ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ B
7 fvoveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A - ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ - ℎ B
8 oveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A - ℎ B = if A ∈ ℋ A 0 ℎ - ℎ B
9 7 8 oveq12d ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A - ℎ B ⋅ ih A - ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ - ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ B
10 6 9 oveq12d ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A + ℎ B ⋅ ih A + ℎ B − T ⁡ A - ℎ B ⋅ ih A - ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ + ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ B − T ⁡ if A ∈ ℋ A 0 ℎ - ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ B
11 fvoveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A + ℎ i ⋅ ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B
12 oveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A + ℎ i ⋅ ℎ B = if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B
13 11 12 oveq12d ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A + ℎ i ⋅ ℎ B ⋅ ih A + ℎ i ⋅ ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B
14 fvoveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A - ℎ i ⋅ ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B
15 oveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A - ℎ i ⋅ ℎ B = if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B
16 14 15 oveq12d ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A - ℎ i ⋅ ℎ B ⋅ ih A - ℎ i ⋅ ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B
17 13 16 oveq12d ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A + ℎ i ⋅ ℎ B ⋅ ih A + ℎ i ⋅ ℎ B − T ⁡ A - ℎ i ⋅ ℎ B ⋅ ih A - ℎ i ⋅ ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B − T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B
18 17 oveq2d ⊢ A = if A ∈ ℋ A 0 ℎ → i ⁢ T ⁡ A + ℎ i ⋅ ℎ B ⋅ ih A + ℎ i ⋅ ℎ B − T ⁡ A - ℎ i ⋅ ℎ B ⋅ ih A - ℎ i ⋅ ℎ B = i ⁢ T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B − T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B
19 10 18 oveq12d ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A + ℎ B ⋅ ih A + ℎ B - T ⁡ A - ℎ B ⋅ ih A - ℎ B + i ⁢ T ⁡ A + ℎ i ⋅ ℎ B ⋅ ih A + ℎ i ⋅ ℎ B − T ⁡ A - ℎ i ⋅ ℎ B ⋅ ih A - ℎ i ⋅ ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ + ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ B - T ⁡ if A ∈ ℋ A 0 ℎ - ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ B + i ⁢ T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B − T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B
20 19 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A + ℎ B ⋅ ih A + ℎ B - T ⁡ A - ℎ B ⋅ ih A - ℎ B + i ⁢ T ⁡ A + ℎ i ⋅ ℎ B ⋅ ih A + ℎ i ⋅ ℎ B − T ⁡ A - ℎ i ⋅ ℎ B ⋅ ih A - ℎ i ⋅ ℎ B 4 = T ⁡ if A ∈ ℋ A 0 ℎ + ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ B - T ⁡ if A ∈ ℋ A 0 ℎ - ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ B + i ⁢ T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B − T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B 4
21 3 20 eqeq12d ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A ⋅ ih B = T ⁡ A + ℎ B ⋅ ih A + ℎ B - T ⁡ A - ℎ B ⋅ ih A - ℎ B + i ⁢ T ⁡ A + ℎ i ⋅ ℎ B ⋅ ih A + ℎ i ⋅ ℎ B − T ⁡ A - ℎ i ⋅ ℎ B ⋅ ih A - ℎ i ⋅ ℎ B 4 ↔ T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih B = T ⁡ if A ∈ ℋ A 0 ℎ + ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ B - T ⁡ if A ∈ ℋ A 0 ℎ - ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ B + i ⁢ T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B − T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B 4
22 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih B = T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ
23 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ + ℎ B = if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ
24 23 fveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → T ⁡ if A ∈ ℋ A 0 ℎ + ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ
25 24 23 oveq12d ⊢ B = if B ∈ ℋ B 0 ℎ → T ⁡ if A ∈ ℋ A 0 ℎ + ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ
26 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ B = if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
27 26 fveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → T ⁡ if A ∈ ℋ A 0 ℎ - ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
28 27 26 oveq12d ⊢ B = if B ∈ ℋ B 0 ℎ → T ⁡ if A ∈ ℋ A 0 ℎ - ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
29 25 28 oveq12d ⊢ B = if B ∈ ℋ B 0 ℎ → T ⁡ if A ∈ ℋ A 0 ℎ + ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ B − T ⁡ if A ∈ ℋ A 0 ℎ - ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ − T ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
30 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → i ⋅ ℎ B = i ⋅ ℎ if B ∈ ℋ B 0 ℎ
31 30 oveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B = if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ
32 31 fveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ
33 32 31 oveq12d ⊢ B = if B ∈ ℋ B 0 ℎ → T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ
34 30 oveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B = if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ
35 34 fveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ
36 35 34 oveq12d ⊢ B = if B ∈ ℋ B 0 ℎ → T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ
37 33 36 oveq12d ⊢ B = if B ∈ ℋ B 0 ℎ → T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B − T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ − T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ
38 37 oveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → i ⁢ T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B − T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B = i ⁢ T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ − T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ
39 29 38 oveq12d ⊢ B = if B ∈ ℋ B 0 ℎ → T ⁡ if A ∈ ℋ A 0 ℎ + ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ B - T ⁡ if A ∈ ℋ A 0 ℎ - ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ B + i ⁢ T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B − T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B = T ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ - T ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ + i ⁢ T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ − T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ
40 39 oveq1d ⊢ B = if B ∈ ℋ B 0 ℎ → T ⁡ if A ∈ ℋ A 0 ℎ + ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ B - T ⁡ if A ∈ ℋ A 0 ℎ - ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ B + i ⁢ T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B − T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B 4 = T ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ - T ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ + i ⁢ T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ − T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ 4
41 22 40 eqeq12d ⊢ B = if B ∈ ℋ B 0 ℎ → T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih B = T ⁡ if A ∈ ℋ A 0 ℎ + ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ B - T ⁡ if A ∈ ℋ A 0 ℎ - ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ B + i ⁢ T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B − T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B 4 ↔ T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ = T ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ - T ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ + i ⁢ T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ − T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ 4
42 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
43 ifhvhv0 ⊢ if B ∈ ℋ B 0 ℎ ∈ ℋ
44 1 42 43 lnopeq0lem1 ⊢ T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ = T ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ - T ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ + i ⁢ T ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ − T ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ 4
45 21 41 44 dedth2h ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A ⋅ ih B = T ⁡ A + ℎ B ⋅ ih A + ℎ B - T ⁡ A - ℎ B ⋅ ih A - ℎ B + i ⁢ T ⁡ A + ℎ i ⋅ ℎ B ⋅ ih A + ℎ i ⋅ ℎ B − T ⁡ A - ℎ i ⋅ ℎ B ⋅ ih A - ℎ i ⋅ ℎ B 4