Metamath Proof Explorer

Theorem lnopeq0lem2

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

Ref Expression
Hypothesis lnopeq0.1 ⊢ 𝑇 ∈ LinOp
Assertion lnopeq0lem2 ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) = ( ( ( ( ( 𝑇 ‘ ( 𝐴 +ℎ 𝐵 ) ) ·ih ( 𝐴 +ℎ 𝐵 ) ) − ( ( 𝑇 ‘ ( 𝐴 −ℎ 𝐵 ) ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) + ( i · ( ( ( 𝑇 ‘ ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) ·ih ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( 𝑇 ‘ ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ·ih ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ) ) ) / 4 ) )

Proof

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