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 ⊢ T ∈ LinOp
lnopeq0lem1.2 ⊢ A ∈ ℋ
lnopeq0lem1.3 ⊢ B ∈ ℋ
Assertion lnopeq0lem1 ⊢ 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 lnopeq0lem1.2 ⊢ A ∈ ℋ
3 lnopeq0lem1.3 ⊢ B ∈ ℋ
4 1 lnopfi ⊢ T : ℋ ⟶ ℋ
5 4 ffvelcdmi ⊢ A ∈ ℋ → T ⁡ A ∈ ℋ
6 2 5 ax-mp ⊢ T ⁡ A ∈ ℋ
7 4 ffvelcdmi ⊢ B ∈ ℋ → T ⁡ B ∈ ℋ
8 3 7 ax-mp ⊢ T ⁡ B ∈ ℋ
9 6 3 8 2 polid2i ⊢ T ⁡ A ⋅ ih B = T ⁡ A + ℎ T ⁡ B ⋅ ih A + ℎ B - T ⁡ A - ℎ T ⁡ B ⋅ ih A - ℎ B + i ⁢ T ⁡ A + ℎ i ⋅ ℎ T ⁡ B ⋅ ih A + ℎ i ⋅ ℎ B − T ⁡ A - ℎ i ⋅ ℎ T ⁡ B ⋅ ih A - ℎ i ⋅ ℎ B 4
10 1 lnopaddi ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A + ℎ B = T ⁡ A + ℎ T ⁡ B
11 2 3 10 mp2an ⊢ T ⁡ A + ℎ B = T ⁡ A + ℎ T ⁡ B
12 11 oveq1i ⊢ T ⁡ A + ℎ B ⋅ ih A + ℎ B = T ⁡ A + ℎ T ⁡ B ⋅ ih A + ℎ B
13 1 lnopsubi ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A - ℎ B = T ⁡ A - ℎ T ⁡ B
14 2 3 13 mp2an ⊢ T ⁡ A - ℎ B = T ⁡ A - ℎ T ⁡ B
15 14 oveq1i ⊢ T ⁡ A - ℎ B ⋅ ih A - ℎ B = T ⁡ A - ℎ T ⁡ B ⋅ ih A - ℎ B
16 12 15 oveq12i ⊢ T ⁡ A + ℎ B ⋅ ih A + ℎ B − T ⁡ A - ℎ B ⋅ ih A - ℎ B = T ⁡ A + ℎ T ⁡ B ⋅ ih A + ℎ B − T ⁡ A - ℎ T ⁡ B ⋅ ih A - ℎ B
17 ax-icn ⊢ i ∈ ℂ
18 1 lnopaddmuli ⊢ i ∈ ℂ ∧ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A + ℎ i ⋅ ℎ B = T ⁡ A + ℎ i ⋅ ℎ T ⁡ B
19 17 2 3 18 mp3an ⊢ T ⁡ A + ℎ i ⋅ ℎ B = T ⁡ A + ℎ i ⋅ ℎ T ⁡ B
20 19 oveq1i ⊢ T ⁡ A + ℎ i ⋅ ℎ B ⋅ ih A + ℎ i ⋅ ℎ B = T ⁡ A + ℎ i ⋅ ℎ T ⁡ B ⋅ ih A + ℎ i ⋅ ℎ B
21 1 lnopsubmuli ⊢ i ∈ ℂ ∧ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A - ℎ i ⋅ ℎ B = T ⁡ A - ℎ i ⋅ ℎ T ⁡ B
22 17 2 3 21 mp3an ⊢ T ⁡ A - ℎ i ⋅ ℎ B = T ⁡ A - ℎ i ⋅ ℎ T ⁡ B
23 22 oveq1i ⊢ T ⁡ A - ℎ i ⋅ ℎ B ⋅ ih A - ℎ i ⋅ ℎ B = T ⁡ A - ℎ i ⋅ ℎ T ⁡ B ⋅ ih A - ℎ i ⋅ ℎ B
24 20 23 oveq12i ⊢ T ⁡ A + ℎ i ⋅ ℎ B ⋅ ih A + ℎ i ⋅ ℎ B − T ⁡ A - ℎ i ⋅ ℎ B ⋅ ih A - ℎ i ⋅ ℎ B = T ⁡ A + ℎ i ⋅ ℎ T ⁡ B ⋅ ih A + ℎ i ⋅ ℎ B − T ⁡ A - ℎ i ⋅ ℎ T ⁡ B ⋅ ih A - ℎ i ⋅ ℎ B
25 24 oveq2i ⊢ i ⁢ T ⁡ A + ℎ i ⋅ ℎ B ⋅ ih A + ℎ i ⋅ ℎ B − T ⁡ A - ℎ i ⋅ ℎ B ⋅ ih A - ℎ i ⋅ ℎ B = i ⁢ T ⁡ A + ℎ i ⋅ ℎ T ⁡ B ⋅ ih A + ℎ i ⋅ ℎ B − T ⁡ A - ℎ i ⋅ ℎ T ⁡ B ⋅ ih A - ℎ i ⋅ ℎ B
26 16 25 oveq12i ⊢ 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 ⁡ A + ℎ T ⁡ B ⋅ ih A + ℎ B - T ⁡ A - ℎ T ⁡ B ⋅ ih A - ℎ B + i ⁢ T ⁡ A + ℎ i ⋅ ℎ T ⁡ B ⋅ ih A + ℎ i ⋅ ℎ B − T ⁡ A - ℎ i ⋅ ℎ T ⁡ B ⋅ ih A - ℎ i ⋅ ℎ B
27 26 oveq1i ⊢ 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 ⁡ A + ℎ T ⁡ B ⋅ ih A + ℎ B - T ⁡ A - ℎ T ⁡ B ⋅ ih A - ℎ B + i ⁢ T ⁡ A + ℎ i ⋅ ℎ T ⁡ B ⋅ ih A + ℎ i ⋅ ℎ B − T ⁡ A - ℎ i ⋅ ℎ T ⁡ B ⋅ ih A - ℎ i ⋅ ℎ B 4
28 9 27 eqtr4i ⊢ 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