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 9478
[AkhiezerGlazman] p. 39	Definition of linear operator norm	df-nmo 8366
[AkhiezerGlazman] p. 64	Theorem	hmopidmch 10049  hmopidmcht 10051
[AkhiezerGlazman] p. 65	Theorem 1	pjcmmul1 10099  pjcmmul2 10100
[AkhiezerGlazman] p. 72	Theorem	cnvunopt 9813  unoplint 9815
[AkhiezerGlazman] p. 72	Equation 2	unopadj2t 9833  unopadjt 9814
[AkhiezerGlazman] p. 73	Theorem	elunop2t 9908  lnopuni 9907
[AkhiezerGlazman] p. 80	Proposition 1	adjlnopt 9989
[Apostol] p. 18	Theorem I.1	addcan 5342  addcant 5343
[Apostol] p. 18	Theorem I.2	negeu 5346
[Apostol] p. 18	Theorem I.3	negsub 5372  negsubt 5373
[Apostol] p. 18	Theorem I.4	negneg 5381  negnegt 5384
[Apostol] p. 18	Theorem I.5	subdi 5420  subdir 5421  subdirt 5419  subdit 5418
[Apostol] p. 18	Theorem I.6	mul01 5422  mul01t 5434  mul02 5423  mul02t 5435
[Apostol] p. 18	Theorem I.7	mulcan 5678  mulcant 5680  mulcant2 5679
[Apostol] p. 18	Theorem I.8	receu 5689
[Apostol] p. 18	Theorem I.9	divrec 5719  divrect 5721  divrecz 5720
[Apostol] p. 18	Theorem I.10	recrec 5744  recrect 5751
[Apostol] p. 18	Theorem I.11	mul0or 5682  mul0ort 5684
[Apostol] p. 18	Theorem I.12	mul2neg 5438  mul2negt 5445  mulneg1 5436  mulneg1t 5442
[Apostol] p. 18	Theorem I.13	divadddiv 5763  divadddivt 5759
[Apostol] p. 18	Theorem I.14	divmuldiv 5761  divmuldivt 5755
[Apostol] p. 18	Theorem I.15	divdivdiv 5764  divdivdivt 5760
[Apostol] p. 20	Axiom 7	rpaddclt 6246  rpmulclt 6247
[Apostol] p. 20	Axiom 9	0nrp 6249
[Apostol] p. 20	Theorem I.17	lttr 5578
[Apostol] p. 20	Theorem I.18	ltadd1 5584
[Apostol] p. 20	Theorem I.19	ltmul1 5797  ltmul1i 5796  ltmul1t 5805  ltmul2 5809  ltmul2t 5806  ltmullem 5633
[Apostol] p. 20	Theorem I.20	msqgt0 5606  msqgt0t 5608
[Apostol] p. 20	Theorem I.21	lt01 5672
[Apostol] p. 20	Theorem I.23	lt0neg1t 5660  ltneg 5596  ltnegt 5647
[Apostol] p. 20	Theorem I.25	lt2add 5589  lt2addt 5636
[Apostol] p. 20	Definition of positive numbers	df-rp 6238
[Apostol] p. 21	Exercise 4	recgt0 5835  recgt0i 5789  recgt0t 5834
[Apostol] p. 22	Definition of integers	df-z 6102
[Apostol] p. 22	Definition of positive integers	dfnn2 5903
[Apostol] p. 22	Definition of rationals	df-q 6213
[Apostol] p. 24	Theorem I.26	supeu 4569  supeui 4574
[Apostol] p. 26	Theorem I.28	nnunb 6036
[Apostol] p. 26	Theorem I.29	arch 6037
[Apostol] p. 28	Exercise 2	btwnz 6182
[Apostol] p. 28	Exercise 3	nnreclt 6038
[Apostol] p. 28	Exercise 4	rebtwnz 6189
[Apostol] p. 28	Exercise 5	zbtwnre 6188
[Apostol] p. 28	Exercise 6	qbtwnre 6235
[Apostol] p. 28	Exercise 10(a)	zneo 6166  zneoOLD 6167
[Apostol] p. 29	Theorem I.35	sqrth 6648
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nn 5893
[Apostol] p. 34	Theorem I.37 (well-ordering principle)	nnwo 6409
[Apostol] p. 361	Remark	crmul 6690  crrecz 6691
[Apostol] p. 363	Remark	absgt0 6797
[Apostol] p. 363	Example	abssub 6800
[BellMachover] p. 36	Lemma 10.3	id1 60
[BellMachover] p. 97	Definition 10.1	df-eu 1380
[BellMachover] p. 460	Notation	df-mo 1381
[BellMachover] p. 460	Definition	mo3 1399
[BellMachover] p. 461	Axiom Ext	ax-ext 1457
[BellMachover] p. 462	Theorem 1.1	bm1.1 1460
[BellMachover] p. 463	Axiom Rep	axrep5 2694
[BellMachover] p. 463	Scheme Sep	axsep 2698
[BellMachover] p. 463	Theorem 1.3ii	bm1.3ii 2702
[BellMachover] p. 466	Axiom Pow	axpow2 2740
[BellMachover] p. 466	Axiom Union	axun2 2867
[BellMachover] p. 468	Definition	df-ord 2950
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 2965
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 2971
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 2967
[BellMachover] p. 471	Definition of N	df-om 3132
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 3019
[BellMachover] p. 471	Definition of Lim	df-lim 2952
[BellMachover] p. 472	Axiom Inf	zfinf 4617
[BellMachover] p. 473	Theorem 2.8	limom 3146
[BellMachover] p. 477	Equation 3.1	df-r1 4634
[BellMachover] p. 478	Definition	rankval2 4661
[BellMachover] p. 478	Theorem 3.3(i)	r1ord3 4648
[BellMachover] p. 480	Axiom Reg	zfreg2 4588
[BellMachover] p. 488	Axiom AC	ac5 4743  aceq4 4725
[BellMachover] p. 490	Definition of aleph	alephval3 4894
[BeltramettiCassinelli] p. 107	Remark 10.3.5	atom1d 10248
[BeltramettiCassinelli] p. 166	Theorem 14.8.4	irred 10289  irredt 10290
[BeltramettiCassinelli1] p. 400	Proposition P8(ii)	atoml2 10278
[Beran] p. 3	Definition of join	dfchj3 9295  sshjval3t 9296
[Beran] p. 39	Theorem 2.3(i)	cmcm2 9508  cmcm2i 9513  cmcm2t 9531
[Beran] p. 40	Theorem 2.3(iii)	lecm 9517  lecmi 9518  lecmt 9532
[Beran] p. 45	Theorem 3.4	cmcmlem 9506
[Beran] p. 49	Theorem 4.2	cm2jt 9535
[Beran] p. 95	Definition	df-sh 9047  sh 9049
[Beran] p. 95	Lemma 3.1(S5)	his5t 8924
[Beran] p. 95	Lemma 3.1(S6)	his6t 8936
[Beran] p. 95	Lemma 3.1(S7)	his7t 8927
[Beran] p. 95	Lemma 3.2(S8)	ho01 9726
[Beran] p. 95	Lemma 3.2(S9)	hoeq1t 9728
[Beran] p. 95	Lemma 3.2(S10)	ho02 9727
[Beran] p. 95	Lemma 3.2(S11)	hoeq2t 9729
[Beran] p. 95	Postulate (S1)	ax-his1 8920  his1 8937
[Beran] p. 95	Postulate (S2)	ax-his2 8921
[Beran] p. 95	Postulate (S3)	ax-his3 8922
[Beran] p. 95	Postulate (S4)	ax-his4 8923
[Beran] p. 96	Definition of norm	df-hnorm 8808  dfhnorm2 8959  normvalt 8961
[Beran] p. 96	Definition for Cauchy sequence	hcau 9022
[Beran] p. 96	Definition of Cauchy sequence	df-hcau 8813
[Beran] p. 96	Definition of complete subspace	chsscm 9083
[Beran] p. 96	Definition of converge	df-hlim 8812  hlim 9027
[Beran] p. 97	Theorem 3.3(i)	norm-i 8971  norm-it 8967
[Beran] p. 97	Theorem 3.3(ii)	norm-ii 8975  norm-iit 8976  normlem0 8946  normlem1 8947  normlem2 8948  normlem3 8949  normlem4 8950  normlem5 8951  normlem6 8952  normlem7 8953  normlem7tALT 8956
[Beran] p. 97	Theorem 3.3(iii)	norm-iii 8977  norm-iiit 8978
[Beran] p. 98	Remark 3.4	bcsALT 9017  bcsHIL 9018  bcst 9019
[Beran] p. 98	Remark 3.4(B)	normlem9at 8958  normpar 8992  normpart 8993
[Beran] p. 98	Remark 3.4(C)	normpyct 8984  normpyth 8980  normpytht 8983
[Beran] p. 99	Remark	lnfn0 9941  lnfn0t 9946  lnop0 9865  lnop0t 9861
[Beran] p. 99	Theorem 3.5(i)	nmcfnex 9956  nmcfnext 9958  nmcopex 9927  nmcopexlem1 9921  nmcopext 9929
[Beran] p. 99	Theorem 3.5(ii)	nmcfnlb 9957  nmcfnlbt 9959  nmcoplb 9928  nmcoplbt 9930
[Beran] p. 99	Theorem 3.5(iii)	lnfncon 9960  lnfncont 9961  lnopcon 9933  lnopcont 9934
[Beran] p. 99	Definition of operator	df-hosum 9478
[Beran] p. 100	Lemma 3.6	normpar2 8994  projlem1 9157  projlem10 9166  projlem11 9167  projlem12 9168  projlem13 9169  projlem14 9170  projlem15 9171  projlem16 9172  projlem17 9173  projlem17 9173  projlem2 9158  projlem21 9177  projlem22 9178  projlem3 9159  projlem5 9161  projlem8 9164  projlem8 9164  projlem9 9165
[Beran] p. 101	Lemma 3.6	norm3adif 8986  norm3adift 8991  norm3dif 8985  norm3dift 8988  projlem 9188  projlem18 9174  projlem19 9175  projlem20 9176  projlem23 9179  projlem24 9180  projlem25 9181  projlem26 9182  projlem27 9183  projlem28 9184  projlem29 9185  projlem30 9186  projlem31 9187  projlem4 9160  projlem6 9162  projlem7 9163
[Beran] p. 102	Theorem 3.7(i)	chocuni 9143  pjpjth 9229  pjpjtht 9228  pjth 9203  pjtht 9204
[Beran] p. 102	Theorem 3.7(ii)	ococ 9217  ococt 9218
[Beran] p. 103	Remark 3.8	nlelch 9964
[Beran] p. 104	Theorem 3.9	riesz3 9965  riesz4 9966  riesz4t 9967
[Beran] p. 104	Theorem 3.10	cnlnadj 9979  cnlnadjeu 9980  cnlnadjeut 9981  cnlnadjlem1 9970  cnlnadjt 9982  nmopadjle 9991
[Beran] p. 106	Theorem 3.11(i)	adjeq0 9994
[Beran] p. 106	Theorem 3.11(v)	nmopadj 9993
[Beran] p. 106	Theorem 3.11(ii)	adjmult 9995
[Beran] p. 106	Theorem 3.11(iv)	adjadjt 9831
[Beran] p. 106	Theorem 3.11(vi)	nmopcoadj 10004  nmopcoadj2 10005
[Beran] p. 106	Theorem 3.11(iii)	adjaddt 9996
[Beran] p. 106	Theorem 3.11(vii)	nmopcoadj0 10006
[Beran] p. 106	Theorem 3.11(viii)	adjco 10003  pjadj2co 10102  pjadjco 10059
[Beran] p. 107	Definition	closedsub 9064  df-ch 9063
[Beran] p. 107	Remark 3.12	chocclt 9155  chsscm 9083  occl 9152  occllem1 9144  occllem2 9145  occllem3 9146  occllem4 9147  occllem5 9148  occllem6 9149  occllem7 9150  occllem8 9151  occlt 9153  ocsh 9127  shocclt 9154  shocsh 9128
[Beran] p. 107	Remark 3.12(B)	ococint 9267
[Beran] p. 107	Remark 3.12(C)	ch2 9085  chcmh 9084
[Beran] p. 108	Theorem 3.13	chintclt 9266
[Beran] p. 109	Property (i)	pjadj 9590  pjadj2t 10084  pjadj3t 10085  pjadjt 9602
[Beran] p. 109	Property (ii)	pjidm 9589  pjidmco 10075  pjidmcot 10079
[Beran] p. 110	Definition of projector ordering	pjord 10071
[Beran] p. 111	Remark	ho0valt 9648  pjch1t 9587
[Beran] p. 111	Definition	df-hfmul 9482  df-hfsum 9481  df-hodif 9480  df-homul 9479  df-hosum 9478
[Beran] p. 111	Lemma 4.4(i)	pjot 9588
[Beran] p. 111	Lemma 4.4(ii)	pjch 9235  pjcht 9611
[Beran] p. 111	Lemma 4.4(iii)	pjoc2 9241  pjoc2t 9242
[Beran] p. 112	Theorem 4.5(i)->(ii)	pjss2 9597
[Beran] p. 112	Theorem 4.5(i)->(iv)	pjssm 9598  pjssmt 10063
[Beran] p. 112	Theorem 4.5(i)<->(ii)	pjss2co 10062
[Beran] p. 112	Theorem 4.5(i)<->(iii)	pjss1co 10061
[Beran] p. 112	Theorem 4.5(i)<->(vi)	pjnormss 10066
[Beran] p. 112	Theorem 4.5(iv)->(v)	pjssge0 9599  pjssge0t 10064
[Beran] p. 112	Theorem 4.5(v)<->(vi)	pjdifnorm 9600  pjdifnormt 10065
[ChoquetDD] p. 2	Definition of mapping	df-mpt 4075
[Cohen] p. 301	Remark	logoprlemOLD 8741  relogoprlem 8723
[Cohen] p. 301	Property 2	logmultOLD 8742  relogmult 8724
[Cohen] p. 301	Property 3	logdivtOLD 8743  relogdivt 8725
[Cohen] p. 301	Property 4	logexptOLD 8744  relogexpt 8728
[Cohen] p. 301	Property 1a	log1 8720  log1OLD 8739
[Cohen] p. 301	Property 1b	loge 8721  logeOLD 8740
[Diestel] p. 2	Definition	df-sgra 10686
[Diestel] p. 28	Definition	df-pgra 10683
[Diestel] p. 28	Definition of hypergraph	ishgrag 10674
[Eisenberg] p. 67	Definition 5.3	df-dif 2045
[Eisenberg] p. 82	Definition 6.3	dfom3 4621
[Eisenberg] p. 125	Definition 8.21	df-map 4324
[Eisenberg] p. 216	Example 13.2(4)	omenps 4627
[Eisenberg] p. 310	Theorem 19.8	cardprc 4852
[Eisenberg] p. 310	Corollary 19.7(2)	cardsdom 4828
[Enderton] p. 18	Axiom of Empty Set	axnul 2705
[Enderton] p. 19	Definition	df-tp 2411
[Enderton] p. 26	Exercise 5	unissb 2524
[Enderton] p. 26	Exercise 10	pwel 2755
[Enderton] p. 28	Exercise 7(b)	pwun 2826
[Enderton] p. 30	Theorem "Distributive laws"	iinun2 2605  iunin2 2604
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2 2607  iundif2 2606
[Enderton] p. 32	Exercise 20	unineq 2251
[Enderton] p. 33	Exercise 23	iinuni 2611
[Enderton] p. 33	Exercise 25	iununi 2612
[Enderton] p. 33	Exercise 24(a)	iinpw 2613
[Enderton] p. 33	Exercise 24(b)	iunpw 2913  iunpwss 2614
[Enderton] p. 36	Definition	opthwiener 2804
[Enderton] p. 38	Exercise 6(a)	unipw 2752
[Enderton] p. 38	Exercise 6(b)	pwuni 2753
[Enderton] p. 41	Lemma 3D	opeluu 2878  rnexg 3358
[Enderton] p. 41	Exercise 8	dmuni 3319  rnuni 3458
[Enderton] p. 42	Definition of a function	dffun6 3540  dffun7 3541
[Enderton] p. 43	Definition of function value	funfv2 3772
[Enderton] p. 43	Definition of single-rooted	funcnv 3559
[Enderton] p. 44	Definition (d)	dfima2 3402  dfima3 3403
[Enderton] p. 47	Theorem 3H	fvco2 3776
[Enderton] p. 49	Axiom of Choice (first form)	ac7 4739  ac7g 4740  aceq3 4724  aceq4 4725  aceq5 4731  aceq6a 4732  aceq6b 4733  aceq7 4734  aceqkm 4772
[Enderton] p. 50	Theorem 3K(a)	imaiun 3865
[Enderton] p. 52	Definition	df-map 4324
[Enderton] p. 53	Exercise 21	coass 3512
[Enderton] p. 53	Exercise 27	dmco2 3504
[Enderton] p. 53	Exercise 14(a)	funin 3568
[Enderton] p. 53	Exercise 22(a)	imass2 3430
[Enderton] p. 54	Remark	ixpf 4356  ixpssmap 4363
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 4348
[Enderton] p. 55	Axiom of Choice (second form)	ac9s 4755
[Enderton] p. 56	Theorem 3M	erref 4275
[Enderton] p. 57	Lemma 3N	erthi 4281
[Enderton] p. 57	Definition	df-ec 4263
[Enderton] p. 58	Definition	df-qs 4266
[Enderton] p. 60	Theorem 3Q	th3q 4317  th3qcor 4316  th3qlem1 4314  th3qlem2 4315
[Enderton] p. 61	Exercise 35	df-ec 4263
[Enderton] p. 65	Exercise 56(a)	dmun 3317
[Enderton] p. 68	Definition of successor	df-suc 2953
[Enderton] p. 71	Definition	df-tr 2677  dftr4 2681
[Enderton] p. 72	Theorem 4E	unisuc 3046
[Enderton] p. 73	Exercise 6	unisuc 3046
[Enderton] p. 79	Theorem 4I(A1)	nna0 4223
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 4225
[Enderton] p. 79	Definition of operation value	df-opr 3966
[Enderton] p. 80	Theorem 4J(A1)	nnm0 4224
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 4226
[Enderton] p. 81	Theorem 4K(1)	nnaass 4237
[Enderton] p. 81	Theorem 4K(2)	nna0r 4227  nnacom 4233
[Enderton] p. 81	Theorem 4K(3)	nndi 4238
[Enderton] p. 81	Theorem 4K(4)	nnmass 4239
[Enderton] p. 81	Theorem 4K(5)	nnmcom 4241
[Enderton] p. 82	Exercise 16	nnm0r 4228  nnmsucr 4240
[Enderton] p. 88	Exercise 23	nnaordex 4249
[Enderton] p. 129	Definition	bren 4375  df-en 4367
[Enderton] p. 132	Theorem 6B(b)	canth 3908
[Enderton] p. 133	Exercise 1	xpomen 7461
[Enderton] p. 133	Exercise 2	qnnen 7465
[Enderton] p. 134	Theorem (Pigeonhole Principle)	php 4510
[Enderton] p. 135	Corollary 6C	php3 4512
[Enderton] p. 136	Corollary 6E	nneneq 4509
[Enderton] p. 136	Corollary 6D(a)	pssinf 4524
[Enderton] p. 136	Corollary 6D(b)	ominf 4525
[Enderton] p. 137	Lemma 6F	pssnn 4530
[Enderton] p. 138	Corollary 6G	ssfi 4532
[Enderton] p. 139	Theorem 6H(c)	mapen 4488
[Enderton] p. 142	Theorem 6I(3)	xpcdaen 4922
[Enderton] p. 142	Theorem 6I(4)	mapcdaen 4923
[Enderton] p. 143	Theorem 6J	cda0en 4916  cda1en 4917
[Enderton] p. 144	Exercise 13	iunfi 4560  unifi 4549  unifi2 4550
[Enderton] p. 144	Corollary 6K	undif2 2337  unfi 4545  unfi2 4546
[Enderton] p. 145	Figure 38	ffoss 3712
[Enderton] p. 145	Definition	df-dom 4368
[Enderton] p. 146	Example 1	domen 4377  domeng 4378
[Enderton] p. 146	Example 3	nndomo 4517  omsdomnn 4526
[Enderton] p. 149	Theorem 6L(a)	cdadom2 4925
[Enderton] p. 149	Theorem 6L(c)	mapdom1 4489  xpdom1 4439  xpdom1g 4440
[Enderton] p. 149	Theorem 6L(d)	mapdom2 4491
[Enderton] p. 151	Theorem 6M	zorn 4788
[Enderton] p. 151	Theorem 6M(4)	ac8 4754  aceq5 4731
[Enderton] p. 159	Theorem 6Q	unictb 7537
[Enderton] p. 162	Lemma 6R	infxpidm 7526
[Enderton] p. 164	Example	infdif 7530
[Enderton] p. 165	Exercise 34	infmap1 7535
[Enderton] p. 168	Definition	df-po 2839
[Enderton] p. 192	Theorem 7M(a)	onel 3098
[Enderton] p. 192	Theorem 7M(b)	ontr1 3003
[Enderton] p. 192	Theorem 7M(c)	onirr 3097
[Enderton] p. 193	Corollary 7N(b)	0elon 3022
[Enderton] p. 193	Corollary 7N(c)	onsuc 3105
[Enderton] p. 193	Corollary 7N(d)	ssonuni 2995
[Enderton] p. 194	Remark	onprc 2989
[Enderton] p. 194	Exercise 16	suc11 3093
[Enderton] p. 197	Definition	df-card 4807
[Enderton] p. 197	Theorem 7P	carden 4822
[Enderton] p. 200	Exercise 25	tfis 3127
[Enderton] p. 202	Lemma 7T	r1tr 4645
[Enderton] p. 202	Definition	df-r1 4634
[Enderton] p. 202	Theorem 7Q	r1val1 4649
[Enderton] p. 204	Theorem 7V(b)	rankval4 4693
[Enderton] p. 206	Theorem 7X(b)	en2lp 4593
[Enderton] p. 207	Exercise 30	rankpr 4683  rankpw 4675  rankuniss 4692
[Enderton] p. 207	Exercise 34	opthreg 4595
[Enderton] p. 208	Exercise 35	suc11reg 4596
[Enderton] p. 212	Definition of aleph	alephval3 4894
[Enderton] p. 213	Theorem 8A(a)	alephord2 4867
[Enderton] p. 213	Theorem 8A(b)	cardalephex 4877
[Enderton] p. 222	Definition of kard	karden 4717  kardex 4716
[Enderton] p. 240	Exercise 25	oarec 4196
[Enderton] p. 257	Definition of cofinality	cflim 4900
[FreydScedrov] p. 283	Axiom of Infinity	ax-inf 4613  inf1 4598  inf2 4599
[Gleason] p. 117	Proposition 9-2.1	df-enq 5028  enqer 5037
[Gleason] p. 117	Proposition 9-2.2	df-1q 5034  df-nq 5029
[Gleason] p. 117	Proposition 9-2.3	df-plpq 5026  df-plq 5030
[Gleason] p. 119	Proposition 9-2.4	caoprmo 4072  df-mpq 5027  df-mq 5031
[Gleason] p. 119	Proposition 9-2.5	df-rq 5032
[Gleason] p. 119	Proposition 9-2.6	ltexpq 5071  ltexpq2 5072
[Gleason] p. 120	Proposition 9-2.6(i)	halfpq 5073  ltbtwnpq 5075
[Gleason] p. 120	Proposition 9-2.6(ii)	ltapq 5067
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmpq 5068
[Gleason] p. 120	Proposition 9-2.6(iv)	ltrpq 5076
[Gleason] p. 121	Definition 9-3.1	df-np 5077
[Gleason] p. 121	Definition 9-3.1 (ii)	prcdpq 5088
[Gleason] p. 121	Definition 9-3.1(iii)	prnmax 5090
[Gleason] p. 122	Definition	df-1p 5078
[Gleason] p. 122	Remark (1)	prub 5089
[Gleason] p. 122	Lemma 9-3.4	prlem934 5130  prlem934a 5128  prlem934b 5129
[Gleason] p. 122	Proposition 9-3.2	df-ltp 5081
[Gleason] p. 122	Proposition 9-3.3	ltsopr 5127  psslinpr 5126  supexpr 5154  suplem1pr 5152  suplem2pr 5153
[Gleason] p. 123	Proposition 9-3.5	addclpr 5111  addclprlem1 5109  addclprlem2 5110  df-plp 5079
[Gleason] p. 123	Proposition 9-3.5(i)	addasspr 5115
[Gleason] p. 123	Proposition 9-3.5(ii)	addcompr 5114
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 5131
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 5140  ltexprlem1 5133  ltexprlem2 5134  ltexprlem3 5135  ltexprlem4 5136  ltexprlem5 5137  ltexprlem6 5138  ltexprlem7 5139
[Gleason] p. 123	Proposition 9-3.5(v)	ltapr 5142  ltaprlem 5141
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanpr 5143
[Gleason] p. 124	Lemma 9-3.6	prlem936 5146  prlem936a 5144  prlem936b 5145
[Gleason] p. 124	Proposition 9-3.7	df-mp 5080  mulclpr 5113  mulclprlem 5112  reclem1pr 5147  reclem2pr 5148
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 5124
[Gleason] p. 124	Proposition 9-3.7(i)	mulasspr 5117
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcompr 5116
[Gleason] p. 124	Proposition 9-3.7(iii)	distrpr 5123
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 5151  reclem3pr 5149  reclem4pr 5150
[Gleason] p. 126	Proposition 9-4.1	df-enr 5157  df-mpr 5156  df-plpr 5155  enrer 5167
[Gleason] p. 126	Proposition 9-4.2	df-0r 5162  df-1r 5163  df-nr 5158
[Gleason] p. 126	Proposition 9-4.3	df-mr 5160  df-plr 5159  negexsr 5202  recexsr 5207  recexsrlem 5203
[Gleason] p. 127	Proposition 9-4.4	df-ltr 5161
[Gleason] p. 130	Proposition 10-1.3	creui 6693  creur 6692  cru 6686  crut 6687  crutOLD 6688
[Gleason] p. 130	Definition 10-1.1(v)	axcnre 5277
[Gleason] p. 132	Definition 10-3.1	crim 6727  crimOLD 6728  crimt 6723  crimtOLD 6724  crre 6725  crreOLD 6726  crret 6721  crretOLD 6722
[Gleason] p. 132	Definition 10-3.2	cjvalt 6714
[Gleason] p. 133	Definition 10.36	absval2 6795  absval2t 6806
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 6742  cjaddt 6766
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 6743  cjmult 6767
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 6732  cjcjt 6765
[Gleason] p. 133	Proposition 10-3.4(f)	cjreb 6735  cjrebt 6754  cjret 6764  rereb 6734  reret 6753
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 6752  addcjt 6769
[Gleason] p. 133	Proposition 10-3.7(a)	absvalt 6713
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 6799  abscjt 6788
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 6796  abs00t 6807
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 6847  releabst 6843
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 6801  absmult 6812
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 6804  sqabsaddt 6802
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 6848  abstrit 6854
[Gleason] p. 134	Definition 10-4.1	df-exp 6520  exp0t 6522  expp1t 6525
[Gleason] p. 135	Proposition 10-4.2(a)	expaddt 6546
[Gleason] p. 135	Proposition 10-4.2(b)	expmult 6547
[Gleason] p. 135	Proposition 10-4.2(c)	mulexpt 6544
[Gleason] p. 140	Exercise 1	znnen 7464
[Gleason] p. 141	Definition 11-2.1	fzvalt 6420
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 7072
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 7085
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 7083
[Gleason] p. 171	Corollary 12-2.2	climmulc 7088  climmulc2 7084
[Gleason] p. 172	Corollary 12-2.5	climfnrcl 7067  climrecl 7066
[Gleason] p. 172	Proposition 12-2.4(c)	climcj 7105
[Gleason] p. 173	Definition 12-3.1	df-ltxr 5481  df-xr 5480  ltxrt 5486
[Gleason] p. 175	Definition 12-4.1	df-limsup 6479  limsupvalt 6480
[Gleason] p. 180	Theorem 12-5.1	climsup 7110
[Gleason] p. 180	Theorem 12-5.3	caucvg3 7122  caucvg3a 7119  caucvg3t 7123  climcau 7111
[Gleason] p. 181	Remark	cau2 6869
[Gleason] p. 182	Exercise 3	cvgcmp 7139
[Gleason] p. 182	Exercise 4	cvgrat 7209
[Gleason] p. 195	Theorem 13-2.12	abs1m 6860
[Gleason] p. 217	Lemma 13-4.1	btwnzge0t 6207
[Gleason] p. 223	Definition 14-1.1	df-met 7754
[Gleason] p. 223	Definition 14-1.1(a)	met0 7776
[Gleason] p. 223	Definition 14-1.1(b)	metgt0 7783
[Gleason] p. 223	Definition 14-1.1(c)	metsym 7777
[Gleason] p. 223	Definition 14-1.1(d)	mettri 7778  mettriOLD 7779
[Gleason] p. 225	Definition 14-1.5	metxp 7797  metxpcl 7795  metxpdval 7792  metxpfval 7794  metxptval 7793
[Gleason] p. 230	Proposition 14-2.6	xplm 7934  xplmi 7932  xplmi2 7933
[Gleason] p. 240	Theorem 14-4.3	metcnp4 7929
[Gleason] p. 240	Proposition 14-4.2	metcnp3 7859
[Gleason] p. 243	Proposition 14-4.16	addcn 7945  mulcn 7947  subcn 7946
[Gleason] p. 295	Remark	bcval4t 6918
[Gleason] p. 295	Equation 2	bcpasc 6926  bcpasc2 6924  bcpasc2t 6925  bcpasct 6927
[Gleason] p. 295	Definition of binomial coefficient	bcvalt 6914  df-bc 6913
[Gleason] p. 296	Remark	bcn0t 6920  bcnnt 6921
[Gleason] p. 296	Theorem 15-2.8	binom 7029
[Gleason] p. 308	Equation 2	ef0 7296
[Gleason] p. 308	Equation 3	efcj 7297  efcjt 7298
[Gleason] p. 309	Corollary 15-4.3	efne0t 7330
[Gleason] p. 309	Corollary 15-4.4	efexpt 7333
[Gleason] p. 310	Equation 14	sinadd 7412  sinaddt 7414
[Gleason] p. 310	Equation 15	cosadd 7413  cosaddt 7415
[Gleason] p. 311	Equation 17	sincossqt 7422
[Gleason] p. 311	Equation 18	cosbndt 7427  sinbndt 7426
[Gleason] p. 311	Lemma 15-4.7	sqeqor 6597  sqeqort 6599
[Gleason] p. 311	Definition of pi	df-pi 7263
[Godowski] p. 730	Equation SF	goeq 10170
[GodowskiGreechie] p. 249	Equation IV	3oa 9585
[Goldberg] p. 10	Definition of operator	df-hosum 9478
[Halmos] p. 31	Theorem 17.3	riesz1t 9968  riesz2t 9969
[Halmos] p. 35	Definition of operator	df-hosum 9478
[Halmos] p. 41	Definition of Hermitian	hmopadj2t 9836
[Halmos] p. 42	Definition of projector ordering	pjord 10071
[Halmos] p. 43	Theorem 26.1	elpjhmopt 10083  elpjidmt 10082  pjnmop 10045
[Halmos] p. 44	Remark	pjinorm 9593  pjinormt 9604
[Halmos] p. 44	Theorem 26.2	elpjcht 10086  pjrn 9619  pjrnt 9624  pjvect 9613
[Halmos] p. 44	Theorem 26.3	pjnorm2t 9644
[Halmos] p. 44	Theorem 26.4	hmopidmpj 10050  hmopidmpjt 10052
[Halmos] p. 45	Theorem 27.1	pjinvar 10089
[Halmos] p. 45	Theorem 27.3	pjoc 10078  pjocvect 9614
[Halmos] p. 45	Theorem 27.4	pjorthco 10067
[Halmos] p. 48	Theorem 29.2	pjsspos 10070
[Halmos] p. 48	Theorem 29.3	pjssdif1 10073  pjssdif2 10072
[Halmos] p. 50	Definition of spectrum	df-spec 9753
[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 961
[Herstein] p. 54	Exercise 28	df-grp 7996
[Herstein] p. 55	Lemma 2.2.1(a)	grpideu 8012
[Herstein] p. 55	Lemma 2.2.1(b)	grpinveu 8023
[Herstein] p. 55	Lemma 2.2.1(c)	grp2inv 8038
[Herstein] p. 55	Lemma 2.2.1(d)	grpinvop 8040
[Herstein] p. 57	Exercise 1	isgrp2i 8036
[Holland] p. 1519	Theorem 2	sumdmd 10314
[Holland] p. 1520	Lemma 5	cdj1 10325  cdj3 10333  cdj3lem1 10326  cdjreu 10324
[Holland] p. 1524	Lemma 7	mddmdin0 10323
[Hughes] p. 14	Definition of operator	df-hosum 9478
[Hughes] p. 44	Equation 1.21b	ax-his3 8922
[Hughes] p. 47	Definition of projection operator	dfpjopt 10081
[Hughes] p. 49	Equation 1.30	eighmret 9858  eigre 9732  eigret 9733
[Hughes] p. 49	Equation 1.31	eighmortht 9859  eigorth 9735  eigortht 9736
[Hughes] p. 137	Remark (ii)	eigpos 9734
[Jech] p. 4	Definition of class	cv 953  cvjust 1469
[Jech] p. 42	Lemma 6.1	alephexp1 7545
[Jech] p. 42	Equation 6.1	alephadd 7543  alephmul 7544
[Jech] p. 43	Lemma 6.2	infmap2 7542
[Jech] p. 71	Lemma 9.3	jech9.3 4657
[Jech] p. 72	Equation 9.3	scott0 4708  scottex 4707
[Jech] p. 72	Exercise 9.1	rankval4 4693
[Jech] p. 72	Scheme "Collection Principle"	cp 4713
[Jech] p. 78	Definition implied by the footnote	opthprc 3221
[KalishMontague] p. 81	Axiom B7' in footnote 1	ax-9 963
[Kalmbach] p. 14	Definition of lattice	chabs1 9411  chabs1t 9409  chabs2 9412  chabs2t 9410  chjass 9379  chjasst 9426
[Kalmbach] p. 15	Definition of atom	df-at 10233  elat 10234
[Kalmbach] p. 15	Definition of covers	cvbr2t 10180
[Kalmbach] p. 20	Definition of commutes	cmbr 9505  cmbrt 9499  df-cm 9498
[Kalmbach] p. 22	Remark	pjoml5 9503  pjoml5t 9528
[Kalmbach] p. 22	Definition	pjoml2 9500  pjoml2t 9526
[Kalmbach] p. 22	Theorem 2(v)	cmcm 9507  cmcmi 9512  cmcmt 9529
[Kalmbach] p. 22	Theorem 2(ii)	omls 9216  pjoml 9238  pjomlt 9239
[Kalmbach] p. 23	Remark	cmbr2 9511  cmcm3 9509  cmcm3i 9514  cmcm3t 9530  cmcm4 9510
[Kalmbach] p. 23	Lemma 3	cmbr3 9515  cmbr3t 9523
[Kalmbach] p. 25	Theorem 5	fh1 9536  fh1t 9533  fh2 9537  fh2t 9534
[Kalmbach] p. 65	Remark	chjatom 10252  chslej 9351  chslejt 9391  shslej 9308  shslejt 9320
[Kalmbach] p. 65	Proposition 1	chocin 9347  chocint 9388  chsupclt 9278  chsupval2t 9272  dfchsup2 9268  h0elch 9098  helch 9087  hsupval2t 9270  ocin 9140  ococss 9137  shococss 9138
[Kalmbach] p. 65	Definition of subspace sum	shsumvalt 9247
[Kalmbach] p. 66	Remark	df-pj 9207  pjssm 9598  pjssmt 10063
[Kalmbach] p. 67	Lemma 3	osum 9558  osumt 9560
[Kalmbach] p. 67	Lemma 4	pjc 10098
[Kalmbach] p. 103	Exercise 6	atmd2 10295
[Kalmbach] p. 103	Exercise 12	mdsl0 10205
[Kalmbach] p. 140	Remark	hatomic 10254  hatomict 10255  hatomistic 10257
[Kalmbach] p. 140	Proposition 1(i)	atexcht 10276
[Kalmbach] p. 140	Proposition 1(ii)	chcv1t 10250
[Kalmbach] p. 140	Proposition 1(iii)	cvexch 10264  cvexcht 10269
[Kalmbach] p. 149	Remark 2	chrelat 10259
[Kalmbach] p. 153	Exercise 5	spansncv 9569  spansncvt 9570
[Kalmbach] p. 153	Proposition 1(ii)	spansncv2t 10190
[Kalmbach] p. 266	Definition	df-st 10109
[Kalmbach] p. 353	Definition of operator	df-hosum 9478
[Kalmbach2] p. 8	Definition of adjoint	df-adjh 9747
[Kreyszig] p. 3	Property M1	metcl 7772
[Kreyszig] p. 4	Property M2	meteq0 7773
[Kreyszig] p. 8	Definition 1.1-8	dscmet 7881
[Kreyszig] p. 12	Equation 5	conjmult 5772  muleqaddt 5688
[Kreyszig] p. 18	Definition 1.3-2	opnfval