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 9514
[AkhiezerGlazman] p. 39	Definition of linear operator norm	df-nmo 8415
[AkhiezerGlazman] p. 64	Theorem	hmopidmch 10087  hmopidmcht 10089
[AkhiezerGlazman] p. 65	Theorem 1	pjcmmul1 10138  pjcmmul2 10139
[AkhiezerGlazman] p. 72	Theorem	cnvunopt 9850  unoplint 9852
[AkhiezerGlazman] p. 72	Equation 2	unopadj2t 9870  unopadjt 9851
[AkhiezerGlazman] p. 73	Theorem	elunop2t 9946  lnopuni 9945
[AkhiezerGlazman] p. 80	Proposition 1	adjlnopt 10027
[Apostol] p. 18	Theorem I.1	addcan 5375  addcant 5376
[Apostol] p. 18	Theorem I.2	negeu 5379
[Apostol] p. 18	Theorem I.3	negsub 5405  negsubt 5406
[Apostol] p. 18	Theorem I.4	negneg 5414  negnegt 5417
[Apostol] p. 18	Theorem I.5	subdi 5453  subdir 5454  subdirt 5452  subdit 5451
[Apostol] p. 18	Theorem I.6	mul01 5455  mul01t 5467  mul02 5456  mul02t 5468
[Apostol] p. 18	Theorem I.7	mulcan 5710  mulcanOLD 5711  mulcant 5714  mulcant2 5712  mulcant2OLD 5713  mulcantOLD 5715
[Apostol] p. 18	Theorem I.8	receu 5725
[Apostol] p. 18	Theorem I.9	divrec 5756  divrect 5758  divrecz 5757
[Apostol] p. 18	Theorem I.10	recrec 5782  recrect 5790
[Apostol] p. 18	Theorem I.11	mul0or 5718  mul0ort 5720
[Apostol] p. 18	Theorem I.12	mul2neg 5471  mul2negt 5478  mulneg1 5469  mulneg1t 5475
[Apostol] p. 18	Theorem I.13	divadddiv 5802  divadddivt 5798
[Apostol] p. 18	Theorem I.14	divmuldiv 5800  divmuldivt 5794
[Apostol] p. 18	Theorem I.15	divdivdiv 5803  divdivdivt 5799
[Apostol] p. 20	Axiom 7	rpaddclt 6304  rpmulclt 6305
[Apostol] p. 20	Axiom 9	0nrp 6307
[Apostol] p. 20	Theorem I.17	lttr 5609
[Apostol] p. 20	Theorem I.18	ltadd1 5615
[Apostol] p. 20	Theorem I.19	ltmul1 5836  ltmul1i 5835  ltmul1t 5844  ltmul2 5848  ltmul2t 5845  ltmullem 5664
[Apostol] p. 20	Theorem I.20	msqgt0 5637  msqgt0t 5639
[Apostol] p. 20	Theorem I.21	lt01 5704
[Apostol] p. 20	Theorem I.23	lt0neg1t 5692  ltneg 5627  ltnegt 5679
[Apostol] p. 20	Theorem I.25	lt2add 5620  lt2addt 5667
[Apostol] p. 20	Definition of positive numbers	df-rp 6295
[Apostol] p. 21	Exercise 4	recgt0 5876  recgt0i 5828  recgt0t 5875
[Apostol] p. 22	Definition of integers	df-z 6150
[Apostol] p. 22	Definition of positive integers	dfnn2 5950
[Apostol] p. 22	Definition of rationals	df-q 6270
[Apostol] p. 24	Theorem I.26	supeu 4597  supeui 4602
[Apostol] p. 26	Theorem I.28	nnunb 6084
[Apostol] p. 26	Theorem I.29	arch 6085
[Apostol] p. 28	Exercise 2	btwnz 6230
[Apostol] p. 28	Exercise 3	nnreclt 6086
[Apostol] p. 28	Exercise 4	rebtwnz 6237
[Apostol] p. 28	Exercise 5	zbtwnre 6236
[Apostol] p. 28	Exercise 6	qbtwnre 6292
[Apostol] p. 28	Exercise 10(a)	zneo 6215
[Apostol] p. 29	Theorem I.35	sqrth 6714
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nn 5940
[Apostol] p. 34	Theorem I.37 (well-ordering principle)	nnwo 6473
[Apostol] p. 361	Remark	crmul 6755  crrecz 6756
[Apostol] p. 363	Remark	absgt0 6857
[Apostol] p. 363	Example	abssub 6860
[BellMachover] p. 36	Lemma 10.3	id1 60
[BellMachover] p. 97	Definition 10.1	df-eu 1385
[BellMachover] p. 460	Notation	df-mo 1386
[BellMachover] p. 460	Definition	mo3 1404
[BellMachover] p. 461	Axiom Ext	ax-ext 1463
[BellMachover] p. 462	Theorem 1.1	bm1.1 1466
[BellMachover] p. 463	Axiom Rep	axrep5 2706
[BellMachover] p. 463	Scheme Sep	axsep 2710
[BellMachover] p. 463	Theorem 1.3ii	bm1.3ii 2714
[BellMachover] p. 466	Axiom Pow	axpow2 2753
[BellMachover] p. 466	Axiom Union	axun2 2877
[BellMachover] p. 468	Definition	df-ord 2960
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 2975
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 2981
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 2977
[BellMachover] p. 471	Definition of N	df-om 3141
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 3028
[BellMachover] p. 471	Definition of Lim	df-lim 2962
[BellMachover] p. 472	Axiom Inf	zfinf 4647
[BellMachover] p. 473	Theorem 2.8	limom 3155
[BellMachover] p. 477	Equation 3.1	df-r1 4665
[BellMachover] p. 478	Definition	rankval2 4692
[BellMachover] p. 478	Theorem 3.3(i)	r1ord3 4679
[BellMachover] p. 480	Axiom Reg	zfreg2 4616
[BellMachover] p. 488	Axiom AC	ac5 4774  aceq4 4756
[BellMachover] p. 490	Definition of aleph	alephval3 4926
[BeltramettiCassinelli] p. 107	Remark 10.3.5	atom1d 10289
[BeltramettiCassinelli] p. 166	Theorem 14.8.4	irred 10330  irredt 10331
[BeltramettiCassinelli1] p. 400	Proposition P8(ii)	atoml2 10319
[Beran] p. 3	Definition of join	dfchj3 9333  sshjval3t 9334
[Beran] p. 39	Theorem 2.3(i)	cmcm2 9544  cmcm2i 9549  cmcm2t 9567
[Beran] p. 40	Theorem 2.3(iii)	lecm 9553  lecmi 9554  lecmt 9568
[Beran] p. 45	Theorem 3.4	cmcmlem 9542
[Beran] p. 49	Theorem 4.2	cm2jt 9571
[Beran] p. 95	Definition	df-sh 9084  sh 9086
[Beran] p. 95	Lemma 3.1(S5)	his5t 8961
[Beran] p. 95	Lemma 3.1(S6)	his6t 8973
[Beran] p. 95	Lemma 3.1(S7)	his7t 8964
[Beran] p. 95	Lemma 3.2(S8)	ho01 9762
[Beran] p. 95	Lemma 3.2(S9)	hoeq1t 9764
[Beran] p. 95	Lemma 3.2(S10)	ho02 9763
[Beran] p. 95	Lemma 3.2(S11)	hoeq2t 9765
[Beran] p. 95	Postulate (S1)	ax-his1 8957  his1 8974
[Beran] p. 95	Postulate (S2)	ax-his2 8958
[Beran] p. 95	Postulate (S3)	ax-his3 8959
[Beran] p. 95	Postulate (S4)	ax-his4 8960
[Beran] p. 96	Definition of norm	df-hnorm 8845  dfhnorm2 8996  normvalt 8998
[Beran] p. 96	Definition for Cauchy sequence	hcau 9059
[Beran] p. 96	Definition of Cauchy sequence	df-hcau 8850
[Beran] p. 96	Definition of complete subspace	chsscm 9120
[Beran] p. 96	Definition of converge	df-hlim 8849  hlim 9064
[Beran] p. 97	Theorem 3.3(i)	norm-i 9008  norm-it 9004
[Beran] p. 97	Theorem 3.3(ii)	norm-ii 9012  norm-iit 9013  normlem0 8983  normlem1 8984  normlem2 8985  normlem3 8986  normlem4 8987  normlem5 8988  normlem6 8989  normlem7 8990  normlem7tALT 8993
[Beran] p. 97	Theorem 3.3(iii)	norm-iii 9014  norm-iiit 9015
[Beran] p. 98	Remark 3.4	bcsALT 9054  bcsHIL 9055  bcst 9056
[Beran] p. 98	Remark 3.4(B)	normlem9at 8995  normpar 9029  normpart 9030
[Beran] p. 98	Remark 3.4(C)	normpyct 9021  normpyth 9017  normpytht 9020
[Beran] p. 99	Remark	lnfn0 9979  lnfn0t 9984  lnop0 9902  lnop0t 9898
[Beran] p. 99	Theorem 3.5(i)	nmcfnex 9994  nmcfnext 9996  nmcopex 9965  nmcopexlem1 9959  nmcopext 9967
[Beran] p. 99	Theorem 3.5(ii)	nmcfnlb 9995  nmcfnlbt 9997  nmcoplb 9966  nmcoplbt 9968
[Beran] p. 99	Theorem 3.5(iii)	lnfncon 9998  lnfncont 9999  lnopcon 9971  lnopcont 9972
[Beran] p. 99	Definition of operator	df-hosum 9514
[Beran] p. 100	Lemma 3.6	normpar2 9031  projlem1 9194  projlem10 9203  projlem11 9204  projlem12 9205  projlem13 9206  projlem14 9207  projlem15 9208  projlem16 9209  projlem17 9210  projlem17 9210  projlem2 9195  projlem21 9214  projlem22 9215  projlem3 9196  projlem5 9198  projlem8 9201  projlem8 9201  projlem9 9202
[Beran] p. 101	Lemma 3.6	norm3adif 9023  norm3adift 9028  norm3dif 9022  norm3dift 9025  projlem 9225  projlem18 9211  projlem19 9212  projlem20 9213  projlem23 9216  projlem24 9217  projlem25 9218  projlem26 9219  projlem27 9220  projlem28 9221  projlem29 9222  projlem30 9223  projlem31 9224  projlem4 9197  projlem6 9199  projlem7 9200  projlemHIL 9226
[Beran] p. 102	Theorem 3.7(i)	chocuni 9180  pjpjth 9267  pjpjtht 9266  pjth 9241  pjtht 9242
[Beran] p. 102	Theorem 3.7(ii)	ococ 9255  ococt 9256
[Beran] p. 103	Remark 3.8	nlelch 10002
[Beran] p. 104	Theorem 3.9	riesz3 10003  riesz4 10004  riesz4t 10005
[Beran] p. 104	Theorem 3.10	cnlnadj 10017  cnlnadjeu 10018  cnlnadjeut 10019  cnlnadjlem1 10008  cnlnadjt 10020  nmopadjle 10029
[Beran] p. 106	Theorem 3.11(i)	adjeq0 10032
[Beran] p. 106	Theorem 3.11(v)	nmopadj 10031
[Beran] p. 106	Theorem 3.11(ii)	adjmult 10033
[Beran] p. 106	Theorem 3.11(iv)	adjadjt 9868
[Beran] p. 106	Theorem 3.11(vi)	nmopcoadj 10042  nmopcoadj2 10043
[Beran] p. 106	Theorem 3.11(iii)	adjaddt 10034
[Beran] p. 106	Theorem 3.11(vii)	nmopcoadj0 10044
[Beran] p. 106	Theorem 3.11(viii)	adjco 10041  pjadj2co 10141  pjadjco 10097
[Beran] p. 107	Definition	closedsub 9101  df-ch 9100
[Beran] p. 107	Remark 3.12	chocclt 9192  chsscm 9120  occl 9189  occllem1 9181  occllem2 9182  occllem3 9183  occllem4 9184  occllem5 9185  occllem6 9186  occllem7 9187  occllem8 9188  occlt 9190  ocsh 9164  shocclt 9191  shocsh 9165
[Beran] p. 107	Remark 3.12(B)	ococint 9305
[Beran] p. 107	Remark 3.12(C)	ch2 9122  chcmh 9121
[Beran] p. 108	Theorem 3.13	chintclt 9304
[Beran] p. 109	Property (i)	pjadj 9626  pjadj2t 10123  pjadj3t 10124  pjadjt 9638
[Beran] p. 109	Property (ii)	pjidm 9625  pjidmco 10113  pjidmcot 10117
[Beran] p. 110	Definition of projector ordering	pjord 10109
[Beran] p. 111	Remark	ho0valt 9684  pjch1t 9623
[Beran] p. 111	Definition	df-hfmul 9518  df-hfsum 9517  df-hodif 9516  df-homul 9515  df-hosum 9514
[Beran] p. 111	Lemma 4.4(i)	pjot 9624
[Beran] p. 111	Lemma 4.4(ii)	pjch 9273  pjcht 9647
[Beran] p. 111	Lemma 4.4(iii)	pjoc2 9279  pjoc2t 9280
[Beran] p. 112	Theorem 4.5(i)->(ii)	pjss2 9633
[Beran] p. 112	Theorem 4.5(i)->(iv)	pjssm 9634  pjssmt 10101
[Beran] p. 112	Theorem 4.5(i)<->(ii)	pjss2co 10100
[Beran] p. 112	Theorem 4.5(i)<->(iii)	pjss1co 10099
[Beran] p. 112	Theorem 4.5(i)<->(vi)	pjnormss 10104
[Beran] p. 112	Theorem 4.5(iv)->(v)	pjssge0 9635  pjssge0t 10102
[Beran] p. 112	Theorem 4.5(v)<->(vi)	pjdifnorm 9636  pjdifnormt 10103
[ChoquetDD] p. 2	Definition of mapping	df-mpt 4082
[Cohen] p. 301	Remark	relogoprlem 8777
[Cohen] p. 301	Property 2	relogmult 8778
[Cohen] p. 301	Property 3	relogdivt 8779
[Cohen] p. 301	Property 4	relogexpt 8782
[Cohen] p. 301	Property 1a	log1 8774
[Cohen] p. 301	Property 1b	loge 8775
[Diestel] p. 2	Definition	df-sgra 10774
[Diestel] p. 28	Definition	df-pgra 10771
[Diestel] p. 28	Definition of hypergraph	ishgrag 10762
[Eisenberg] p. 67	Definition 5.3	df-dif 2055
[Eisenberg] p. 82	Definition 6.3	dfom3 4651
[Eisenberg] p. 125	Definition 8.21	df-map 4333
[Eisenberg] p. 216	Example 13.2(4)	omenps 4658
[Eisenberg] p. 310	Theorem 19.8	cardprc 4884
[Eisenberg] p. 310	Corollary 19.7(2)	cardsdom 4859
[Enderton] p. 18	Axiom of Empty Set	axnul 2717
[Enderton] p. 19	Definition	df-tp 2422
[Enderton] p. 26	Exercise 5	unissb 2535
[Enderton] p. 26	Exercise 10	pwel 2768
[Enderton] p. 28	Exercise 7(b)	pwun 2838
[Enderton] p. 30	Theorem "Distributive laws"	iinun2 2617  iunin2 2616
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2 2619  iundif2 2618
[Enderton] p. 32	Exercise 20	unineq 2261
[Enderton] p. 33	Exercise 23	iinuni 2623
[Enderton] p. 33	Exercise 25	iununi 2624
[Enderton] p. 33	Exercise 24(a)	iinpw 2625
[Enderton] p. 33	Exercise 24(b)	iunpw 2923  iunpwss 2626
[Enderton] p. 36	Definition	opthwiener 2816
[Enderton] p. 38	Exercise 6(a)	unipw 2765
[Enderton] p. 38	Exercise 6(b)	pwuni 2766
[Enderton] p. 41	Lemma 3D	opeluu 2888  rnex 3370  rnexg 3368
[Enderton] p. 41	Exercise 8	dmuni 3328  rnuni 3468
[Enderton] p. 42	Definition of a function	dffun6 3548  dffun7 3549
[Enderton] p. 43	Definition of function value	funfv2 3780
[Enderton] p. 43	Definition of single-rooted	funcnv 3566
[Enderton] p. 44	Definition (d)	dfima2 3414  dfima3 3415
[Enderton] p. 47	Theorem 3H	fvco2 3784
[Enderton] p. 49	Axiom of Choice (first form)	ac7 4770  ac7g 4771  aceq3 4755  aceq4 4756  aceq5 4762  aceq6a 4763  aceq6b 4764  aceq7 4765  aceqkm 4803
[Enderton] p. 50	Theorem 3K(a)	imaiun 3873
[Enderton] p. 52	Definition	df-map 4333
[Enderton] p. 53	Exercise 21	coass 3521
[Enderton] p. 53	Exercise 27	dmco2 3513
[Enderton] p. 53	Exercise 14(a)	funin 3575
[Enderton] p. 53	Exercise 22(a)	imass2 3442
[Enderton] p. 54	Remark	ixpf 4365  ixpssmap 4372
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 4357
[Enderton] p. 55	Axiom of Choice (second form)	ac9s 4786
[Enderton] p. 56	Theorem 3M	erref 4284
[Enderton] p. 57	Lemma 3N	erthi 4290
[Enderton] p. 57	Definition	df-ec 4272
[Enderton] p. 58	Definition	df-qs 4275
[Enderton] p. 60	Theorem 3Q	th3q 4326  th3qcor 4325  th3qlem1 4323  th3qlem2 4324
[Enderton] p. 61	Exercise 35	df-ec 4272
[Enderton] p. 65	Exercise 56(a)	dmun 3326
[Enderton] p. 68	Definition of successor	df-suc 2963
[Enderton] p. 71	Definition	df-tr 2689  dftr4 2693
[Enderton] p. 72	Theorem 4E	unisuc 3055
[Enderton] p. 73	Exercise 6	unisuc 3055
[Enderton] p. 79	Theorem 4I(A1)	nna0 4232
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 4234
[Enderton] p. 79	Definition of operation value	df-opr 3974
[Enderton] p. 80	Theorem 4J(A1)	nnm0 4233
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 4235
[Enderton] p. 81	Theorem 4K(1)	nnaass 4246
[Enderton] p. 81	Theorem 4K(2)	nna0r 4236  nnacom 4242
[Enderton] p. 81	Theorem 4K(3)	nndi 4247
[Enderton] p. 81	Theorem 4K(4)	nnmass 4248
[Enderton] p. 81	Theorem 4K(5)	nnmcom 4250
[Enderton] p. 82	Exercise 16	nnm0r 4237  nnmsucr 4249
[Enderton] p. 88	Exercise 23	nnaordex 4258
[Enderton] p. 129	Definition	bren 4386  df-en 4377
[Enderton] p. 132	Theorem 6B(b)	canth 3916
[Enderton] p. 133	Exercise 1	xpomen 7515
[Enderton] p. 133	Exercise 2	qnnen 7518
[Enderton] p. 134	Theorem (Pigeonhole Principle)	php 4523
[Enderton] p. 135	Corollary 6C	php3 4525  php3OLD 4526
[Enderton] p. 136	Corollary 6E	nneneq 4522
[Enderton] p. 136	Corollary 6D(a)	pssinf 4539  pssinfOLD 4540
[Enderton] p. 136	Corollary 6D(b)	ominf 4541  ominfOLD 4542
[Enderton] p. 137	Lemma 6F	pssnn 4549
[Enderton] p. 138	Corollary 6G	ssfi 4552  ssfiOLD 4553
[Enderton] p. 139	Theorem 6H(c)	mapen 4501
[Enderton] p. 142	Theorem 6I(3)	xpcdaen 4955
[Enderton] p. 142	Theorem 6I(4)	mapcdaen 4956
[Enderton] p. 143	Theorem 6J	cda0en 4949  cda1en 4950
[Enderton] p. 144	Exercise 13	unifi 4574  unifi2 4575  unifi2OLD 4577  unifiOLD 4576
[Enderton] p. 144	Corollary 6K	undif2 2348  unfi 4568  unfi2 4570  unfi2OLD 4571  unfiOLD 4569
[Enderton] p. 145	Figure 38	ffoss 3720
[Enderton] p. 145	Definition	df-dom 4378
[Enderton] p. 146	Example 1	domen 4388  domeng 4389
[Enderton] p. 146	Example 3	nndomo 4531  omsdomnn 4543
[Enderton] p. 149	Theorem 6L(a)	cdadom2 4958
[Enderton] p. 149	Theorem 6L(c)	mapdom1 4502  xpdom1 4453  xpdom1g 4454
[Enderton] p. 149	Theorem 6L(d)	mapdom2 4504
[Enderton] p. 151	Theorem 6M	zorn 4819
[Enderton] p. 151	Theorem 6M(4)	ac8 4785  aceq5 4762
[Enderton] p. 159	Theorem 6Q	unictb 7591
[Enderton] p. 162	Lemma 6R	infxpidm 7579
[Enderton] p. 164	Example	infdif 7583
[Enderton] p. 165	Exercise 34	infmap1 7588
[Enderton] p. 168	Definition	df-po 2849
[Enderton] p. 192	Theorem 7M(a)	onel 3107
[Enderton] p. 192	Theorem 7M(b)	ontr1 3012
[Enderton] p. 192	Theorem 7M(c)	onirr 3106
[Enderton] p. 193	Corollary 7N(b)	0elon 3031
[Enderton] p. 193	Corollary 7N(c)	onsuc 3114
[Enderton] p. 193	Corollary 7N(d)	ssonuni 3004
[Enderton] p. 194	Remark	onprc 2998
[Enderton] p. 194	Exercise 16	suc11 3102
[Enderton] p. 197	Definition	df-card 4838
[Enderton] p. 197	Theorem 7P	carden 4853
[Enderton] p. 200	Exercise 25	tfis 3136
[Enderton] p. 202	Lemma 7T	r1tr 4676
[Enderton] p. 202	Definition	df-r1 4665
[Enderton] p. 202	Theorem 7Q	r1val1 4680
[Enderton] p. 204	Theorem 7V(b)	rankval4 4724
[Enderton] p. 206	Theorem 7X(b)	en2lp 4623
[Enderton] p. 207	Exercise 30	rankpr 4714  rankpw 4706  rankuniss 4723
[Enderton] p. 207	Exercise 34	opthreg 4625
[Enderton] p. 208	Exercise 35	suc11reg 4626
[Enderton] p. 212	Definition of aleph	alephval3 4926
[Enderton] p. 213	Theorem 8A(a)	alephord2 4899
[Enderton] p. 213	Theorem 8A(b)	cardalephex 4909
[Enderton] p. 222	Definition of kard	karden 4748  kardex 4747
[Enderton] p. 240	Exercise 25	oarec 4205
[Enderton] p. 257	Definition of cofinality	cflim 4933
[FreydScedrov] p. 283	Axiom of Infinity	ax-inf 4643  inf1 4628  inf2 4629
[Gleason] p. 117	Proposition 9-2.1	df-enq 5061  enqer 5070
[Gleason] p. 117	Proposition 9-2.2	df-1q 5067  df-nq 5062
[Gleason] p. 117	Proposition 9-2.3	df-plpq 5059  df-plq 5063
[Gleason] p. 119	Proposition 9-2.4	caoprmo 4079  df-mpq 5060  df-mq 5064
[Gleason] p. 119	Proposition 9-2.5	df-rq 5065
[Gleason] p. 119	Proposition 9-2.6	ltexpq 5104  ltexpq2 5105
[Gleason] p. 120	Proposition 9-2.6(i)	halfpq 5106  ltbtwnpq 5108
[Gleason] p. 120	Proposition 9-2.6(ii)	ltapq 5100
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmpq 5101
[Gleason] p. 120	Proposition 9-2.6(iv)	ltrpq 5109
[Gleason] p. 121	Definition 9-3.1	df-np 5110
[Gleason] p. 121	Definition 9-3.1 (ii)	prcdpq 5121
[Gleason] p. 121	Definition 9-3.1(iii)	prnmax 5123
[Gleason] p. 122	Definition	df-1p 5111
[Gleason] p. 122	Remark (1)	prub 5122
[Gleason] p. 122	Lemma 9-3.4	prlem934 5163  prlem934a 5161  prlem934b 5162
[Gleason] p. 122	Proposition 9-3.2	df-ltp 5114
[Gleason] p. 122	Proposition 9-3.3	ltsopr 5160  psslinpr 5159  supexpr 5187  suplem1pr 5185  suplem2pr 5186
[Gleason] p. 123	Proposition 9-3.5	addclpr 5144  addclprlem1 5142  addclprlem2 5143  df-plp 5112
[Gleason] p. 123	Proposition 9-3.5(i)	addasspr 5148
[Gleason] p. 123	Proposition 9-3.5(ii)	addcompr 5147
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 5164
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 5173  ltexprlem1 5166  ltexprlem2 5167  ltexprlem3 5168  ltexprlem4 5169  ltexprlem5 5170  ltexprlem6 5171  ltexprlem7 5172
[Gleason] p. 123	Proposition 9-3.5(v)	ltapr 5175  ltaprlem 5174
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanpr 5176
[Gleason] p. 124	Lemma 9-3.6	prlem936 5179  prlem936a 5177  prlem936b 5178
[Gleason] p. 124	Proposition 9-3.7	df-mp 5113  mulclpr 5146  mulclprlem 5145  reclem1pr 5180  reclem2pr 5181
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 5157
[Gleason] p. 124	Proposition 9-3.7(i)	mulasspr 5150
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcompr 5149
[Gleason] p. 124	Proposition 9-3.7(iii)	distrpr 5156
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 5184  reclem3pr 5182  reclem4pr 5183
[Gleason] p. 126	Proposition 9-4.1	df-enr 5190  df-mpr 5189  df-plpr 5188  enrer 5200
[Gleason] p. 126	Proposition 9-4.2	df-0r 5195  df-1r 5196  df-nr 5191
[Gleason] p. 126	Proposition 9-4.3	df-mr 5193  df-plr 5192  negexsr 5235  recexsr 5240  recexsrlem 5236
[Gleason] p. 127	Proposition 9-4.4	df-ltr 5194
[Gleason] p. 130	Proposition 10-1.3	creui 6758  creur 6757  cru 6752  crut 6753
[Gleason] p. 130	Definition 10-1.1(v)	axcnre 5310
[Gleason] p. 132	Definition 10-3.1	crim 6787  crimt 6785  crre 6786  crret 6784
[Gleason] p. 132	Definition 10-3.2	cjvalt 6778
[Gleason] p. 133	Definition 10.36	absval2 6855  absval2t 6866
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 6802  cjaddt 6826
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 6803  cjmult 6827
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 6792  cjcjt 6825
[Gleason] p. 133	Proposition 10-3.4(f)	cjreb 6795  cjrebt 6814  cjret 6824  rereb 6794  rerebt 6791  reret 6813
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 6812  addcjt 6829
[Gleason] p. 133	Proposition 10-3.7(a)	absvalt 6777
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 6859  abscjt 6848
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 6856  abs00t 6867
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 6904  releabst 6900
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 6861  absmult 6872
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 6864  sqabsaddt 6862
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 6905  abstrit 6912
[Gleason] p. 134	Definition 10-4.1	df-exp 6584  exp0t 6586  expp1t 6589
[Gleason] p. 135	Proposition 10-4.2(a)	expaddt 6611
[Gleason] p. 135	Proposition 10-4.2(b)	expmult 6612
[Gleason] p. 135	Proposition 10-4.2(c)	mulexpt 6609
[Gleason] p. 140	Exercise 1	znnen 7517
[Gleason] p. 141	Definition 11-2.1	fzvalt 6484
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 7131
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 7144
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 7142
[Gleason] p. 171	Corollary 12-2.2	climmulc 7147  climmulc2 7143
[Gleason] p. 172	Corollary 12-2.5	climfnrcl 7125  climrecl 7124
[Gleason] p. 172	Proposition 12-2.4(c)	climcj 7164
[Gleason] p. 173	Definition 12-3.1	df-ltxr 5514  df-xr 5513  ltxrt 5519
[Gleason] p. 175	Definition 12-4.1	df-limsup 6543  limsupvalt 6544
[Gleason] p. 180	Theorem 12-5.1	climsup 7169
[Gleason] p. 180	Theorem 12-5.3	caucvg3 7181  caucvg3a 7178  caucvg3t 7182  climcau 7170
[Gleason] p. 181	Remark	cau2 6927
[Gleason] p. 182	Exercise 3	cvgcmp 7198
[Gleason] p. 182	Exercise 4	cvgrat 7269
[Gleason] p. 195	Theorem 13-2.12	abs1m 6918
[Gleason] p. 217	Lemma 13-4.1	btwnzge0t 6260
[Gleason] p. 223	Definition 14-1.1	df-met 7803
[Gleason] p. 223	Definition 14-1.1(a)	met0 7825
[Gleason] p. 223	Definition 14-1.1(b)	metgt0 7830
[Gleason] p. 223	Definition 14-1.1(c)	metsym 7826
[Gleason] p. 223	Definition 14-1.1(d)	mettri 7827
[Gleason] p. 225	Definition 14-1.5	metxp 7844  metxpcl 7842  metxpdval 7839  metxpfval 7841  metxptval 7840
[Gleason] p. 230	Proposition 14-2.6	xplm 7985  xplmi 7983  xplmi2 7984
[Gleason] p. 240	Theorem 14-4.3	metcnp4 7980
[Gleason] p. 240	Proposition 14-4.2	metcnp3 7906
[Gleason] p. 243	Proposition 14-4.16	addcn 7996  mulcn 7998  subcn 7997
[Gleason] p. 295	Remark	bcval4t 6975
[Gleason] p. 295	Equation 2	bcpasc 6983  bcpasc2 6981  bcpasc2t 6982  bcpasct 6984
[Gleason] p. 295	Definition of binomial coefficient	bcvalt 6972  df-bc 6971
[Gleason] p. 296	Remark	bcn0t 6977  bcnnt 6978
[Gleason] p. 296	Theorem 15-2.8	binom 7086
[Gleason] p. 308	Equation 2	ef0 7349
[Gleason] p. 308	Equation 3	efcj 7350  efcjt 7351
[Gleason] p. 309	Corollary 15-4.3	efne0t 7383
[Gleason] p. 309	Corollary 15-4.4	efexpt 7386
[Gleason] p. 310	Equation 14	sinadd 7465  sinaddt 7467
[Gleason] p. 310	Equation 15	cosadd 7466  cosaddt 7468
[Gleason] p. 311	Equation 17	sincossqt 7475
[Gleason] p. 311	Equation 18	cosbndt 7481  sinbndt 7480
[Gleason] p. 311	Lemma 15-4.7	sqeqor 6662  sqeqort 6664
[Gleason] p. 311	Definition of pi	df-pi 7316
[Godowski] p. 730	Equation SF	goeq 10209
[GodowskiGreechie] p. 249	Equation IV	3oa 9621
[Goldberg] p. 10	Definition of operator	df-hosum 9514
[Halmos] p. 31	Theorem 17.3	riesz1t 10006  riesz2t 10007
[Halmos] p. 35	Definition of operator	df-hosum 9514
[Halmos] p. 41	Definition of Hermitian	hmopadj2t 9873
[Halmos] p. 42	Definition of projector ordering	pjord 10109
[Halmos] p. 43	Theorem 26.1	elpjhmopt 10121  elpjidmt 10120  pjnmop 10083
[Halmos] p. 44	Remark	pjinorm 9629  pjinormt 9640
[Halmos] p. 44	Theorem 26.2	elpjcht 10125  pjrn 9655  pjrnt 9660  pjvect 9649
[Halmos] p. 44	Theorem 26.3	pjnorm2t 9680
[Halmos] p. 44	Theorem 26.4	hmopidmpj 10088  hmopidmpjt 10090
[Halmos] p. 45	Theorem 27.1	pjinvar 10128
[Halmos] p. 45	Theorem 27.3	pjoc 10116  pjocvect 9650
[Halmos] p. 45	Theorem 27.4	pjorthco 10105
[Halmos] p. 48	Theorem 29.2	pjsspos 10108
[Halmos] p. 48	Theorem 29.3	pjssdif1 10111  pjssdif2 10110
[Halmos] p. 50	Definition of spectrum	df-spec 9789
[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 966
[Herstein] p. 54	Exercise 28	df-grp 8047
[Herstein] p. 55	Lemma 2.2.1(a)	grpideu 8063
[Herstein] p. 55	Lemma 2.2.1(b)	grpinveu 8073
[Herstein] p. 55	Lemma 2.2.1(c)	grp2inv 8087
[Herstein] p. 55	Lemma 2.2.1(d)	grpinvop 8089
[Herstein] p. 57	Exercise 1	isgrp2i 8085
[Holland] p. 1519	Theorem 2	sumdmd 10356
[Holland] p. 1520	Lemma 5	cdj1 10369  cdj3 10377  cdj3lem1 10370  cdjreu 10368
[Holland] p. 1524	Lemma 7	mddmdin0 10367
[Hughes] p. 14	Definition of operator	df-hosum 9514
[Hughes] p. 44	Equation 1.21b	ax-his3 8959
[Hughes] p. 47	Definition of projection operator	dfpjopt 10119
[Hughes] p. 49	Equation 1.30	eighmret 9895  eigre 9768  eigret 9769
[Hughes] p. 49	Equation 1.31	eighmortht 9896  eigorth 9771  eigortht 9772
[Hughes] p. 137	Remark (ii)	eigpos 9770
[Jech] p. 4	Definition of class	cv 958  cvjust 1475
[Jech] p. 42	Lemma 6.1	alephexp1 7599
[Jech] p. 42	Equation 6.1	alephadd 7597  alephmul 7598
[Jech] p. 43	Lemma 6.2	infmap2 7596
[Jech] p. 71	Lemma 9.3	jech9.3 4688
[Jech] p. 72	Equation 9.3	scott0 4739  scottex 4738
[Jech] p. 72	Exercise 9.1	rankval4 4724
[Jech] p. 72	Scheme "Collection Principle"	cp 4744
[Jech] p. 78	Definition implied by the footnote	opthprc 3230
[KalishMontague] p. 81	Axiom B7' in footnote 1	ax-9 968
[Kalmbach] p. 14	Definition of lattice	chabs1 9449  chabs1t 9447  chabs2 9450  chabs2t 9448  chjass 9417  chjasst 9464
[Kalmbach] p. 15	Definition of atom	df-at 10274  elat 10275
[Kalmbach] p. 15	Definition of covers	cvbr2t 10219
[Kalmbach] p. 20	Definition of commutes	cmbr 9541  cmbrt 9535  df-cm 9534
[Kalmbach] p. 22	Remark	pjoml5 9539  pjoml5t 9564
[Kalmbach] p. 22	Definition	pjoml2 9536  pjoml2t 9562
[Kalmbach] p. 22	Theorem 2(v)	cmcm 9543  cmcmi 9548  cmcmt 9565
[Kalmbach] p. 22	Theorem 2(ii)	omls 9254  pjoml 9276  pjomlt 9277
[Kalmbach] p. 23	Remark	cmbr2 9547  cmcm3 9545  cmcm3i 9550  cmcm3t 9566  cmcm4 9546
[Kalmbach] p. 23	Lemma 3	cmbr3 9551  cmbr3t 9559
[Kalmbach] p. 25	Theorem 5	fh1 9572  fh1t 9569  fh2 9573  fh2t 9570
[Kalmbach] p. 65	Remark	chjatom 10293  chslej 9389  chslejt 9429  shslej 9346  shslejt 9358
[Kalmbach] p. 65	Proposition 1	chocin 9385  chocint 9426  chsupclt 9316  chsupval2t 9310  dfchsup2 9306  h0elch 9135  helch 9124  hsupval2t 9308  ocin 9177  ococss 9174  shococss 9175
[Kalmbach] p. 65	Definition of subspace sum	shsumvalt 9285
[Kalmbach] p. 66	Remark	df-pj 9245  pjssm 9634  pjssmt 10101
[Kalmbach] p. 67	Lemma 3	osum 9594  osumt 9596
[Kalmbach] p. 67	Lemma 4	pjc 10137
[Kalmbach] p. 103	Exercise 6	atmd2 10336
[Kalmbach] p. 103	Exercise 12	mdsl0 10246
[Kalmbach] p. 140	Remark	hatomic 10295  hatomict 10296  hatomistic 10298
[Kalmbach] p. 140	Proposition 1(i)	atexcht 10317
[Kalmbach] p. 140	Proposition 1(ii)	chcv1t 10291
[Kalmbach] p. 140	Proposition 1(iii)	cvexch 10305  cvexcht 10310
[Kalmbach] p. 149	Remark 2	chrelat 10300
[Kalmbach] p. 153	Exercise 5	spansncv 9605  spansncvt 9606
[Kalmbach] p. 153	Proposition 1(ii)	spansncv2t 10229
[Kalmbach] p. 266	Definition	df-st 10148
[Kalmbach] p. 353	Definition of operator	df-hosum 9514
[Kalmbach2] p. 8	Definition of adjoint	df-adjh 9783
[Kreyszig] p. 3	Property M1	metcl 7821
[Kreyszig] p. 4	Property M2	meteq0 7822
[Kreyszig] p. 8	Definition 1.1-8	dscmet 7928
[Kreyszig] p. 12	Equation 5	conjmult 5811  muleqaddt 5724
[Kreyszig] p. 18	Definition 1.3-2	opnfval 7867
[Kreyszig] p. 19	Remark	opntop 7880
[Kreyszig] p. 19	Theorem T1	opn0 7883  opnm 7870
[Kreyszig] p. 19	Theorem T2	opnuni 7878
[Kreyszig] p. 19	Definition of neighborhood	metnei 7888
[Kreyszig] p. 20	Definition 1.3-3	metcnp2 7898
[Kreyszig] p. 25	Definition 1.4-1	lmbr 7938
[Kreyszig] p. 26	Lemma 1.4-2(a)	lmuni 7961
[Kreyszig] p. 28	Theorem 1.4-5	lmcau 8006
[Kreyszig] p. 28	Definition 1.4-3	iscau 7946  iscms 7956
[Kreyszig] p. 30	Theorem 1.4-7	cmsss 8007
[Kreyszig] p. 30	Theorem 1.4-6(a)	metcls 7976  metelcls 7975
[Kr