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 ) ) )