This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ ℋ
normpar.2 ⊢ 𝐵 ∈ ℋ
Assertion normpari ( ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ↑ 2 ) ) = ( ( 2 · ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ) + ( 2 · ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) )

Proof

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