pjthlem7 - Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
GIF version

Theorem pjthlem7 9249

Description: Lemma for pjthi 9257.

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

**Assertion**
Ref	Expression
pjthlem7	⊢ (D ≠ 0_h → ((S · (∗ ‘S)) · (D ·_ih D)) = (R · ((abs ‘(C ·_ih D))↑2)))

**Proof of Theorem pjthlem7**
Step	Hyp	Ref	Expression
1		pjthlem6.1	. . . . 5 ⊢ D ∈ ℋ
2		pjthlem6.2	. . . . 5 ⊢ R = (1 / (D ·_ih D))
3	1, 2	pjthlem2 9244	. . . 4 ⊢ (D ≠ 0_h → R ∈ ℝ)
4		pjthlem6.4	. . . . . . . . 9 ⊢ S = (R · (C ·_ih D))
5	4	a1i 8	. . . . . . . 8 ⊢ (R ∈ ℝ → S = (R · (C ·_ih D)))
6		recn 5333	. . . . . . . . . . 11 ⊢ (R ∈ ℝ → R ∈ ℂ)
7		pjthlem6.3	. . . . . . . . . . . . 13 ⊢ C ∈ ℋ
8	7, 1	hicli 8972	. . . . . . . . . . . 12 ⊢ (C ·_ih D) ∈ ℂ
9		cjmul 6845	. . . . . . . . . . . 12 ⊢ ((R ∈ ℂ ⋀ (C ·_ih D) ∈ ℂ) → (∗ ‘(R · (C ·_ih D))) = ((∗ ‘R) · (∗ ‘(C ·_ih D))))
10	8, 9	mpan2 700	. . . . . . . . . . 11 ⊢ (R ∈ ℂ → (∗ ‘(R · (C ·_ih D))) = ((∗ ‘R) · (∗ ‘(C ·_ih D))))
11	6, 10	syl 10	. . . . . . . . . 10 ⊢ (R ∈ ℝ → (∗ ‘(R · (C ·_ih D))) = ((∗ ‘R) · (∗ ‘(C ·_ih D))))
12		cjre 6842	. . . . . . . . . . 11 ⊢ (R ∈ ℝ → (∗ ‘R) = R)
13	12	opreq1d 3991	. . . . . . . . . 10 ⊢ (R ∈ ℝ → ((∗ ‘R) · (∗ ‘(C ·_ih D))) = (R · (∗ ‘(C ·_ih D))))
14	11, 13	eqtrd 1514	. . . . . . . . 9 ⊢ (R ∈ ℝ → (∗ ‘(R · (C ·_ih D))) = (R · (∗ ‘(C ·_ih D))))
15	4	fveq2i 3743	. . . . . . . . 9 ⊢ (∗ ‘S) = (∗ ‘(R · (C ·_ih D)))
16	14, 15	syl5eq 1526	. . . . . . . 8 ⊢ (R ∈ ℝ → (∗ ‘S) = (R · (∗ ‘(C ·_ih D))))
17	5, 16	opreq12d 3994	. . . . . . 7 ⊢ (R ∈ ℝ → (S · (∗ ‘S)) = ((R · (C ·_ih D)) · (R · (∗ ‘(C ·_ih D)))))
18		mul4 5440	. . . . . . . 8 ⊢ (((R ∈ ℂ ⋀ (C ·_ih D) ∈ ℂ) ⋀ (R ∈ ℂ ⋀ (∗ ‘(C ·_ih D)) ∈ ℂ)) → ((R · (C ·_ih D)) · (R · (∗ ‘(C ·_ih D)))) = ((R · R) · ((C ·_ih D) · (∗ ‘(C ·_ih D)))))
19	6, 8	jctir 293	. . . . . . . 8 ⊢ (R ∈ ℝ → (R ∈ ℂ ⋀ (C ·_ih D) ∈ ℂ))
20	8	cjcli 6799	. . . . . . . . 9 ⊢ (∗ ‘(C ·_ih D)) ∈ ℂ
21	6, 20	jctir 293	. . . . . . . 8 ⊢ (R ∈ ℝ → (R ∈ ℂ ⋀ (∗ ‘(C ·_ih D)) ∈ ℂ))
22	18, 19, 21	sylanc 474	. . . . . . 7 ⊢ (R ∈ ℝ → ((R · (C ·_ih D)) · (R · (∗ ‘(C ·_ih D)))) = ((R · R) · ((C ·_ih D) · (∗ ‘(C ·_ih D)))))
23	17, 22	eqtrd 1514	. . . . . 6 ⊢ (R ∈ ℝ → (S · (∗ ‘S)) = ((R · R) · ((C ·_ih D) · (∗ ‘(C ·_ih D)))))
24	23	opreq1d 3991	. . . . 5 ⊢ (R ∈ ℝ → ((S · (∗ ‘S)) · (D ·_ih D)) = (((R · R) · ((C ·_ih D) · (∗ ‘(C ·_ih D)))) · (D ·_ih D)))
25		mulcl 5323	. . . . . . 7 ⊢ ((R ∈ ℂ ⋀ R ∈ ℂ) → (R · R) ∈ ℂ)
26	25, 6, 6	sylanc 474	. . . . . 6 ⊢ (R ∈ ℝ → (R · R) ∈ ℂ)
27	8, 20	mulcli 5341	. . . . . . 7 ⊢ ((C ·_ih D) · (∗ ‘(C ·_ih D))) ∈ ℂ
28	1, 1	hicli 8972	. . . . . . 7 ⊢ (D ·_ih D) ∈ ℂ
29		mul23 5439	. . . . . . 7 ⊢ (((R · R) ∈ ℂ ⋀ ((C ·_ih D) · (∗ ‘(C ·_ih D))) ∈ ℂ ⋀ (D ·_ih D) ∈ ℂ) → (((R · R) · ((C ·_ih D) · (∗ ‘(C ·_ih D)))) · (D ·_ih D)) = (((R · R) · (D ·_ih D)) · ((C ·_ih D) · (∗ ‘(C ·_ih D)))))
30	27, 28, 29	mp3an23 912	. . . . . 6 ⊢ ((R · R) ∈ ℂ → (((R · R) · ((C ·_ih D) · (∗ ‘(C ·_ih D)))) · (D ·_ih D)) = (((R · R) · (D ·_ih D)) · ((C ·_ih D) · (∗ ‘(C ·_ih D)))))
31	26, 30	syl 10	. . . . 5 ⊢ (R ∈ ℝ → (((R · R) · ((C ·_ih D) · (∗ ‘(C ·_ih D)))) · (D ·_ih D)) = (((R · R) · (D ·_ih D)) · ((C ·_ih D) · (∗ ‘(C ·_ih D)))))
32	24, 31	eqtrd 1514	. . . 4 ⊢ (R ∈ ℝ → ((S · (∗ ‘S)) · (D ·_ih D)) = (((R · R) · (D ·_ih D)) · ((C ·_ih D) · (∗ ‘(C ·_ih D)))))
33	3, 32	syl 10	. . 3 ⊢ (D ≠ 0_h → ((S · (∗ ‘S)) · (D ·_ih D)) = (((R · R) · (D ·_ih D)) · ((C ·_ih D) · (∗ ‘(C ·_ih D)))))
34		mul23 5439	. . . . . . . 8 ⊢ ((R ∈ ℂ ⋀ R ∈ ℂ ⋀ (D ·_ih D) ∈ ℂ) → ((R · R) · (D ·_ih D)) = ((R · (D ·_ih D)) · R))
35	28, 34	mp3an3 909	. . . . . . 7 ⊢ ((R ∈ ℂ ⋀ R ∈ ℂ) → ((R · R) · (D ·_ih D)) = ((R · (D ·_ih D)) · R))
36	35, 6, 6	sylanc 474	. . . . . 6 ⊢ (R ∈ ℝ → ((R · R) · (D ·_ih D)) = ((R · (D ·_ih D)) · R))
37	3, 36	syl 10	. . . . 5 ⊢ (D ≠ 0_h → ((R · R) · (D ·_ih D)) = ((R · (D ·_ih D)) · R))
38		ax-his4 8976	. . . . . . . . . . 11 ⊢ ((D ∈ ℋ ⋀ D ≠ 0_h) → 0 < (D ·_ih D))
39	1, 38	mpan 699	. . . . . . . . . 10 ⊢ (D ≠ 0_h → 0 < (D ·_ih D))
40		hiidrcl 8985	. . . . . . . . . . . 12 ⊢ (D ∈ ℋ → (D ·_ih D) ∈ ℝ)
41	1, 40	ax-mp 7	. . . . . . . . . . 11 ⊢ (D ·_ih D) ∈ ℝ
42	41	gt0ne0i 5631	. . . . . . . . . 10 ⊢ (0 < (D ·_ih D) → (D ·_ih D) ≠ 0)
43	39, 42	syl 10	. . . . . . . . 9 ⊢ (D ≠ 0_h → (D ·_ih D) ≠ 0)
44	28	recclzi 5736	. . . . . . . . 9 ⊢ ((D ·_ih D) ≠ 0 → (1 / (D ·_ih D)) ∈ ℂ)
45		mulcom 5326	. . . . . . . . . 10 ⊢ (((1 / (D ·_ih D)) ∈ ℂ ⋀ (D ·_ih D) ∈ ℂ) → ((1 / (D ·_ih D)) · (D ·_ih D)) = ((D ·_ih D) · (1 / (D ·_ih D))))
46	28, 45	mpan2 700	. . . . . . . . 9 ⊢ ((1 / (D ·_ih D)) ∈ ℂ → ((1 / (D ·_ih D)) · (D ·_ih D)) = ((D ·_ih D) · (1 / (D ·_ih D))))
47	43, 44, 46	3syl 20	. . . . . . . 8 ⊢ (D ≠ 0_h → ((1 / (D ·_ih D)) · (D ·_ih D)) = ((D ·_ih D) · (1 / (D ·_ih D))))
48	28	recidzi 5750	. . . . . . . . 9 ⊢ ((D ·_ih D) ≠ 0 → ((D ·_ih D) · (1 / (D ·_ih D))) = 1)
49	39, 42, 48	3syl 20	. . . . . . . 8 ⊢ (D ≠ 0_h → ((D ·_ih D) · (1 / (D ·_ih D))) = 1)
50	47, 49	eqtrd 1514	. . . . . . 7 ⊢ (D ≠ 0_h → ((1 / (D ·_ih D)) · (D ·_ih D)) = 1)
51	2	opreq1i 3987	. . . . . . 7 ⊢ (R · (D ·_ih D)) = ((1 / (D ·_ih D)) · (D ·_ih D))
52	50, 51	syl5eq 1526	. . . . . 6 ⊢ (D ≠ 0_h → (R · (D ·_ih D)) = 1)
53	52	opreq1d 3991	. . . . 5 ⊢ (D ≠ 0_h → ((R · (D ·_ih D)) · R) = (1 · R))
54		mulid2 5437	. . . . . 6 ⊢ (R ∈ ℂ → (1 · R) = R)
55	3, 6, 54	3syl 20	. . . . 5 ⊢ (D ≠ 0_h → (1 · R) = R)
56	37, 53, 55	3eqtrd 1518	. . . 4 ⊢ (D ≠ 0_h → ((R · R) · (D ·_ih D)) = R)
57	56	opreq1d 3991	. . 3 ⊢ (D ≠ 0_h → (((R · R) · (D ·_ih D)) · ((C ·_ih D) · (∗ ‘(C ·_ih D)))) = (R · ((C ·_ih D) · (∗ ‘(C ·_ih D)))))
58	33, 57	eqtrd 1514	. 2 ⊢ (D ≠ 0_h → ((S · (∗ ‘S)) · (D ·_ih D)) = (R · ((C ·_ih D) · (∗ ‘(C ·_ih D)))))
59	8	absvalsqi 6869	. . 3 ⊢ ((abs ‘(C ·_ih D))↑2) = ((C ·_ih D) · (∗ ‘(C ·_ih D)))
60	59	opreq2i 3988	. 2 ⊢ (R · ((abs ‘(C ·_ih D))↑2)) = (R · ((C ·_ih D) · (∗ ‘(C ·_ih D))))
61	58, 60	syl6eqr 1532	1 ⊢ (D ≠ 0_h → ((S · (∗ ‘S)) · (D ·_ih D)) = (R · ((abs ‘(C ·_ih D))↑2)))

Colors of variables: wff set class

Syntax hints: → wi 3 ⋀ wa 223 = wceq 960 ∈ wcel 962 ≠ wne 1592 class class class wbr 2634 ‘cfv 3198 (class class class)co 3979 ℂcc 5252 ℝcr 5253 0cc0 5254 1c1 5255 · cmul 5259 / cdiv 5314 < clt 5506 2c2 5975 ↑cexp 6599 ∗ccj 6781 abscabs 6782 ℋ chil 8812 0_hc0v 8815 ·_ih csp 8817

This theorem is referenced by: pjthlem8 9250

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 966 ax-gen 967 ax-8 968 ax-9 969 ax-10 970 ax-11 971 ax-12 972 ax-13 973 ax-14 974 ax-17 975 ax-4 977 ax-5o 979 ax-6o 982 ax-9o 1127 ax-10o 1144 ax-16 1214 ax-11o 1222 ax-ext 1464 ax-rep 2708 ax-sep 2718 ax-nul 2725 ax-pow 2758 ax-pr 2795 ax-un 2882 ax-inf2 4642 ax-hfi 8970 ax-his1 8973 ax-his4 8976

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 780 df-3an 781 df-ex 985 df-sb 1176 df-eu 1386 df-mo 1387 df-clab 1470 df-cleq 1475 df-clel 1478 df-ne 1594 df-nel 1595 df-ral 1656 df-rex 1657 df-reu 1658 df-rab 1659 df-v 1819 df-sbc 1949 df-csb 2012 df-dif 2060 df-un 2061 df-in 2062 df-ss 2064 df-pss 2066 df-nul 2292 df-if 2374 df-pw 2414 df-sn 2424 df-pr 2425 df-tp 2427 df-op 2428 df-uni 2518 df-int 2548 df-iun 2582 df-br 2635 df-opab 2682 df-tr 2696 df-eprel 2848 df-id 2851 df-po 2856 df-so 2866 df-fr 2933 df-we 2950 df-ord 2967 df-on 2968 df-lim 2969 df-suc 2970 df-om 3148 df-xp 3200 df-rel 3201 df-cnv 3202 df-co 3203 df-dm 3204 df-rn 3205 df-res 3206 df-ima 3207 df-fun 3208 df-fn 3209 df-f 3210 df-f1 3211 df-fo 3212 df-f1o 3213 df-fv 3214 df-rdg 3948 df-opr 3981 df-oprab 3982 df-1st 4095 df-2nd 4096 df-1o 4149 df-oadd 4151 df-omul 4152 df-er 4277 df-ec 4279 df-qs 4282 df-en 4386 df-dom 4387 df-sdom 4388 df-sup 4589 df-ni 5020 df-pli 5021 df-mi 5022 df-lti 5023 df-plpq 5055 df-mpq 5056 df-enq 5057 df-nq 5058 df-plq 5059 df-mq 5060 df-rq 5061 df-ltq 5062 df-1q 5063 df-np 5106 df-1p 5107 df-plp 5108 df-mp 5109 df-ltp 5110 df-plpr 5184 df-mpr 5185 df-enr 5186 df-nr 5187 df-plr 5188 df-mr 5189 df-ltr 5190 df-0r 5191 df-1r 5192 df-m1r 5193 df-c 5260 df-0 5261 df-1 5262 df-i 5263 df-r 5264 df-plus 5265 df-mul 5266 df-lt 5267 df-sub 5376 df-neg 5378 df-pnf 5507 df-mnf 5508 df-xr 5509 df-ltxr 5510 df-le 5511 df-div 5723 df-n 5939 df-2 5984 df-n0 6132 df-z 6168 df-seq1 6509 df-exp 6600 df-sqr 6702 df-re 6783 df-im 6784 df-cj 6785 df-abs 6786