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 e. ~H
	normpar.2	|- B e. ~H
Assertion	normpari	|- ( ( ( normh ` ( A -h B ) ) ^ 2 ) + ( ( normh ` ( A +h B ) ) ^ 2 ) ) = ( ( 2 x. ( ( normh ` A ) ^ 2 ) ) + ( 2 x. ( ( normh ` B ) ^ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		normpar.1	|- A e. ~H
2		normpar.2	|- B e. ~H
3	1 2	hvsubcli	|- ( A -h B ) e. ~H
4	3	normsqi	|- ( ( normh ` ( A -h B ) ) ^ 2 ) = ( ( A -h B ) .ih ( A -h B ) )
5	1 2	hvaddcli	|- ( A +h B ) e. ~H
6	5	normsqi	|- ( ( normh ` ( A +h B ) ) ^ 2 ) = ( ( A +h B ) .ih ( A +h B ) )
7	4 6	oveq12i	|- ( ( ( normh ` ( A -h B ) ) ^ 2 ) + ( ( normh ` ( A +h B ) ) ^ 2 ) ) = ( ( ( A -h B ) .ih ( A -h B ) ) + ( ( A +h B ) .ih ( A +h B ) ) )
8	1	normsqi	|- ( ( normh ` A ) ^ 2 ) = ( A .ih A )
9	8	oveq2i	|- ( 2 x. ( ( normh ` A ) ^ 2 ) ) = ( 2 x. ( A .ih A ) )
10	1 1	hicli	|- ( A .ih A ) e. CC
11	10	2timesi	|- ( 2 x. ( A .ih A ) ) = ( ( A .ih A ) + ( A .ih A ) )
12	9 11	eqtri	|- ( 2 x. ( ( normh ` A ) ^ 2 ) ) = ( ( A .ih A ) + ( A .ih A ) )
13	2	normsqi	|- ( ( normh ` B ) ^ 2 ) = ( B .ih B )
14	13	oveq2i	|- ( 2 x. ( ( normh ` B ) ^ 2 ) ) = ( 2 x. ( B .ih B ) )
15	2 2	hicli	|- ( B .ih B ) e. CC
16	15	2timesi	|- ( 2 x. ( B .ih B ) ) = ( ( B .ih B ) + ( B .ih B ) )
17	14 16	eqtri	|- ( 2 x. ( ( normh ` B ) ^ 2 ) ) = ( ( B .ih B ) + ( B .ih B ) )
18	12 17	oveq12i	|- ( ( 2 x. ( ( normh ` A ) ^ 2 ) ) + ( 2 x. ( ( normh ` B ) ^ 2 ) ) ) = ( ( ( A .ih A ) + ( A .ih A ) ) + ( ( B .ih B ) + ( B .ih B ) ) )
19	1 2 1 2	normlem9	|- ( ( A -h B ) .ih ( A -h B ) ) = ( ( ( A .ih A ) + ( B .ih B ) ) - ( ( A .ih B ) + ( B .ih A ) ) )
20	10 15	addcli	|- ( ( A .ih A ) + ( B .ih B ) ) e. CC
21	1 2	hicli	|- ( A .ih B ) e. CC
22	2 1	hicli	|- ( B .ih A ) e. CC
23	21 22	addcli	|- ( ( A .ih B ) + ( B .ih A ) ) e. CC
24	20 23	negsubi	|- ( ( ( A .ih A ) + ( B .ih B ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) ) = ( ( ( A .ih A ) + ( B .ih B ) ) - ( ( A .ih B ) + ( B .ih A ) ) )
25	19 24	eqtr4i	|- ( ( A -h B ) .ih ( A -h B ) ) = ( ( ( A .ih A ) + ( B .ih B ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) )
26	1 2 1 2	normlem8	|- ( ( A +h B ) .ih ( A +h B ) ) = ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih B ) + ( B .ih A ) ) )
27	25 26	oveq12i	|- ( ( ( A -h B ) .ih ( A -h B ) ) + ( ( A +h B ) .ih ( A +h B ) ) ) = ( ( ( ( A .ih A ) + ( B .ih B ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) ) + ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih B ) + ( B .ih A ) ) ) )
28	23	negcli	|- -u ( ( A .ih B ) + ( B .ih A ) ) e. CC
29	20 28 20 23	add42i	|- ( ( ( ( A .ih A ) + ( B .ih B ) ) + -u ( ( 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 ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) ) )
30	23	negidi	|- ( ( ( A .ih B ) + ( B .ih A ) ) + -u ( ( 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 ) ) + -u ( ( 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 ) ) ) e. CC
33	32	addid1i	|- ( ( ( ( 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 ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) ) ) = ( ( ( A .ih A ) + ( A .ih A ) ) + ( ( B .ih B ) + ( B .ih B ) ) )
36	27 29 35	3eqtri	|- ( ( ( A -h B ) .ih ( A -h B ) ) + ( ( A +h B ) .ih ( A +h B ) ) ) = ( ( ( A .ih A ) + ( A .ih A ) ) + ( ( B .ih B ) + ( B .ih B ) ) )
37	18 36	eqtr4i	|- ( ( 2 x. ( ( normh ` A ) ^ 2 ) ) + ( 2 x. ( ( normh ` B ) ^ 2 ) ) ) = ( ( ( A -h B ) .ih ( A -h B ) ) + ( ( A +h B ) .ih ( A +h B ) ) )
38	7 37	eqtr4i	|- ( ( ( normh ` ( A -h B ) ) ^ 2 ) + ( ( normh ` ( A +h B ) ) ^ 2 ) ) = ( ( 2 x. ( ( normh ` A ) ^ 2 ) ) + ( 2 x. ( ( normh ` B ) ^ 2 ) ) )