Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
GIF version

Theorem normlem3 5065

Description: Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97.

**Hypotheses**
Ref	Expression
normlem1.1	⊢ S ∈ ℂ
normlem1.2	⊢ F ∈ ℋ
normlem1.3	⊢ G ∈ ℋ
normlem2.4	⊢ B = -(((∗ ‘S) · (F ·_i G)) + (S · (G ·_i F)))
normlem3.5	⊢ A = (G ·_i G)
normlem3.6	⊢ C = (F ·_i F)
normlem3.7	⊢ R ∈ ℝ

**Assertion**
Ref	Expression
normlem3	⊢ (((A · (R↑2)) + (B · R)) + C) = (((F ·_i F) + (((∗ ‘S) · -R) · (F ·_i G))) + (((S · -R) · (G ·_i F)) + ((R↑2) · (G ·_i G))))

**Proof of Theorem normlem3**
Step	Hyp	Ref	Expression
1		normlem3.6	. . 3 ⊢ C = (F ·_i F)
2		normlem3.5	. . . . . . 7 ⊢ A = (G ·_i G)
3		normlem1.3	. . . . . . . 8 ⊢ G ∈ ℋ
4	3, 3	hicl 5044	. . . . . . 7 ⊢ (G ·_i G) ∈ ℂ
5	2, 4	eqeltr 1159	. . . . . 6 ⊢ A ∈ ℂ
6		normlem3.7	. . . . . . . 8 ⊢ R ∈ ℝ
7	6	recn 4098	. . . . . . 7 ⊢ R ∈ ℂ
8	7	sqcl 4686	. . . . . 6 ⊢ (R↑2) ∈ ℂ
9	5, 8	mulcl 4105	. . . . 5 ⊢ (A · (R↑2)) ∈ ℂ
10		normlem1.1	. . . . . . . 8 ⊢ S ∈ ℂ
11		normlem1.2	. . . . . . . 8 ⊢ F ∈ ℋ
12		normlem2.4	. . . . . . . 8 ⊢ B = -(((∗ ‘S) · (F ·_i G)) + (S · (G ·_i F)))
13	10, 11, 3, 12	normlem2 5064	. . . . . . 7 ⊢ B ∈ ℝ
14	13	recn 4098	. . . . . 6 ⊢ B ∈ ℂ
15	14, 7	mulcl 4105	. . . . 5 ⊢ (B · R) ∈ ℂ
16	9, 15	addcom 4106	. . . 4 ⊢ ((A · (R↑2)) + (B · R)) = ((B · R) + (A · (R↑2)))
17	10	cjcl 4804	. . . . . . . . . 10 ⊢ (∗ ‘S) ∈ ℂ
18	11, 3	hicl 5044	. . . . . . . . . 10 ⊢ (F ·_i G) ∈ ℂ
19	17, 18	mulcl 4105	. . . . . . . . 9 ⊢ ((∗ ‘S) · (F ·_i G)) ∈ ℂ
20	3, 11	hicl 5044	. . . . . . . . . 10 ⊢ (G ·_i F) ∈ ℂ
21	10, 20	mulcl 4105	. . . . . . . . 9 ⊢ (S · (G ·_i F)) ∈ ℂ
22	19, 21	addcl 4104	. . . . . . . 8 ⊢ (((∗ ‘S) · (F ·_i G)) + (S · (G ·_i F))) ∈ ℂ
23	22, 7	mulneg1 4190	. . . . . . 7 ⊢ (-(((∗ ‘S) · (F ·_i G)) + (S · (G ·_i F))) · R) = -((((∗ ‘S) · (F ·_i G)) + (S · (G ·_i F))) · R)
24	12	opreq1i 3009	. . . . . . 7 ⊢ (B · R) = (-(((∗ ‘S) · (F ·_i G)) + (S · (G ·_i F))) · R)
25	22, 7	mulneg2 4191	. . . . . . 7 ⊢ ((((∗ ‘S) · (F ·_i G)) + (S · (G ·_i F))) · -R) = -((((∗ ‘S) · (F ·_i G)) + (S · (G ·_i F))) · R)
26	23, 24, 25	3eqtr4 1126	. . . . . 6 ⊢ (B · R) = ((((∗ ‘S) · (F ·_i G)) + (S · (G ·_i F))) · -R)
27	7	negcl 4142	. . . . . . 7 ⊢ -R ∈ ℂ
28	19, 21, 27	adddir 4111	. . . . . 6 ⊢ ((((∗ ‘S) · (F ·_i G)) + (S · (G ·_i F))) · -R) = ((((∗ ‘S) · (F ·_i G)) · -R) + ((S · (G ·_i F)) · -R))
29	17, 18, 27	mul23 4179	. . . . . . 7 ⊢ (((∗ ‘S) · (F ·_i G)) · -R) = (((∗ ‘S) · -R) · (F ·_i G))
30	10, 20, 27	mul23 4179	. . . . . . 7 ⊢ ((S · (G ·_i F)) · -R) = ((S · -R) · (G ·_i F))
31	29, 30	opreq12i 3011	. . . . . 6 ⊢ ((((∗ ‘S) · (F ·_i G)) · -R) + ((S · (G ·_i F)) · -R)) = ((((∗ ‘S) · -R) · (F ·_i G)) + ((S · -R) · (G ·_i F)))
32	26, 28, 31	3eqtr 1123	. . . . 5 ⊢ (B · R) = ((((∗ ‘S) · -R) · (F ·_i G)) + ((S · -R) · (G ·_i F)))
33	8, 5	mulcom 4107	. . . . . 6 ⊢ ((R↑2) · A) = (A · (R↑2))
34	2	opreq2i 3010	. . . . . 6 ⊢ ((R↑2) · A) = ((R↑2) · (G ·_i G))
35	33, 34	eqtr3 1121	. . . . 5 ⊢ (A · (R↑2)) = ((R↑2) · (G ·_i G))
36	32, 35	opreq12i 3011	. . . 4 ⊢ ((B · R) + (A · (R↑2))) = (((((∗ ‘S) · -R) · (F ·_i G)) + ((S · -R) · (G ·_i F))) + ((R↑2) · (G ·_i G)))
37	17, 27	mulcl 4105	. . . . . 6 ⊢ ((∗ ‘S) · -R) ∈ ℂ
38	37, 18	mulcl 4105	. . . . 5 ⊢ (((∗ ‘S) · -R) · (F ·_i G)) ∈ ℂ
39	10, 27	mulcl 4105	. . . . . 6 ⊢ (S · -R) ∈ ℂ
40	39, 20	mulcl 4105	. . . . 5 ⊢ ((S · -R) · (G ·_i F)) ∈ ℂ
41	8, 4	mulcl 4105	. . . . 5 ⊢ ((R↑2) · (G ·_i G)) ∈ ℂ
42	38, 40, 41	addass 4108	. . . 4 ⊢ (((((∗ ‘S) · -R) · (F ·_i G)) + ((S · -R) · (G ·_i F))) + ((R↑2) · (G ·_i G))) = ((((∗ ‘S) · -R) · (F ·_i G)) + (((S · -R) · (G ·_i F)) + ((R↑2) · (G ·_i G))))
43	16, 36, 42	3eqtr 1123	. . 3 ⊢ ((A · (R↑2)) + (B · R)) = ((((∗ ‘S) · -R) · (F ·_i G)) + (((S · -R) · (G ·_i F)) + ((R↑2) · (G ·_i G))))
44	1, 43	opreq12i 3011	. 2 ⊢ (C + ((A · (R↑2)) + (B · R))) = ((F ·_i F) + ((((∗ ‘S) · -R) · (F ·_i G)) + (((S · -R) · (G ·_i F)) + ((R↑2) · (G ·_i G)))))
45	9, 15	addcl 4104	. . 3 ⊢ ((A · (R↑2)) + (B · R)) ∈ ℂ
46	11, 11	hicl 5044	. . . 4 ⊢ (F ·_i F) ∈ ℂ
47	1, 46	eqeltr 1159	. . 3 ⊢ C ∈ ℂ
48	45, 47	addcom 4106	. 2 ⊢ (((A · (R↑2)) + (B · R)) + C) = (C + ((A · (R↑2)) + (B · R)))
49	40, 41	addcl 4104	. . 3 ⊢ (((S · -R) · (G ·_i F)) + ((R↑2) · (G ·_i G))) ∈ ℂ
50	46, 38, 49	addass 4108	. 2 ⊢ (((F ·_i F) + (((∗ ‘S) · -R) · (F ·_i G))) + (((S · -R) · (G ·_i F)) + ((R↑2) · (G ·_i G)))) = ((F ·_i F) + ((((∗ ‘S) · -R) · (F ·_i G)) + (((S · -R) · (G ·_i F)) + ((R↑2) · (G ·_i G)))))
51	44, 48, 50	3eqtr4 1126	1 ⊢ (((A · (R↑2)) + (B · R)) + C) = (((F ·_i F) + (((∗ ‘S) · -R) · (F ·_i G))) + (((S · -R) · (G ·_i F)) + ((R↑2) · (G ·_i G))))

Colors of variables: wff set class

Syntax hints: = wceq 1091 ∈ wcel 1092 ‘cfv 2422 (class class class)co 3001 ℂcc 4026 ℝcr 4027 + caddc 4031 · cmulc 4032 -cneg 4090 2c2 4454 ↑cexp 4675 ∗ccj 4788 ℋ chil 4958 ·_i csp 4963

This theorem is referenced by: normlem4 5066

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-hicl 5043 ax-his1 5045

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-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-re 4790 df-im 4791 df-cj 4792

metamath.org