Metamath Proof Explorer

Theorem lnopeq0lem1

Description: Lemma for lnopeq0i . Apply the generalized polarization identity polid2i to the quadratic form ( ( Tx ) , x ) . (Contributed by NM, 26-Jul-2006) (New usage is discouraged.)

Ref Expression
Hypotheses lnopeq0.1 ⊢ 𝑇 ∈ LinOp
lnopeq0lem1.2 ⊢ 𝐴 ∈ ℋ
lnopeq0lem1.3 ⊢ 𝐵 ∈ ℋ
Assertion lnopeq0lem1 ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) = ( ( ( ( ( 𝑇 ‘ ( 𝐴 +ℎ 𝐵 ) ) ·ih ( 𝐴 +ℎ 𝐵 ) ) − ( ( 𝑇 ‘ ( 𝐴 −ℎ 𝐵 ) ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) + ( i · ( ( ( 𝑇 ‘ ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) ·ih ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( 𝑇 ‘ ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ·ih ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ) ) ) / 4 )

Proof

Step Hyp Ref Expression
1 lnopeq0.1 ⊢ 𝑇 ∈ LinOp
2 lnopeq0lem1.2 ⊢ 𝐴 ∈ ℋ
3 lnopeq0lem1.3 ⊢ 𝐵 ∈ ℋ
4 1 lnopfi ⊢ 𝑇 : ℋ ⟶ ℋ
5 4 ffvelcdmi ⊢ ( 𝐴 ∈ ℋ → ( 𝑇 ‘ 𝐴 ) ∈ ℋ )
6 2 5 ax-mp ⊢ ( 𝑇 ‘ 𝐴 ) ∈ ℋ
7 4 ffvelcdmi ⊢ ( 𝐵 ∈ ℋ → ( 𝑇 ‘ 𝐵 ) ∈ ℋ )
8 3 7 ax-mp ⊢ ( 𝑇 ‘ 𝐵 ) ∈ ℋ
9 6 3 8 2 polid2i ⊢ ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) = ( ( ( ( ( ( 𝑇 ‘ 𝐴 ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ·ih ( 𝐴 +ℎ 𝐵 ) ) − ( ( ( 𝑇 ‘ 𝐴 ) −ℎ ( 𝑇 ‘ 𝐵 ) ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) + ( i · ( ( ( ( 𝑇 ‘ 𝐴 ) +ℎ ( i ·ℎ ( 𝑇 ‘ 𝐵 ) ) ) ·ih ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( ( 𝑇 ‘ 𝐴 ) −ℎ ( i ·ℎ ( 𝑇 ‘ 𝐵 ) ) ) ·ih ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ) ) ) / 4 )
10 1 lnopaddi ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 +ℎ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) +ℎ ( 𝑇 ‘ 𝐵 ) ) )
11 2 3 10 mp2an ⊢ ( 𝑇 ‘ ( 𝐴 +ℎ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) +ℎ ( 𝑇 ‘ 𝐵 ) )
12 11 oveq1i ⊢ ( ( 𝑇 ‘ ( 𝐴 +ℎ 𝐵 ) ) ·ih ( 𝐴 +ℎ 𝐵 ) ) = ( ( ( 𝑇 ‘ 𝐴 ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ·ih ( 𝐴 +ℎ 𝐵 ) )
13 1 lnopsubi ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) −ℎ ( 𝑇 ‘ 𝐵 ) ) )
14 2 3 13 mp2an ⊢ ( 𝑇 ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) −ℎ ( 𝑇 ‘ 𝐵 ) )
15 14 oveq1i ⊢ ( ( 𝑇 ‘ ( 𝐴 −ℎ 𝐵 ) ) ·ih ( 𝐴 −ℎ 𝐵 ) ) = ( ( ( 𝑇 ‘ 𝐴 ) −ℎ ( 𝑇 ‘ 𝐵 ) ) ·ih ( 𝐴 −ℎ 𝐵 ) )
16 12 15 oveq12i ⊢ ( ( ( 𝑇 ‘ ( 𝐴 +ℎ 𝐵 ) ) ·ih ( 𝐴 +ℎ 𝐵 ) ) − ( ( 𝑇 ‘ ( 𝐴 −ℎ 𝐵 ) ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) = ( ( ( ( 𝑇 ‘ 𝐴 ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ·ih ( 𝐴 +ℎ 𝐵 ) ) − ( ( ( 𝑇 ‘ 𝐴 ) −ℎ ( 𝑇 ‘ 𝐵 ) ) ·ih ( 𝐴 −ℎ 𝐵 ) ) )
17 ax-icn ⊢ i ∈ ℂ
18 1 lnopaddmuli ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) = ( ( 𝑇 ‘ 𝐴 ) +ℎ ( i ·ℎ ( 𝑇 ‘ 𝐵 ) ) ) )
19 17 2 3 18 mp3an ⊢ ( 𝑇 ‘ ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) = ( ( 𝑇 ‘ 𝐴 ) +ℎ ( i ·ℎ ( 𝑇 ‘ 𝐵 ) ) )
20 19 oveq1i ⊢ ( ( 𝑇 ‘ ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) ·ih ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) = ( ( ( 𝑇 ‘ 𝐴 ) +ℎ ( i ·ℎ ( 𝑇 ‘ 𝐵 ) ) ) ·ih ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) )
21 1 lnopsubmuli ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) = ( ( 𝑇 ‘ 𝐴 ) −ℎ ( i ·ℎ ( 𝑇 ‘ 𝐵 ) ) ) )
22 17 2 3 21 mp3an ⊢ ( 𝑇 ‘ ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) = ( ( 𝑇 ‘ 𝐴 ) −ℎ ( i ·ℎ ( 𝑇 ‘ 𝐵 ) ) )
23 22 oveq1i ⊢ ( ( 𝑇 ‘ ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ·ih ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) = ( ( ( 𝑇 ‘ 𝐴 ) −ℎ ( i ·ℎ ( 𝑇 ‘ 𝐵 ) ) ) ·ih ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) )
24 20 23 oveq12i ⊢ ( ( ( 𝑇 ‘ ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) ·ih ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( 𝑇 ‘ ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ·ih ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ) = ( ( ( ( 𝑇 ‘ 𝐴 ) +ℎ ( i ·ℎ ( 𝑇 ‘ 𝐵 ) ) ) ·ih ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( ( 𝑇 ‘ 𝐴 ) −ℎ ( i ·ℎ ( 𝑇 ‘ 𝐵 ) ) ) ·ih ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) )
25 24 oveq2i ⊢ ( i · ( ( ( 𝑇 ‘ ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) ·ih ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( 𝑇 ‘ ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ·ih ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ) ) = ( i · ( ( ( ( 𝑇 ‘ 𝐴 ) +ℎ ( i ·ℎ ( 𝑇 ‘ 𝐵 ) ) ) ·ih ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( ( 𝑇 ‘ 𝐴 ) −ℎ ( i ·ℎ ( 𝑇 ‘ 𝐵 ) ) ) ·ih ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ) )
26 16 25 oveq12i ⊢ ( ( ( ( 𝑇 ‘ ( 𝐴 +ℎ 𝐵 ) ) ·ih ( 𝐴 +ℎ 𝐵 ) ) − ( ( 𝑇 ‘ ( 𝐴 −ℎ 𝐵 ) ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) + ( i · ( ( ( 𝑇 ‘ ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) ·ih ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( 𝑇 ‘ ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ·ih ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ) ) ) = ( ( ( ( ( 𝑇 ‘ 𝐴 ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ·ih ( 𝐴 +ℎ 𝐵 ) ) − ( ( ( 𝑇 ‘ 𝐴 ) −ℎ ( 𝑇 ‘ 𝐵 ) ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) + ( i · ( ( ( ( 𝑇 ‘ 𝐴 ) +ℎ ( i ·ℎ ( 𝑇 ‘ 𝐵 ) ) ) ·ih ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( ( 𝑇 ‘ 𝐴 ) −ℎ ( i ·ℎ ( 𝑇 ‘ 𝐵 ) ) ) ·ih ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ) ) )
27 26 oveq1i ⊢ ( ( ( ( ( 𝑇 ‘ ( 𝐴 +ℎ 𝐵 ) ) ·ih ( 𝐴 +ℎ 𝐵 ) ) − ( ( 𝑇 ‘ ( 𝐴 −ℎ 𝐵 ) ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) + ( i · ( ( ( 𝑇 ‘ ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) ·ih ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( 𝑇 ‘ ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ·ih ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ) ) ) / 4 ) = ( ( ( ( ( ( 𝑇 ‘ 𝐴 ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ·ih ( 𝐴 +ℎ 𝐵 ) ) − ( ( ( 𝑇 ‘ 𝐴 ) −ℎ ( 𝑇 ‘ 𝐵 ) ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) + ( i · ( ( ( ( 𝑇 ‘ 𝐴 ) +ℎ ( i ·ℎ ( 𝑇 ‘ 𝐵 ) ) ) ·ih ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( ( 𝑇 ‘ 𝐴 ) −ℎ ( i ·ℎ ( 𝑇 ‘ 𝐵 ) ) ) ·ih ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ) ) ) / 4 )
28 9 27 eqtr4i ⊢ ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) = ( ( ( ( ( 𝑇 ‘ ( 𝐴 +ℎ 𝐵 ) ) ·ih ( 𝐴 +ℎ 𝐵 ) ) − ( ( 𝑇 ‘ ( 𝐴 −ℎ 𝐵 ) ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) + ( i · ( ( ( 𝑇 ‘ ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) ·ih ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( 𝑇 ‘ ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ·ih ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ) ) ) / 4 )