Metamath Proof Explorer

Theorem normpari

Description: Parallelogram law for norms. Remark 3.4(B) of Beran p. 98. (Contributed by NM, 21-Aug-1999) (New usage is discouraged.)

Ref Expression
Hypotheses normpar.1 ⊢ A ∈ ℋ
normpar.2 ⊢ B ∈ ℋ
Assertion normpari ⊢ norm ℎ ⁡ A - ℎ B 2 + norm ℎ ⁡ A + ℎ B 2 = 2 ⁢ norm ℎ ⁡ A 2 + 2 ⁢ norm ℎ ⁡ B 2

Proof

Step Hyp Ref Expression
1 normpar.1 ⊢ A ∈ ℋ
2 normpar.2 ⊢ B ∈ ℋ
3 1 2 hvsubcli ⊢ A - ℎ B ∈ ℋ
4 3 normsqi ⊢ norm ℎ ⁡ A - ℎ B 2 = A - ℎ B ⋅ ih A - ℎ B
5 1 2 hvaddcli ⊢ A + ℎ B ∈ ℋ
6 5 normsqi ⊢ norm ℎ ⁡ A + ℎ B 2 = A + ℎ B ⋅ ih A + ℎ B
7 4 6 oveq12i ⊢ norm ℎ ⁡ A - ℎ B 2 + norm ℎ ⁡ A + ℎ B 2 = A - ℎ B ⋅ ih A - ℎ B + A + ℎ B ⋅ ih A + ℎ B
8 1 normsqi ⊢ norm ℎ ⁡ A 2 = A ⋅ ih A
9 8 oveq2i ⊢ 2 ⁢ norm ℎ ⁡ A 2 = 2 ⁢ A ⋅ ih A
10 1 1 hicli ⊢ A ⋅ ih A ∈ ℂ
11 10 2timesi ⊢ 2 ⁢ A ⋅ ih A = A ⋅ ih A + A ⋅ ih A
12 9 11 eqtri ⊢ 2 ⁢ norm ℎ ⁡ A 2 = A ⋅ ih A + A ⋅ ih A
13 2 normsqi ⊢ norm ℎ ⁡ B 2 = B ⋅ ih B
14 13 oveq2i ⊢ 2 ⁢ norm ℎ ⁡ B 2 = 2 ⁢ B ⋅ ih B
15 2 2 hicli ⊢ B ⋅ ih B ∈ ℂ
16 15 2timesi ⊢ 2 ⁢ B ⋅ ih B = B ⋅ ih B + B ⋅ ih B
17 14 16 eqtri ⊢ 2 ⁢ norm ℎ ⁡ B 2 = B ⋅ ih B + B ⋅ ih B
18 12 17 oveq12i ⊢ 2 ⁢ norm ℎ ⁡ A 2 + 2 ⁢ norm ℎ ⁡ B 2 = A ⋅ ih A + A ⋅ ih A + B ⋅ ih B + B ⋅ ih B
19 1 2 1 2 normlem9 ⊢ A - ℎ B ⋅ ih A - ℎ B = A ⋅ ih A + B ⋅ ih B - A ⋅ ih B + B ⋅ ih A
20 10 15 addcli ⊢ A ⋅ ih A + B ⋅ ih B ∈ ℂ
21 1 2 hicli ⊢ A ⋅ ih B ∈ ℂ
22 2 1 hicli ⊢ B ⋅ ih A ∈ ℂ
23 21 22 addcli ⊢ A ⋅ ih B + B ⋅ ih A ∈ ℂ
24 20 23 negsubi ⊢ A ⋅ ih A + B ⋅ ih B + − A ⋅ ih B + B ⋅ ih A = A ⋅ ih A + B ⋅ ih B - A ⋅ ih B + B ⋅ ih A
25 19 24 eqtr4i ⊢ A - ℎ B ⋅ ih A - ℎ B = A ⋅ ih A + B ⋅ ih B + − A ⋅ ih B + B ⋅ ih A
26 1 2 1 2 normlem8 ⊢ A + ℎ B ⋅ ih A + ℎ B = A ⋅ ih A + B ⋅ ih B + A ⋅ ih B + B ⋅ ih A
27 25 26 oveq12i ⊢ A - ℎ B ⋅ ih A - ℎ B + A + ℎ B ⋅ ih A + ℎ B = A ⋅ ih A + B ⋅ ih B + − A ⋅ ih B + B ⋅ ih A + A ⋅ ih A + B ⋅ ih B + A ⋅ ih B + B ⋅ ih A
28 23 negcli ⊢ − A ⋅ ih B + B ⋅ ih A ∈ ℂ
29 20 28 20 23 add42i ⊢ A ⋅ ih A + B ⋅ ih B + − A ⋅ ih B + B ⋅ ih A + A ⋅ ih A + B ⋅ ih B + A ⋅ ih B + B ⋅ ih A = A ⋅ ih A + B ⋅ ih B + A ⋅ ih A + B ⋅ ih B + A ⋅ ih B + B ⋅ ih A + − A ⋅ ih B + B ⋅ ih A
30 23 negidi ⊢ A ⋅ ih B + B ⋅ ih A + − A ⋅ ih B + B ⋅ ih A = 0
31 30 oveq2i ⊢ A ⋅ ih A + B ⋅ ih B + A ⋅ ih A + B ⋅ ih B + A ⋅ ih B + B ⋅ ih A + − A ⋅ ih B + B ⋅ ih A = A ⋅ ih A + B ⋅ ih B + A ⋅ ih A + B ⋅ ih B + 0
32 20 20 addcli ⊢ A ⋅ ih A + B ⋅ ih B + A ⋅ ih A + B ⋅ ih B ∈ ℂ
33 32 addridi ⊢ A ⋅ ih A + B ⋅ ih B + A ⋅ ih A + B ⋅ ih B + 0 = A ⋅ ih A + B ⋅ ih B + A ⋅ ih A + B ⋅ ih B
34 10 15 10 15 add4i ⊢ A ⋅ ih A + B ⋅ ih B + A ⋅ ih A + B ⋅ ih B = A ⋅ ih A + A ⋅ ih A + B ⋅ ih B + B ⋅ ih B
35 31 33 34 3eqtri ⊢ A ⋅ ih A + B ⋅ ih B + A ⋅ ih A + B ⋅ ih B + A ⋅ ih B + B ⋅ ih A + − A ⋅ ih B + B ⋅ ih A = A ⋅ ih A + A ⋅ ih A + B ⋅ ih B + B ⋅ ih B
36 27 29 35 3eqtri ⊢ A - ℎ B ⋅ ih A - ℎ B + A + ℎ B ⋅ ih A + ℎ B = A ⋅ ih A + A ⋅ ih A + B ⋅ ih B + B ⋅ ih B
37 18 36 eqtr4i ⊢ 2 ⁢ norm ℎ ⁡ A 2 + 2 ⁢ norm ℎ ⁡ B 2 = A - ℎ B ⋅ ih A - ℎ B + A + ℎ B ⋅ ih A + ℎ B
38 7 37 eqtr4i ⊢ norm ℎ ⁡ A - ℎ B 2 + norm ℎ ⁡ A + ℎ B 2 = 2 ⁢ norm ℎ ⁡ A 2 + 2 ⁢ norm ℎ ⁡ B 2