Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
GIF version

Theorem pjthlem7 5231

Description: Lemma for Theorem 3.7(i) of [Beran] p. 102.

**Hypotheses**
Ref	Expression
pjthlem6.1	⊢ D ∈ ℋ
pjthlem6.2	⊢ R = (1 / (D ·_i D))
pjthlem6.3	⊢ C ∈ ℋ
pjthlem6.4	⊢ S = (R · (C ·_i D))

**Assertion**
Ref	Expression
pjthlem7	⊢ (¬ D = 0_v → ((S · (∗ ‘S)) · (D ·_i D)) = (R · ((abs ‘(C ·_i D))↑2)))

**Proof of Theorem pjthlem7**
Step	Hyp	Ref	Expression
1		pjthlem6.1	. . . . 5 ⊢ D ∈ ℋ
2		pjthlem6.2	. . . . 5 ⊢ R = (1 / (D ·_i D))
3	1, 2	pjthlem2 5226	. . . 4 ⊢ (¬ D = 0_v → R ∈ ℝ)
4		pjthlem6.4	. . . . . . . . 9 ⊢ S = (R · (C ·_i D))
5	4	a1i 7	. . . . . . . 8 ⊢ (R ∈ ℝ → S = (R · (C ·_i D)))
6		recnt 4097	. . . . . . . . . . 11 ⊢ (R ∈ ℝ → R ∈ ℂ)
7		pjthlem6.3	. . . . . . . . . . . . 13 ⊢ C ∈ ℋ
8	7, 1	hicl 5044	. . . . . . . . . . . 12 ⊢ (C ·_i D) ∈ ℂ
9		cjmult 4832	. . . . . . . . . . . 12 ⊢ ((R ∈ ℂ ∧ (C ·_i D) ∈ ℂ) → (∗ ‘(R · (C ·_i D))) = ((∗ ‘R) · (∗ ‘(C ·_i D))))
10	8, 9	mpan2 519	. . . . . . . . . . 11 ⊢ (R ∈ ℂ → (∗ ‘(R · (C ·_i D))) = ((∗ ‘R) · (∗ ‘(C ·_i D))))
11	6, 10	syl 12	. . . . . . . . . 10 ⊢ (R ∈ ℝ → (∗ ‘(R · (C ·_i D))) = ((∗ ‘R) · (∗ ‘(C ·_i D))))
12		cjret 4829	. . . . . . . . . . 11 ⊢ (R ∈ ℝ → (∗ ‘R) = R)
13	12	opreq1d 3012	. . . . . . . . . 10 ⊢ (R ∈ ℝ → ((∗ ‘R) · (∗ ‘(C ·_i D))) = (R · (∗ ‘(C ·_i D))))
14	11, 13	eqtrd 1128	. . . . . . . . 9 ⊢ (R ∈ ℝ → (∗ ‘(R · (C ·_i D))) = (R · (∗ ‘(C ·_i D))))
15	4	fveq2i 2835	. . . . . . . . 9 ⊢ (∗ ‘S) = (∗ ‘(R · (C ·_i D)))
16	14, 15	syl5eq 1136	. . . . . . . 8 ⊢ (R ∈ ℝ → (∗ ‘S) = (R · (∗ ‘(C ·_i D))))
17	5, 16	opreq12d 3014	. . . . . . 7 ⊢ (R ∈ ℝ → (S · (∗ ‘S)) = ((R · (C ·_i D)) · (R · (∗ ‘(C ·_i D)))))
18		mul4t 4177	. . . . . . . 8 ⊢ (((R ∈ ℂ ∧ (C ·_i D) ∈ ℂ) ∧ (R ∈ ℂ ∧ (∗ ‘(C ·_i D)) ∈ ℂ)) → ((R · (C ·_i D)) · (R · (∗ ‘(C ·_i D)))) = ((R · R) · ((C ·_i D) · (∗ ‘(C ·_i D)))))
19	6, 8	jctir 241	. . . . . . . 8 ⊢ (R ∈ ℝ → (R ∈ ℂ ∧ (C ·_i D) ∈ ℂ))
20	8	cjcl 4804	. . . . . . . . 9 ⊢ (∗ ‘(C ·_i D)) ∈ ℂ
21	6, 20	jctir 241	. . . . . . . 8 ⊢ (R ∈ ℝ → (R ∈ ℂ ∧ (∗ ‘(C ·_i D)) ∈ ℂ))
22	18, 19, 21	sylanc 361	. . . . . . 7 ⊢ (R ∈ ℝ → ((R · (C ·_i D)) · (R · (∗ ‘(C ·_i D)))) = ((R · R) · ((C ·_i D) · (∗ ‘(C ·_i D)))))
23	17, 22	eqtrd 1128	. . . . . 6 ⊢ (R ∈ ℝ → (S · (∗ ‘S)) = ((R · R) · ((C ·_i D) · (∗ ‘(C ·_i D)))))
24	23	opreq1d 3012	. . . . 5 ⊢ (R ∈ ℝ → ((S · (∗ ‘S)) · (D ·_i D)) = (((R · R) · ((C ·_i D) · (∗ ‘(C ·_i D)))) · (D ·_i D)))
25		axmulcl 4068	. . . . . . 7 ⊢ ((R ∈ ℂ ∧ R ∈ ℂ) → (R · R) ∈ ℂ)
26	25, 6, 6	sylanc 361	. . . . . 6 ⊢ (R ∈ ℝ → (R · R) ∈ ℂ)
27	8, 20	mulcl 4105	. . . . . . 7 ⊢ ((C ·_i D) · (∗ ‘(C ·_i D))) ∈ ℂ
28	1, 1	hicl 5044	. . . . . . . 8 ⊢ (D ·_i D) ∈ ℂ
29		mul23t 4176	. . . . . . . 8 ⊢ (((R · R) ∈ ℂ ∧ ((C ·_i D) · (∗ ‘(C ·_i D))) ∈ ℂ ∧ (D ·_i D) ∈ ℂ) → (((R · R) · ((C ·_i D) · (∗ ‘(C ·_i D)))) · (D ·_i D)) = (((R · R) · (D ·_i D)) · ((C ·_i D) · (∗ ‘(C ·_i D)))))
30	28, 29	mp3an3 641	. . . . . . 7 ⊢ (((R · R) ∈ ℂ ∧ ((C ·_i D) · (∗ ‘(C ·_i D))) ∈ ℂ) → (((R · R) · ((C ·_i D) · (∗ ‘(C ·_i D)))) · (D ·_i D)) = (((R · R) · (D ·_i D)) · ((C ·_i D) · (∗ ‘(C ·_i D)))))
31	27, 30	mpan2 519	. . . . . 6 ⊢ ((R · R) ∈ ℂ → (((R · R) · ((C ·_i D) · (∗ ‘(C ·_i D)))) · (D ·_i D)) = (((R · R) · (D ·_i D)) · ((C ·_i D) · (∗ ‘(C ·_i D)))))
32	26, 31	syl 12	. . . . 5 ⊢ (R ∈ ℝ → (((R · R) · ((C ·_i D) · (∗ ‘(C ·_i D)))) · (D ·_i D)) = (((R · R) · (D ·_i D)) · ((C ·_i D) · (∗ ‘(C ·_i D)))))
33	24, 32	eqtrd 1128	. . . 4 ⊢ (R ∈ ℝ → ((S · (∗ ‘S)) · (D ·_i D)) = (((R · R) · (D ·_i D)) · ((C ·_i D) · (∗ ‘(C ·_i D)))))
34	3, 33	syl 12	. . 3 ⊢ (¬ D = 0_v → ((S · (∗ ‘S)) · (D ·_i D)) = (((R · R) · (D ·_i D)) · ((C ·_i D) · (∗ ‘(C ·_i D)))))
35		mul23t 4176	. . . . . . . 8 ⊢ ((R ∈ ℂ ∧ R ∈ ℂ ∧ (D ·_i D) ∈ ℂ) → ((R · R) · (D ·_i D)) = ((R · (D ·_i D)) · R))
36	28, 35	mp3an3 641	. . . . . . 7 ⊢ ((R ∈ ℂ ∧ R ∈ ℂ) → ((R · R) · (D ·_i D)) = ((R · (D ·_i D)) · R))
37	36, 6, 6	sylanc 361	. . . . . 6 ⊢ (R ∈ ℝ → ((R · R) · (D ·_i D)) = ((R · (D ·_i D)) · R))
38	3, 37	syl 12	. . . . 5 ⊢ (¬ D = 0_v → ((R · R) · (D ·_i D)) = ((R · (D ·_i D)) · R))
39		axhis42 5049	. . . . . . . . . . 11 ⊢ ((D ∈ ℋ ∧ ¬ D = 0_v) → 0 < (D ·_i D))
40	1, 39	mpan 518	. . . . . . . . . 10 ⊢ (¬ D = 0_v → 0 < (D ·_i D))
41		hiidrclt 5053	. . . . . . . . . . . 12 ⊢ (D ∈ ℋ → (D ·_i D) ∈ ℝ)
42	1, 41	ax-mp 6	. . . . . . . . . . 11 ⊢ (D ·_i D) ∈ ℝ
43	42	gt0ne0 4340	. . . . . . . . . 10 ⊢ (0 < (D ·_i D) → (D ·_i D) ≠ 0)
44	40, 43	syl 12	. . . . . . . . 9 ⊢ (¬ D = 0_v → (D ·_i D) ≠ 0)
45		1cn 4101	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
46	45, 28	divclz 4222	. . . . . . . . 9 ⊢ ((D ·_i D) ≠ 0 → (1 / (D ·_i D)) ∈ ℂ)
47		axmulcom 4071	. . . . . . . . . 10 ⊢ (((1 / (D ·_i D)) ∈ ℂ ∧ (D ·_i D) ∈ ℂ) → ((1 / (D ·_i D)) · (D ·_i D)) = ((D ·_i D) · (1 / (D ·_i D))))
48	28, 47	mpan2 519	. . . . . . . . 9 ⊢ ((1 / (D ·_i D)) ∈ ℂ → ((1 / (D ·_i D)) · (D ·_i D)) = ((D ·_i D) · (1 / (D ·_i D))))
49	44, 46, 48	3syl 21	. . . . . . . 8 ⊢ (¬ D = 0_v → ((1 / (D ·_i D)) · (D ·_i D)) = ((D ·_i D) · (1 / (D ·_i D))))
50	28	recidz 4234	. . . . . . . . 9 ⊢ ((D ·_i D) ≠ 0 → ((D ·_i D) · (1 / (D ·_i D))) = 1)
51	40, 43, 50	3syl 21	. . . . . . . 8 ⊢ (¬ D = 0_v → ((D ·_i D) · (1 / (D ·_i D))) = 1)
52	49, 51	eqtrd 1128	. . . . . . 7 ⊢ (¬ D = 0_v → ((1 / (D ·_i D)) · (D ·_i D)) = 1)
53	2	opreq1i 3009	. . . . . . 7 ⊢ (R · (D ·_i D)) = ((1 / (D ·_i D)) · (D ·_i D))
54	52, 53	syl5eq 1136	. . . . . 6 ⊢ (¬ D = 0_v → (R · (D ·_i D)) = 1)
55	54	opreq1d 3012	. . . . 5 ⊢ (¬ D = 0_v → ((R · (D ·_i D)) · R) = (1 · R))
56		mulid2t 4175	. . . . . 6 ⊢ (R ∈ ℂ → (1 · R) = R)
57	3, 6, 56	3syl 21	. . . . 5 ⊢ (¬ D = 0_v → (1 · R) = R)
58	38, 55, 57	3eqtrd 1132	. . . 4 ⊢ (¬ D = 0_v → ((R · R) · (D ·_i D)) = R)
59	58	opreq1d 3012	. . 3 ⊢ (¬ D = 0_v → (((R · R) · (D ·_i D)) · ((C ·_i D) · (∗ ‘(C ·_i D)))) = (R · ((C ·_i D) · (∗ ‘(C ·_i D)))))
60	34, 59	eqtrd 1128	. 2 ⊢ (¬ D = 0_v → ((S · (∗ ‘S)) · (D ·_i D)) = (R · ((C ·_i D) · (∗ ‘(C ·_i D)))))
61	8	absvalsq 4837	. . 3 ⊢ ((abs ‘(C ·_i D))↑2) = ((C ·_i D) · (∗ ‘(C ·_i D)))
62	61	opreq2i 3010	. 2 ⊢ (R · ((abs ‘(C ·_i D))↑2)) = (R · ((C ·_i D) · (∗ ‘(C ·_i D))))
63	60, 62	syl6eqr 1142	1 ⊢ (¬ D = 0_v → ((S · (∗ ‘S)) · (D ·_i D)) = (R · ((abs ‘(C ·_i D))↑2)))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ∧ wa 196 = wceq 1091 ∈ wcel 1092 ≠ wne 1190 class class class wbr 2054 ‘cfv 2422 (class class class)co 3001 ℂcc 4026 ℝcr 4027 0cc0 4028 1c1 4029 · cmulc 4032 < clt 4033 / cdiv 4091 2c2 4454 ↑cexp 4675 ∗ccj 4788 abscabs 4789 ℋ chil 4958 0_vc0v 4961 ·_i csp 4963

This theorem is referenced by: pjthlem8 5232

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 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-abs 4793

metamath.org