Bibliographic Cross-Reference - Metamath Proof Explorer

Bibliographic Cross-Reference

Bibliographic Cross-References   This table collects in one place the bibliographic references made in the Metamath Proof Explorer's axiom, definition, and theorem Descriptions. If you are studying a particular set theory book, this list can be handy for finding out where any corresponding Metamath theorems might be located. Keep in mind that we usually give only one reference for a theorem that may appear in several books, so it can also be useful to browse the Related Theorems around a theorem of interest.

Bibliographic Cross-Reference for the Metamath Proof Explorer

Bibliographic Reference	Description	Metamath Proof Explorer Page(s)
[AkhiezerGlazman] p. 30	Definition of operator	df-hosum 9637
[AkhiezerGlazman] p. 39	Definition of linear operator norm	df-nmo 8275
[AkhiezerGlazman] p. 64	Theorem	hmopidmch 10204  hmopidmcht 10206
[AkhiezerGlazman] p. 65	Theorem 1	pjcmmul1 10253  pjcmmul2 10254
[AkhiezerGlazman] p. 72	Theorem	cnvunopt 9972  unoplint 9974
[AkhiezerGlazman] p. 72	Equation 2	unopadj2t 9992  unopadjt 9973
[AkhiezerGlazman] p. 73	Theorem	elunop2t 10067  lnopuni 10066
[AkhiezerGlazman] p. 80	Proposition 1	adjlnopt 10148
[Apostol] p. 18	Theorem I.1	addcan 5274  addcant 5275
[Apostol] p. 18	Theorem I.2	negeu 5278
[Apostol] p. 18	Theorem I.3	negsub 5304  negsubt 5305
[Apostol] p. 18	Theorem I.4	negneg 5313  negnegt 5316
[Apostol] p. 18	Theorem I.5	subdi 5352  subdir 5353  subdirt 5351  subdit 5350
[Apostol] p. 18	Theorem I.6	mul01 5354  mul01t 5366  mul02 5355  mul02t 5367
[Apostol] p. 18	Theorem I.7	mulcan 5610  mulcant 5612  mulcant2 5611
[Apostol] p. 18	Theorem I.8	receu 5621
[Apostol] p. 18	Theorem I.9	divrec 5651  divrect 5653  divrecz 5652
[Apostol] p. 18	Theorem I.10	recrec 5676  recrect 5683
[Apostol] p. 18	Theorem I.11	mul0or 5614  mul0ort 5616
[Apostol] p. 18	Theorem I.12	mul2neg 5370  mul2negt 5377  mulneg1 5368  mulneg1t 5374
[Apostol] p. 18	Theorem I.13	divadddiv 5695  divadddivt 5691
[Apostol] p. 18	Theorem I.14	divmuldiv 5693  divmuldivt 5687
[Apostol] p. 18	Theorem I.15	divdivdiv 5696  divdivdivt 5692
[Apostol] p. 20	Axiom 7	rpaddclt 6178  rpmulclt 6179
[Apostol] p. 20	Axiom 9	0nrp 6181
[Apostol] p. 20	Theorem I.17	lttr 5510
[Apostol] p. 20	Theorem I.18	ltadd1 5516
[Apostol] p. 20	Theorem I.19	ltmul1 5729  ltmul1i 5728  ltmul1t 5737  ltmul2 5741  ltmul2t 5738  ltmullem 5565
[Apostol] p. 20	Theorem I.20	msqgt0 5538  msqgt0t 5540
[Apostol] p. 20	Theorem I.21	lt01 5604
[Apostol] p. 20	Theorem I.23	lt0neg1t 5592  ltneg 5528  ltnegt 5579
[Apostol] p. 20	Theorem I.25	lt2add 5521  lt2addt 5568
[Apostol] p. 20	Definition of positive numbers	df-rp 6170
[Apostol] p. 21	Exercise 4	recgt0 5767  recgt0i 5721  recgt0t 5766
[Apostol] p. 22	Definition of integers	df-z 6034
[Apostol] p. 22	Definition of positive integers	dfnn2 5835
[Apostol] p. 22	Definition of rationals	df-q 6145
[Apostol] p. 24	Theorem I.26	supeu 4504  supeui 4509
[Apostol] p. 26	Theorem I.28	nnunb 5968
[Apostol] p. 26	Theorem I.29	arch 5969
[Apostol] p. 28	Exercise 2	btwnz 6114
[Apostol] p. 28	Exercise 3	nnreclt 5970
[Apostol] p. 28	Exercise 4	rebtwnz 6121
[Apostol] p. 28	Exercise 5	zbtwnre 6120
[Apostol] p. 28	Exercise 6	qbtwnre 6167
[Apostol] p. 28	Exercise 10(a)	zneo 6098  zneoOLD 6099
[Apostol] p. 29	Theorem I.35	sqrth 6580
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nn 5825
[Apostol] p. 34	Theorem I.37 (well-ordering principle)	nnwo 6341
[Apostol] p. 361	Remark	crmul 6622  crrecz 6623
[Apostol] p. 363	Remark	absgt0 6729
[Apostol] p. 363	Example	abssub 6732
[BellMachover] p. 36	Lemma 10.3	id1 60
[BellMachover] p. 97	Definition 10.1	df-eu 1359
[BellMachover] p. 460	Notation	df-mo 1360
[BellMachover] p. 460	Definition	mo3 1378
[BellMachover] p. 461	Axiom Ext	ax-ext 1436
[BellMachover] p. 462	Theorem 1.1	bm1.1 1439
[BellMachover] p. 463	Axiom Rep	axrep5 2666
[BellMachover] p. 463	Scheme Sep	axsep 2670
[BellMachover] p. 463	Theorem 1.3ii	bm1.3ii 2674
[BellMachover] p. 466	Axiom Pow	axpow2 2712
[BellMachover] p. 466	Axiom Union	axun2 2832
[BellMachover] p. 468	Definition	df-ord 2914
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 2929
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 2935
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 2931
[BellMachover] p. 471	Definition of N	df-om 3095
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 2982
[BellMachover] p. 471	Definition of Lim	df-lim 2916
[BellMachover] p. 472	Axiom Inf	zfinf 4550
[BellMachover] p. 473	Theorem 2.8	limom 3109
[BellMachover] p. 477	Equation 3.1	df-r1 4567
[BellMachover] p. 478	Definition	rankval2 4594
[BellMachover] p. 478	Theorem 3.3(i)	r1ord3 4581
[BellMachover] p. 480	Axiom Reg	zfreg2 4521
[BellMachover] p. 488	Axiom AC	ac5 4676  aceq4 4658
[BellMachover] p. 490	Definition of aleph	alephval3 4826
[BeltramettiCassinelli] p. 107	Remark 10.3.5	atom1d 10402
[BeltramettiCassinelli] p. 166	Theorem 14.8.4	irred 10443  irredt 10444
[BeltramettiCassinelli1] p. 400	Proposition P8(ii)	atoml2 10432
[Beran] p. 3	Definition of join	dfchj3 9454  sshjval3t 9455
[Beran] p. 39	Theorem 2.3(i)	cmcm2 9667  cmcm2i 9672  cmcm2t 9690
[Beran] p. 40	Theorem 2.3(iii)	lecm 9676  lecmi 9677  lecmt 9691
[Beran] p. 45	Theorem 3.4	cmcmlem 9665
[Beran] p. 49	Theorem 4.2	cm2jt 9694
[Beran] p. 95	Definition	df-sh 9227  sh 9229
[Beran] p. 95	Lemma 3.1(S5)	his5t 9102
[Beran] p. 95	Lemma 3.1(S6)	his6t 9114
[Beran] p. 95	Lemma 3.1(S7)	his7t 9105
[Beran] p. 95	Lemma 3.2(S8)	ho01 9885
[Beran] p. 95	Lemma 3.2(S9)	hoeq1t 9887
[Beran] p. 95	Lemma 3.2(S10)	ho02 9886
[Beran] p. 95	Lemma 3.2(S11)	hoeq2t 9888
[Beran] p. 95	Postulate (S1)	ax-his1 9098  his1 9115
[Beran] p. 95	Postulate (S2)	ax-his2 9099
[Beran] p. 95	Postulate (S3)	ax-his3 9100
[Beran] p. 95	Postulate (S4)	ax-his4 9101
[Beran] p. 96	Definition of norm	df-hnorm 9137  normvalt 9139
[Beran] p. 96	Definition for Cauchy sequence	hcau 9201
[Beran] p. 96	Definition of Cauchy sequence	df-hcau 9200
[Beran] p. 96	Definition of complete subspace	chsscm 9263
[Beran] p. 96	Definition of converge	df-hlim 9206  hlim 9207
[Beran] p. 97	Theorem 3.3(i)	norm-i 9149  norm-it 9145
[Beran] p. 97	Theorem 3.3(ii)	norm-ii 9153  norm-iit 9154  normlem0 9124  normlem1 9125  normlem2 9126  normlem3 9127  normlem4 9128  normlem5 9129  normlem6 9130  normlem7 9131  normlem7tALT 9134
[Beran] p. 97	Theorem 3.3(iii)	norm-iii 9155  norm-iiit 9156
[Beran] p. 98	Remark 3.4	bcsALT 9195  bcsHIL 9196  bcst 9197
[Beran] p. 98	Remark 3.4(B)	normlem9at 9136  normpar 9170  normpart 9171
[Beran] p. 98	Remark 3.4(C)	normpyct 9162  normpyth 9158  normpytht 9161
[Beran] p. 99	Remark	lnfn0 10100  lnfn0t 10105  lnop0 10024  lnop0t 10020
[Beran] p. 99	Theorem 3.5(i)	nmcfnex 10115  nmcfnext 10117  nmcopex 10086  nmcopexlem1 10080  nmcopext 10088
[Beran] p. 99	Theorem 3.5(ii)	nmcfnlb 10116  nmcfnlbt 10118  nmcoplb 10087  nmcoplbt 10089
[Beran] p. 99	Theorem 3.5(iii)	lnfncon 10119  lnfncont 10120  lnopcon 10092  lnopcont 10093
[Beran] p. 99	Definition of operator	df-hosum 9637
[Beran] p. 100	Lemma 3.6	normpar2 9172  projlem1 9316  projlem10 9325  projlem11 9326  projlem12 9327  projlem13 9328  projlem14 9329  projlem15 9330  projlem16 9331  projlem17 9332  projlem17 9332  projlem2 9317  projlem21 9336  projlem22 9337  projlem3 9318  projlem5 9320  projlem8 9323  projlem8 9323  projlem9 9324
[Beran] p. 101	Lemma 3.6	norm3adif 9164  norm3adift 9169  norm3dif 9163  norm3dift 9166  projlem 9347  projlem18 9333  projlem19 9334  projlem20 9335  projlem23 9338  projlem24 9339  projlem25 9340  projlem26 9341  projlem27 9342  projlem28 9343  projlem29 9344  projlem30 9345  projlem31 9346  projlem4 9319  projlem6 9321  projlem7 9322
[Beran] p. 102	Theorem 3.7(i)	chocuni 9302  pjpjth 9388  pjpjtht 9387  pjth 9362  pjtht 9363
[Beran] p. 102	Theorem 3.7(ii)	ococ 9376  ococt 9377
[Beran] p. 103	Remark 3.8	nlelch 10123
[Beran] p. 104	Theorem 3.9	riesz3 10124  riesz4 10125  riesz4t 10126
[Beran] p. 104	Theorem 3.10	cnlnadj 10138  cnlnadjeu 10139  cnlnadjeut 10140  cnlnadjlem1 10129  cnlnadjt 10141  nmopadjle 10150
[Beran] p. 106	Theorem 3.11(v)	nmopadj 10152
[Beran] p. 106	Theorem 3.11(ii)	adjmult 10153
[Beran] p. 106	Theorem 3.11(iv)	adjadjt 9990
[Beran] p. 106	Theorem 3.11(vi)	nmopcoadj 10162  nmopcoadj2 10163
[Beran] p. 106	Theorem 3.11(iii)	adjaddt 10154
[Beran] p. 106	Theorem 3.11(viii)	adjco 10161  pjadj2co 10256  pjadjco 10214
[Beran] p. 107	Definition	closedsub 9244  df-ch 9243
[Beran] p. 107	Remark 3.12	chocclt 9314  chsscm 9263  occl 9311  occllem1 9303  occllem2 9304  occllem3 9305  occllem4 9306  occllem5 9307  occllem6 9308  occllem7 9309  occllem8 9310  occlt 9312  ocsh 9286  shocclt 9313  shocsh 9287
[Beran] p. 107	Remark 3.12(B)	ococint 9426
[Beran] p. 107	Remark 3.12(C)	ch2 9265  chcmh 9264
[Beran] p. 108	Theorem 3.13	chintclt 9425
[Beran] p. 109	Property (i)	pjadj 9749  pjadj2t 10238  pjadj3t 10239  pjadjt 9761
[Beran] p. 109	Property (ii)	pjidm 9748  pjidmco 10230  pjidmcot 10233
[Beran] p. 110	Definition of projector ordering	pjord 10226
[Beran] p. 111	Remark	ho0valt 9807  pjch1t 9746
[Beran] p. 111	Definition	df-hfmul 9641  df-hfsum 9640  df-hodif 9639  df-homul 9638  df-hosum 9637
[Beran] p. 111	Lemma 4.4(i)	pjot 9747
[Beran] p. 111	Lemma 4.4(ii)	pjch 9394  pjcht 9770
[Beran] p. 111	Lemma 4.4(iii)	pjoc2 9400  pjoc2t 9401
[Beran] p. 112	Theorem 4.5(i)->(ii)	pjss2 9756
[Beran] p. 112	Theorem 4.5(i)->(iv)	pjssm 9757  pjssmt 10218
[Beran] p. 112	Theorem 4.5(i)<->(ii)	pjss2co 10217
[Beran] p. 112	Theorem 4.5(i)<->(iii)	pjss1co 10216
[Beran] p. 112	Theorem 4.5(i)<->(vi)	pjnormss 10221
[Beran] p. 112	Theorem 4.5(iv)->(v)	pjssge0 9758  pjssge0t 10219
[Beran] p. 112	Theorem 4.5(v)<->(vi)	pjdifnorm 9759  pjdifnormt 10220
[ChoquetDD] p. 2	Definition of mapping	df-mpt 4013
[Cohen] p. 301	Remark	logoprlemOLD 8622  relogoprlem 8604
[Cohen] p. 301	Property 2	logmultOLD 8623  relogmult 8605
[Cohen] p. 301	Property 3	logdivtOLD 8624  relogdivt 8606
[Cohen] p. 301	Property 4	logexptOLD 8625  relogexpt 8609
[Cohen] p. 301	Property 1a	log1 8601  log1OLD 8620
[Cohen] p. 301	Property 1b	loge 8602  logeOLD 8621
[Diestel] p. 2	Definition	df-sgra 8963
[Diestel] p. 28	Definition	df-pgra 8960
[Diestel] p. 28	Definition of hypergraph	ishgrag 8951
[Eisenberg] p. 67	Definition 5.3	df-dif 2020
[Eisenberg] p. 82	Definition 6.3	dfom3 4554
[Eisenberg] p. 125	Definition 8.21	df-map 4262
[Eisenberg] p. 216	Example 13.2(4)	omenps 4560
[Eisenberg] p. 310	Theorem 19.8	cardprc 4784
[Eisenberg] p. 310	Corollary 19.7(2)	cardsdom 4760
[Enderton] p. 18	Axiom of Empty Set	axnul 2677
[Enderton] p. 19	Definition	df-tp 2386
[Enderton] p. 26	Exercise 5	unissb 2496
[Enderton] p. 26	Exercise 10	pwel 2727
[Enderton] p. 28	Exercise 7(b)	pwun 2791
[Enderton] p. 30	Theorem "Distributive laws"	iinun2 2577  iunin2 2576
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2 2579  iundif2 2578
[Enderton] p. 32	Exercise 20	unineq 2226
[Enderton] p. 33	Exercise 23	iinuni 2583
[Enderton] p. 33	Exercise 25	iununi 2584
[Enderton] p. 33	Exercise 24(a)	iinpw 2585
[Enderton] p. 33	Exercise 24(b)	iunpw 2877  iunpwss 2586
[Enderton] p. 36	Definition	opthwiener 2770
[Enderton] p. 38	Exercise 6(a)	unipw 2724
[Enderton] p. 38	Exercise 6(b)	pwuni 2725
[Enderton] p. 41	Lemma 3D	opeluu 2842  rnexg 3313
[Enderton] p. 41	Exercise 8	dmuni 3276  rnuni 3408
[Enderton] p. 42	Definition of a function	dffun6 3480  dffun7 3481
[Enderton] p. 43	Definition of function value	funfv2 3710
[Enderton] p. 43	Definition of single-rooted	funcnv 3497
[Enderton] p. 44	Definition (d)	dfima2 3356  dfima3 3357
[Enderton] p. 47	Theorem 3H	fvco2 3714
[Enderton] p. 49	Axiom of Choice (first form)	ac7 4672  ac7g 4673  aceq3 4657  aceq4 4658  aceq5 4664  aceq6a 4665  aceq6b 4666  aceq7 4667  aceqkm 4705
[Enderton] p. 50	Theorem 3K(a)	imaiun 3803
[Enderton] p. 52	Definition	df-map 4262
[Enderton] p. 53	Exercise 21	coass 3454
[Enderton] p. 53	Exercise 27	dmco2 3446
[Enderton] p. 53	Exercise 14(a)	funin 3506
[Enderton] p. 53	Exercise 22(a)	imass2 3384
[Enderton] p. 54	Remark	ixpf 4294  ixpssmap 4301
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 4286
[Enderton] p. 55	Axiom of Choice (second form)	ac9s 4688
[Enderton] p. 56	Theorem 3M	erref 4213
[Enderton] p. 57	Lemma 3N	erthi 4219
[Enderton] p. 57	Definition	df-ec 4201
[Enderton] p. 58	Definition	df-qs 4204
[Enderton] p. 60	Theorem 3Q	th3q 4255  th3qcor 4254  th3qlem1 4252  th3qlem2 4253
[Enderton] p. 61	Exercise 35	df-ec 4201
[Enderton] p. 65	Exercise 56(a)	dmun 3274
[Enderton] p. 68	Definition of successor	df-suc 2917
[Enderton] p. 71	Definition	df-tr 2649  dftr4 2653
[Enderton] p. 72	Theorem 4E	unisuc 3009
[Enderton] p. 73	Exercise 6	unisuc 3009
[Enderton] p. 79	Theorem 4I(A1)	nna0 4161
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 4163
[Enderton] p. 79	Definition of operation value	df-opr 3904
[Enderton] p. 80	Theorem 4J(A1)	nnm0 4162
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 4164
[Enderton] p. 81	Theorem 4K(1)	nnaass 4175
[Enderton] p. 81	Theorem 4K(2)	nna0r 4165  nnacom 4171
[Enderton] p. 81	Theorem 4K(3)	nndi 4176
[Enderton] p. 81	Theorem 4K(4)	nnmass 4177
[Enderton] p. 81	Theorem 4K(5)	nnmcom 4179
[Enderton] p. 82	Exercise 16	nnm0r 4166  nnmsucr 4178
[Enderton] p. 88	Exercise 23	nnaordex 4187
[Enderton] p. 129	Definition	bren 4313  df-en 4305
[Enderton] p. 132	Theorem 6B(b)	canth 3846
[Enderton] p. 133	Exercise 1	xpomen 7393
[Enderton] p. 133	Exercise 2	qnnen 7397
[Enderton] p. 134	Theorem (Pigeonhole Principle)	php 4445
[Enderton] p. 135	Corollary 6C	php3 4447
[Enderton] p. 136	Corollary 6E	nneneq 4444
[Enderton] p. 136	Corollary 6D(a)	pssinf 4459
[Enderton] p. 136	Corollary 6D(b)	ominf 4460
[Enderton] p. 137	Lemma 6F	pssnn 4465
[Enderton] p. 138	Corollary 6G	ssfi 4467
[Enderton] p. 139	Theorem 6H(c)	mapen 4423
[Enderton] p. 142	Theorem 6I(3)	xpcdaen 4854
[Enderton] p. 142	Theorem 6I(4)	mapcdaen 4855
[Enderton] p. 143	Theorem 6J	cda0en 4848  cda1en 4849
[Enderton] p. 144	Exercise 13	iunfi 4495  unifi 4484  unifi2 4485
[Enderton] p. 144	Corollary 6K	undif2 2312  unfi 4480  unfi2 4481
[Enderton] p. 145	Figure 38	ffoss 3650
[Enderton] p. 145	Definition	df-dom 4306
[Enderton] p. 146	Example 1	domen 4315  domeng 4316
[Enderton] p. 146	Example 3	nndomo 4452  omsdomnn 4461
[Enderton] p. 149	Theorem 6L(a)	cdadom2 4857
[Enderton] p. 149	Theorem 6L(c)	mapdom1 4424  xpdom1 4377  xpdom1g 4378
[Enderton] p. 149	Theorem 6L(d)	mapdom2 4426
[Enderton] p. 151	Theorem 6M	zorn 4721
[Enderton] p. 151	Theorem 6M(4)	ac8 4687  aceq5 4664
[Enderton] p. 159	Theorem 6Q	unictb 7469
[Enderton] p. 162	Lemma 6R	infxpidm 7458
[Enderton] p. 164	Example	infdif 7462
[Enderton] p. 165	Exercise 34	infmap1 7467
[Enderton] p. 168	Definition	df-po 2804
[Enderton] p. 192	Theorem 7M(a)	onel 3061
[Enderton] p. 192	Theorem 7M(b)	ontr1 2966
[Enderton] p. 192	Theorem 7M(c)	onirr 3060
[Enderton] p. 193	Corollary 7N(b)	0elon 2985
[Enderton] p. 193	Corollary 7N(c)	onsuc 3068
[Enderton] p. 193	Corollary 7N(d)	ssonuni 2958
[Enderton] p. 194	Remark	onprc 2952
[Enderton] p. 194	Exercise 16	suc11 3056
[Enderton] p. 197	Definition	df-card 4740
[Enderton] p. 197	Theorem 7P	carden 4755
[Enderton] p. 200	Exercise 25	tfis 3090
[Enderton] p. 202	Lemma 7T	r1tr 4578
[Enderton] p. 202	Definition	df-r1 4567
[Enderton] p. 202	Theorem 7Q	r1val1 4582
[Enderton] p. 204	Theorem 7V(b)	rankval4 4626
[Enderton] p. 206	Theorem 7X(b)	en2lp 4526
[Enderton] p. 207	Exercise 30	rankpr 4616  rankpw 4608  rankuniss 4625
[Enderton] p. 207	Exercise 34	opthreg 4528
[Enderton] p. 208	Exercise 35	suc11reg 4529
[Enderton] p. 212	Definition of aleph	alephval3 4826
[Enderton] p. 213	Theorem 8A(a)	alephord2 4799
[Enderton] p. 213	Theorem 8A(b)	cardalephex 4809
[Enderton] p. 222	Definition of kard	karden 4650  kardex 4649
[Enderton] p. 240	Exercise 25	oarec 4134
[Enderton] p. 257	Definition of cofinality	cflim 4832
[FreydScedrov] p. 283	Axiom of Infinity	ax-inf 4546  inf1 4531  inf2 4532
[Gleason] p. 117	Proposition 9-2.1	df-enq 4960  enqer 4969
[Gleason] p. 117	Proposition 9-2.2	df-1q 4966  df-nq 4961
[Gleason] p. 117	Proposition 9-2.3	df-plpq 4958  df-plq 4962
[Gleason] p. 119	Proposition 9-2.4	caoprmo 4010  df-mpq 4959  df-mq 4963
[Gleason] p. 119	Proposition 9-2.5	df-rq 4964
[Gleason] p. 119	Proposition 9-2.6	ltexpq 5003  ltexpq2 5004
[Gleason] p. 120	Proposition 9-2.6(i)	halfpq 5005  ltbtwnpq 5007
[Gleason] p. 120	Proposition 9-2.6(ii)	ltapq 4999
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmpq 5000
[Gleason] p. 120	Proposition 9-2.6(iv)	ltrpq 5008
[Gleason] p. 121	Definition 9-3.1	df-np 5009
[Gleason] p. 121	Definition 9-3.1 (ii)	prcdpq 5020
[Gleason] p. 121	Definition 9-3.1(iii)	prnmax 5022
[Gleason] p. 122	Definition	df-1p 5010
[Gleason] p. 122	Remark (1)	prub 5021
[Gleason] p. 122	Lemma 9-3.4	prlem934 5062  prlem934a 5060  prlem934b 5061
[Gleason] p. 122	Proposition 9-3.2	df-ltp 5013
[Gleason] p. 122	Proposition 9-3.3	ltsopr 5059  psslinpr 5058  supexpr 5086  suplem1pr 5084  suplem2pr 5085
[Gleason] p. 123	Proposition 9-3.5	addclpr 5043  addclprlem1 5041  addclprlem2 5042  df-plp 5011
[Gleason] p. 123	Proposition 9-3.5(i)	addasspr 5047
[Gleason] p. 123	Proposition 9-3.5(ii)	addcompr 5046
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 5063
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 5072  ltexprlem1 5065  ltexprlem2 5066  ltexprlem3 5067  ltexprlem4 5068  ltexprlem5 5069  ltexprlem6 5070  ltexprlem7 5071
[Gleason] p. 123	Proposition 9-3.5(v)	ltapr 5074  ltaprlem 5073
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanpr 5075
[Gleason] p. 124	Lemma 9-3.6	prlem936 5078  prlem936a 5076  prlem936b 5077
[Gleason] p. 124	Proposition 9-3.7	df-mp 5012  mulclpr 5045  mulclprlem 5044  reclem1pr 5079  reclem2pr 5080
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 5056
[Gleason] p. 124	Proposition 9-3.7(i)	mulasspr 5049
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcompr 5048
[Gleason] p. 124	Proposition 9-3.7(iii)	distrpr 5055
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 5083  reclem3pr 5081  reclem4pr 5082
[Gleason] p. 126	Proposition 9-4.1	df-enr 5089  df-mpr 5088  df-plpr 5087  enrer 5099
[Gleason] p. 126	Proposition 9-4.2	df-0r 5094  df-1r 5095  df-nr 5090
[Gleason] p. 126	Proposition 9-4.3	df-mr 5092  df-plr 5091  negexsr 5134  recexsr 5139  recexsrlem 5135
[Gleason] p. 127	Proposition 9-4.4	df-ltr 5093
[Gleason] p. 130	Proposition 10-1.3	creui 6625  creur 6624  cru 6618  crut 6619  crutOLD 6620
[Gleason] p. 130	Definition 10-1.1(v)	axcnre 5209
[Gleason] p. 132	Definition 10-3.1	crim 6659  crimOLD 6660  crimt 6655  crimtOLD 6656  crre 6657  crreOLD 6658  crret 6653  crretOLD 6654
[Gleason] p. 132	Definition 10-3.2	cjvalt 6646
[Gleason] p. 133	Definition 10.36	absval2 6727  absval2t 6738
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 6674  cjaddt 6698
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 6675  cjmult 6699
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 6664  cjcjt 6697
[Gleason] p. 133	Proposition 10-3.4(f)	cjreb 6667  cjrebt 6686  cjret 6696  rereb 6666  reret 6685
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 6684  addcjt 6701
[Gleason] p. 133	Proposition 10-3.7(a)	absvalt 6645
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 6731  abscjt 6720
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 6728  abs00t 6739
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 6779  releabst 6775
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 6733  absmult 6744
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 6736  sqabsaddt 6734
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 6780  abstrit 6786
[Gleason] p. 134	Definition 10-4.1	df-exp 6452  exp0t 6454  expp1t 6457
[Gleason] p. 135	Proposition 10-4.2(a)	expaddt 6478
[Gleason] p. 135	Proposition 10-4.2(b)	expmult 6479
[Gleason] p. 135	Proposition 10-4.2(c)	mulexpt 6476
[Gleason] p. 140	Exercise 1	znnen 7396
[Gleason] p. 141	Definition 11-2.1	fzvalt 6352
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 7004
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 7017
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 7015
[Gleason] p. 171	Corollary 12-2.2	climmulc 7020  climmulc2 7016
[Gleason] p. 172	Corollary 12-2.5	climfnrcl 6999  climrecl 6998
[Gleason] p. 172	Proposition 12-2.4(c)	climcj 7037
[Gleason] p. 173	Definition 12-3.1	df-ltxr 5413  df-xr 5412  ltxrt 5418
[Gleason] p. 175	Definition 12-4.1	df-limsup 6411  limsupvalt 6412
[Gleason] p. 180	Theorem 12-5.1	climsup 7042
[Gleason] p. 180	Theorem 12-5.3	caucvg3 7054  caucvg3a 7051  caucvg3t 7055  climcau 7043
[Gleason] p. 181	Remark	cau2 6801
[Gleason] p. 182	Exercise 3	cvgcmp 7071
[Gleason] p. 182	Exercise 4	cvgrat 7141
[Gleason] p. 195	Theorem 13-2.12	abs1m 6792
[Gleason] p. 217	Lemma 13-4.1	btwnzge0t 6139
[Gleason] p. 223	Definition 14-1.1	df-met 7680
[Gleason] p. 223	Definition 14-1.1(a)	met0 7702
[Gleason] p. 223	Definition 14-1.1(b)	metgt0 7709
[Gleason] p. 223	Definition 14-1.1(c)	metsym 7703
[Gleason] p. 223	Definition 14-1.1(d)	mettri 7704  mettriOLD 7705
[Gleason] p. 225	Definition 14-1.5	metxp 7722  metxpcl 7720  metxpdval 7717  metxpfval 7719  metxptval 7718
[Gleason] p. 230	Proposition 14-2.6	xplm 7857  xplmi 7855  xplmi2 7856
[Gleason] p. 240	Theorem 14-4.3	metcnp4 7852
[Gleason] p. 240	Proposition 14-4.2	metcnp3 7783
[Gleason] p. 243	Proposition 14-4.16	addcn 7868  mulcn 7870  subcn 7869
[Gleason] p. 295	Remark	bcval4t 6850
[Gleason] p. 295	Equation 2	bcpasc 6858  bcpasc2 6856  bcpasc2t 6857  bcpasct 6859
[Gleason] p. 295	Definition of binomial coefficient	bcvalt 6846  df-bc 6845
[Gleason] p. 296	Remark	bcn0t 6852  bcnnt 6853
[Gleason] p. 296	Theorem 15-2.8	binom 6961
[Gleason] p. 308	Equation 2	ef0 7228
[Gleason] p. 308	Equation 3	efcj 7229  efcjt 7230
[Gleason] p. 309	Corollary 15-4.3	efne0t 7262
[Gleason] p. 309	Corollary 15-4.4	efexpt 7265
[Gleason] p. 310	Equation 14	sinadd 7344  sinaddt 7346
[Gleason] p. 310	Equation 15	cosadd 7345  cosaddt 7347
[Gleason] p. 311	Equation 17	sincossqt 7354
[Gleason] p. 311	Equation 18	cosbndt 7359  sinbndt 7358
[Gleason] p. 311	Lemma 15-4.7	sqeqor 6529  sqeqort 6531
[Gleason] p. 311	Definition of pi	df-pi 7195
[Godowski] p. 730	Equation SF	goeq 10324
[GodowskiGreechie] p. 249	Equation IV	3oa 9744
[Goldberg] p. 10	Definition of operator	df-hosum 9637
[Halmos] p. 31	Theorem 17.3	riesz1t 10127  riesz2t 10128
[Halmos] p. 35	Definition of operator	df-hosum 9637
[Halmos] p. 41	Definition of Hermitian	hmopadj2t 9995
[Halmos] p. 42	Definition of projector ordering	pjord 10226
[Halmos] p. 43	Theorem 26.1	elpjhmopt 10237  elpjidmt 10236  pjnmop 10200
[Halmos] p. 44	Remark	pjinorm 9752  pjinormt 9763
[Halmos] p. 44	Theorem 26.2	elpjcht 10240  pjrn 9778  pjrnt 9783  pjvect 9772
[Halmos] p. 44	Theorem 26.3	pjnorm2t 9803
[Halmos] p. 44	Theorem 26.4	hmopidmpj 10205  hmopidmpjt 10207
[Halmos] p. 45	Theorem 27.1	pjinvar 10243
[Halmos] p. 45	Theorem 27.3	pjoc 10232  pjocvect 9773
[Halmos] p. 45	Theorem 27.4	pjorthco 10222
[Halmos] p. 48	Theorem 29.2	pjsspos 10225
[Halmos] p. 48	Theorem 29.3	pjssdif1 10228  pjssdif2 10227
[Halmos] p. 50	Definition of spectrum	df-spec 9912
[Hamilton] p. 28	Definition 2.1	ax-1 4
[Hamilton] p. 31	Example 2.7(a)	id1 60
[Hamilton] p. 73	Rule 1	ax-mp 7
[Hamilton] p. 74	Rule 2	ax-gen 955
[Herstein] p. 54	Exercise 28	df-grp 7919
[Herstein] p. 55	Lemma 2.2.1(a)	grpideu 7935
[Herstein] p. 55	Lemma 2.2.1(b)	grpinveu 7946
[Herstein] p. 55	Lemma 2.2.1(c)	grp2inv 7961
[Herstein] p. 55	Lemma 2.2.1(d)	grpinvop 7963
[Herstein] p. 57	Exercise 1	isgrp2i 7959
[Holland] p. 1519	Theorem 2	sumdmd 10468
[Holland] p. 1520	Lemma 5	cdj1 10479  cdj3 10487  cdj3lem1 10480  cdjreu 10478
[Holland] p. 1524	Lemma 7	mddmdin0 10477
[Hughes] p. 14	Definition of operator	df-hosum 9637
[Hughes] p. 44	Equation 1.21b	ax-his3 9100
[Hughes] p. 47	Definition of projection operator	dfpjopt 10235
[Hughes] p. 49	Equation 1.30	eighmret 10017  eigre 9891  eigret 9892
[Hughes] p. 49	Equation 1.31	eighmortht 10018  eigorth 9894  eigortht 9895
[Hughes] p. 137	Remark (ii)	eigpos 9893
[Jech] p. 4	Definition of class	cv 1098  cvjust 1448
[Jech] p. 42	Lemma 6.1	alephexp1 7477
[Jech] p. 42	Equation 6.1	alephadd 7475  alephmul 7476
[Jech] p. 43	Lemma 6.2	infmap2 7474
[Jech] p. 71	Lemma 9.3	jech9.3 4590
[Jech] p. 72	Equation 9.3	scott0 4641  scottex 4640
[Jech] p. 72	Exercise 9.1	rankval4 4626
[Jech] p. 72	Scheme "Collection Principle"	cp 4646
[Jech] p. 78	Definition implied by the footnote	opthprc 3183
[KalishMontague] p. 81	Axiom B7' in footnote 1	ax-9 1102
[Kalmbach] p. 14	Definition of lattice	chabs1 9570  chabs1t 9568  chabs2 9571  chabs2t 9569  chjass 9538  chjasst 9585
[Kalmbach] p. 15	Definition of atom	df-at 10387  elat 10388
[Kalmbach] p. 15	Definition of covers	cvbr2t 10334
[Kalmbach] p. 20	Definition of commutes	cmbr 9664  cmbrt 9658  df-cm 9657
[Kalmbach] p. 22	Remark	pjoml5 9662  pjoml5t 9687
[Kalmbach] p. 22	Definition	pjoml2 9659  pjoml2t 9685
[Kalmbach] p. 22	Theorem 2(v)	cmcm 9666  cmcmi 9671  cmcmt 9688
[Kalmbach] p. 22	Theorem 2(ii)	omls 9375  pjoml 9397  pjomlt 9398
[Kalmbach] p. 23	Remark	cmbr2 9670  cmcm3 9668  cmcm3i 9673  cmcm3t 9689  cmcm4 9669
[Kalmbach] p. 23	Lemma 3	cmbr3 9674  cmbr3t 9682
[Kalmbach] p. 25	Theorem 5	fh1 9695  fh1t 9692  fh2 9696  fh2t 9693
[Kalmbach] p. 65	Remark	chjatom 10406  chslej 9510  chslejt 9550  shslej 9467  shslejt 9479
[Kalmbach] p. 65	Proposition 1	chocin 9506  chocint 9547  chsupclt 9437  chsupval2t 9431  dfchsup2 9427  h0elch 9278  helch 9267  hsupval2t 9429  ocin 9299  ococss 9296  shococss 9297
[Kalmbach] p. 65	Definition of subspace sum	shsumvalt 9406
[Kalmbach] p. 66	Remark	df-pj 9366  pjssm 9757  pjssmt 10218
[Kalmbach] p. 67	Lemma 3	osum 9717  osumt 9719
[Kalmbach] p. 67	Lemma 4	pjc 10252
[Kalmbach] p. 103	Exercise 6	atmd2 10449
[Kalmbach] p. 103	Exercise 12	mdsl0 10359
[Kalmbach] p. 140	Remark	hatomic 10408  hatomict 10409  hatomistic 10411
[Kalmbach] p. 140	Proposition 1(i)	atexcht 10430
[Kalmbach] p. 140	Proposition 1(ii)	chcv1t 10404
[Kalmbach] p. 140	Proposition 1(iii)	cvexch 10418  cvexcht 10423
[Kalmbach] p. 149	Remark 2	chrelat 10413
[Kalmbach] p. 153	Exercise 5	spansncv 9728  spansncvt 9729
[Kalmbach] p. 153	Proposition 1(ii)	spansncv2t 10344
[Kalmbach] p. 266	Definition	df-st 10263
[Kalmbach] p. 353	Definition of operator	df-hosum 9637
[Kalmbach2] p. 8	Definition of adjoint	df-adjh 9906
[Kreyszig] p. 3	Property M1	metcl 7698
[Kreyszig] p. 4	Property M2	meteq0 7699
[Kreyszig] p. 8	Definition 1.1-8	dscmet 7804
[Kreyszig] p. 12	Equation 5	conjmult 5704  muleqaddt 5620
[Kreyszig] p. 18	Definition 1.3-2	opnfval 7745
[Kreyszig] p. 19	Remark	opntop 7758
[Kreyszig] p. 19	Theorem T1	opn0 7761  opnm 7748
[