Metamath Proof Explorer

Theorem normpar

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

Ref Expression
Assertion normpar ⊢ A ∈ ℋ ∧ B ∈ ℋ → norm ℎ ⁡ A - ℎ B 2 + norm ℎ ⁡ A + ℎ B 2 = 2 ⁢ norm ℎ ⁡ A 2 + 2 ⁢ norm ℎ ⁡ B 2

Proof

Step Hyp Ref Expression
1 fvoveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B
2 1 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B 2
3 fvoveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A + ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B
4 3 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A + ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2
5 2 4 oveq12d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ B 2 + norm ℎ ⁡ A + ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B 2 + norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2
6 fveq2 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ
7 6 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2
8 7 oveq2d ⊢ A = if A ∈ ℋ A 0 ℎ → 2 ⁢ norm ℎ ⁡ A 2 = 2 ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2
9 8 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → 2 ⁢ norm ℎ ⁡ A 2 + 2 ⁢ norm ℎ ⁡ B 2 = 2 ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2 + 2 ⁢ norm ℎ ⁡ B 2
10 5 9 eqeq12d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ B 2 + norm ℎ ⁡ A + ℎ B 2 = 2 ⁢ norm ℎ ⁡ A 2 + 2 ⁢ norm ℎ ⁡ B 2 ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B 2 + norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2 = 2 ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2 + 2 ⁢ norm ℎ ⁡ B 2
11 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ B = if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
12 11 fveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
13 12 oveq1d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ 2
14 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ + ℎ B = if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ
15 14 fveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ
16 15 oveq1d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ 2
17 13 16 oveq12d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B 2 + norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ 2 + norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ 2
18 fveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ B = norm ℎ ⁡ if B ∈ ℋ B 0 ℎ
19 18 oveq1d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ B 2 = norm ℎ ⁡ if B ∈ ℋ B 0 ℎ 2
20 19 oveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → 2 ⁢ norm ℎ ⁡ B 2 = 2 ⁢ norm ℎ ⁡ if B ∈ ℋ B 0 ℎ 2
21 20 oveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → 2 ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2 + 2 ⁢ norm ℎ ⁡ B 2 = 2 ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2 + 2 ⁢ norm ℎ ⁡ if B ∈ ℋ B 0 ℎ 2
22 17 21 eqeq12d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B 2 + norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2 = 2 ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2 + 2 ⁢ norm ℎ ⁡ B 2 ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ 2 + norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ 2 = 2 ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2 + 2 ⁢ norm ℎ ⁡ if B ∈ ℋ B 0 ℎ 2
23 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
24 ifhvhv0 ⊢ if B ∈ ℋ B 0 ℎ ∈ ℋ
25 23 24 normpari ⊢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ 2 + norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ 2 = 2 ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2 + 2 ⁢ norm ℎ ⁡ if B ∈ ℋ B 0 ℎ 2
26 10 22 25 dedth2h ⊢ A ∈ ℋ ∧ B ∈ ℋ → norm ℎ ⁡ A - ℎ B 2 + norm ℎ ⁡ A + ℎ B 2 = 2 ⁢ norm ℎ ⁡ A 2 + 2 ⁢ norm ℎ ⁡ B 2