Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
GIF version

Theorem normpar 5099

Description: Parallelogram law for norms. Remark 3.4(B) of [Beran] p. 98.

**Hypotheses**
Ref	Expression
normpar.1	⊢ A ∈ ℋ
normpar.2	⊢ B ∈ ℋ

**Assertion**
Ref	Expression
normpar	⊢ (((norm ‘(A −_v B))↑2) + ((norm ‘(A +_v B))↑2)) = ((2 · ((norm ‘A)↑2)) + (2 · ((norm ‘B)↑2)))

**Proof of Theorem normpar**
Step	Hyp	Ref	Expression
1		normpar.1	. . . . . 6 ⊢ A ∈ ℋ
2		normpar.2	. . . . . 6 ⊢ B ∈ ℋ
3	1, 2	normlem8 5071	. . . . 5 ⊢ ((A −_v B) ·_i (A −_v B)) = (((A ·_i A) + (B ·_i B)) − ((A ·_i B) + (B ·_i A)))
4	1, 1	hicl 5044	. . . . . . 7 ⊢ (A ·_i A) ∈ ℂ
5	2, 2	hicl 5044	. . . . . . 7 ⊢ (B ·_i B) ∈ ℂ
6	4, 5	addcl 4104	. . . . . 6 ⊢ ((A ·_i A) + (B ·_i B)) ∈ ℂ
7	1, 2	hicl 5044	. . . . . . 7 ⊢ (A ·_i B) ∈ ℂ
8	2, 1	hicl 5044	. . . . . . 7 ⊢ (B ·_i A) ∈ ℂ
9	7, 8	addcl 4104	. . . . . 6 ⊢ ((A ·_i B) + (B ·_i A)) ∈ ℂ
10	6, 9	subneg 4148	. . . . 5 ⊢ (((A ·_i A) + (B ·_i B)) − ((A ·_i B) + (B ·_i A))) = (((A ·_i A) + (B ·_i B)) + -((A ·_i B) + (B ·_i A)))
11	3, 10	eqtr 1119	. . . 4 ⊢ ((A −_v B) ·_i (A −_v B)) = (((A ·_i A) + (B ·_i B)) + -((A ·_i B) + (B ·_i A)))
12	1, 2	normlem9 5070	. . . 4 ⊢ ((A +_v B) ·_i (A +_v B)) = (((A ·_i A) + (B ·_i B)) + ((A ·_i B) + (B ·_i A)))
13	11, 12	opreq12i 3011	. . 3 ⊢ (((A −_v B) ·_i (A −_v B)) + ((A +_v B) ·_i (A +_v B))) = ((((A ·_i A) + (B ·_i B)) + -((A ·_i B) + (B ·_i A))) + (((A ·_i A) + (B ·_i B)) + ((A ·_i B) + (B ·_i A))))
14	9	negcl 4142	. . . 4 ⊢ -((A ·_i B) + (B ·_i A)) ∈ ℂ
15	6, 14, 6, 9	add42 4131	. . 3 ⊢ ((((A ·_i A) + (B ·_i B)) + -((A ·_i B) + (B ·_i A))) + (((A ·_i A) + (B ·_i B)) + ((A ·_i B) + (B ·_i A)))) = ((((A ·_i A) + (B ·_i B)) + ((A ·_i A) + (B ·_i B))) + (((A ·_i B) + (B ·_i A)) + -((A ·_i B) + (B ·_i A))))
16	9	negid 4147	. . . . 5 ⊢ (((A ·_i B) + (B ·_i A)) + -((A ·_i B) + (B ·_i A))) = 0
17	16	opreq2i 3010	. . . 4 ⊢ ((((A ·_i A) + (B ·_i B)) + ((A ·_i A) + (B ·_i B))) + (((A ·_i B) + (B ·_i A)) + -((A ·_i B) + (B ·_i A)))) = ((((A ·_i A) + (B ·_i B)) + ((A ·_i A) + (B ·_i B))) + 0)
18	6, 6	addcl 4104	. . . . 5 ⊢ (((A ·_i A) + (B ·_i B)) + ((A ·_i A) + (B ·_i B))) ∈ ℂ
19	18	addid1 4112	. . . 4 ⊢ ((((A ·_i A) + (B ·_i B)) + ((A ·_i A) + (B ·_i B))) + 0) = (((A ·_i A) + (B ·_i B)) + ((A ·_i A) + (B ·_i B)))
20	4, 5, 4, 5	add4 4130	. . . 4 ⊢ (((A ·_i A) + (B ·_i B)) + ((A ·_i A) + (B ·_i B))) = (((A ·_i A) + (A ·_i A)) + ((B ·_i B) + (B ·_i B)))
21	17, 19, 20	3eqtr 1123	. . 3 ⊢ ((((A ·_i A) + (B ·_i B)) + ((A ·_i A) + (B ·_i B))) + (((A ·_i B) + (B ·_i A)) + -((A ·_i B) + (B ·_i A)))) = (((A ·_i A) + (A ·_i A)) + ((B ·_i B) + (B ·_i B)))
22	13, 15, 21	3eqtr 1123	. 2 ⊢ (((A −_v B) ·_i (A −_v B)) + ((A +_v B) ·_i (A +_v B))) = (((A ·_i A) + (A ·_i A)) + ((B ·_i B) + (B ·_i B)))
23	1, 2	hvsubcl 5002	. . . 4 ⊢ (A −_v B) ∈ ℋ
24	23	normsq 5082	. . 3 ⊢ ((norm ‘(A −_v B))↑2) = ((A −_v B) ·_i (A −_v B))
25	1, 2	hvaddcl 4999	. . . 4 ⊢ (A +_v B) ∈ ℋ
26	25	normsq 5082	. . 3 ⊢ ((norm ‘(A +_v B))↑2) = ((A +_v B) ·_i (A +_v B))
27	24, 26	opreq12i 3011	. 2 ⊢ (((norm ‘(A −_v B))↑2) + ((norm ‘(A +_v B))↑2)) = (((A −_v B) ·_i (A −_v B)) + ((A +_v B) ·_i (A +_v B)))
28	1	normsq 5082	. . . . 5 ⊢ ((norm ‘A)↑2) = (A ·_i A)
29	28	opreq2i 3010	. . . 4 ⊢ (2 · ((norm ‘A)↑2)) = (2 · (A ·_i A))
30	4	2times 4489	. . . 4 ⊢ (2 · (A ·_i A)) = ((A ·_i A) + (A ·_i A))
31	29, 30	eqtr 1119	. . 3 ⊢ (2 · ((norm ‘A)↑2)) = ((A ·_i A) + (A ·_i A))
32	2	normsq 5082	. . . . 5 ⊢ ((norm ‘B)↑2) = (B ·_i B)
33	32	opreq2i 3010	. . . 4 ⊢ (2 · ((norm ‘B)↑2)) = (2 · (B ·_i B))
34	5	2times 4489	. . . 4 ⊢ (2 · (B ·_i B)) = ((B ·_i B) + (B ·_i B))
35	33, 34	eqtr 1119	. . 3 ⊢ (2 · ((norm ‘B)↑2)) = ((B ·_i B) + (B ·_i B))
36	31, 35	opreq12i 3011	. 2 ⊢ ((2 · ((norm ‘A)↑2)) + (2 · ((norm ‘B)↑2))) = (((A ·_i A) + (A ·_i A)) + ((B ·_i B) + (B ·_i B)))
37	22, 27, 36	3eqtr4 1126	1 ⊢ (((norm ‘(A −_v B))↑2) + ((norm ‘(A +_v B))↑2)) = ((2 · ((norm ‘A)↑2)) + (2 · ((norm ‘B)↑2)))

Colors of variables: wff set class

Syntax hints: = wceq 1091 ∈ wcel 1092 ‘cfv 2422 (class class class)co 3001 0cc0 4028 + caddc 4031 · cmulc 4032 − cmin 4089 -cneg 4090 2c2 4454 ↑cexp 4675 ℋ chil 4958 +_v cva 4959 −_v cmv 4962 ·_i csp 4963 normcno 4964

This theorem is referenced by: normpar2 5100

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079 ax-hvaddcl 4984 ax-hvzercl 4987 ax-hvmulcl 4989 ax-hvmulzer 4995 ax-hicl 5043 ax-his1 5045 ax-his2 5046 ax-his3 5047 ax-his4 5048

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-sup 2154 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fo 2436 df-f1o 2437 df-fv 2438 df-rdg 2970 df-opr 3003 df-oprab 3004 df-1st 3087 df-2nd 3088 df-1o 3104 df-oadd 3106 df-omul 3107 df-er 3200 df-ec 3202 df-qs 3205 df-ni 3794 df-pli 3795 df-mi 3796 df-lti 3797 df-plpq 3829 df-mpq 3830 df-enq 3831 df-nq 3832 df-plq 3833 df-mq 3834 df-rq 3835 df-ltq 3836 df-1q 3837 df-np 3880 df-1p 3881 df-plp 3882 df-mp 3883 df-ltp 3884 df-plpr 3958 df-mpr 3959 df-enr 3960 df-nr 3961 df-plr 3962 df-mr 3963 df-ltr 3964 df-0r 3965 df-1r 3966 df-m1r 3967 df-c 4034 df-0 4035 df-1 4036 df-i 4037 df-r 4038 df-plus 4039 df-mul 4040 df-lt 4041 df-sub 4133 df-neg 4135 df-div 4216 df-le 4277 df-n 4423 df-2 4462 df-n0 4535 df-z 4564 df-seq 4661 df-exp 4676 df-sqr 4728 df-re 4790 df-im 4791 df-cj 4792 df-hvsub 4996 df-hnorm 5074

metamath.org