Theorem fmptco 6893

Description: Composition of two functions expressed as ordered-pair class abstractions. If 𝐹 has the equation (𝑥 + 2) and 𝐺 the equation (3∗𝑧) then (𝐺 ∘ 𝐹) has the equation (3∗(𝑥 + 2)). (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro, 24-Jul-2014.)

Hypotheses

Ref	Expression
fmptco.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝐵)
fmptco.2	⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅))
fmptco.3	⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆))
fmptco.4	⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇)

Assertion

Ref	Expression
fmptco	⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇))

Distinct variable groups:   𝑥,𝐴   𝑥,𝑦,𝐵   𝑦,𝑅   𝜑,𝑥   𝑥,𝑆   𝑦,𝑇

Allowed substitution hints:   𝜑(𝑦)   𝐴(𝑦)   𝑅(𝑥)   𝑆(𝑦)   𝑇(𝑥)   𝐹(𝑥,𝑦)   𝐺(𝑥,𝑦)

Proof of Theorem fmptco

Dummy variables 𝑣 𝑢 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relco 6099	. 2 ⊢ Rel (𝐺 ∘ 𝐹)
2		mptrel 5699	. 2 ⊢ Rel (𝑥 ∈ 𝐴 ↦ 𝑇)
3		fmptco.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅))
4		fmptco.1	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝐵)
5	3, 4	fmpt3d 6882	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
6	5	ffund 6520	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝐹)
7		funbrfv 6718	. . . . . . . . . . 11 ⊢ (Fun 𝐹 → (𝑧𝐹𝑢 → (𝐹‘𝑧) = 𝑢))
8	7	imp 409	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ 𝑧𝐹𝑢) → (𝐹‘𝑧) = 𝑢)
9	6, 8	sylan 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → (𝐹‘𝑧) = 𝑢)
10	9	eqcomd 2829	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → 𝑢 = (𝐹‘𝑧))
11	10	a1d 25	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → (𝑢𝐺𝑤 → 𝑢 = (𝐹‘𝑧)))
12	11	expimpd 456	. . . . . 6 ⊢ (𝜑 → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) → 𝑢 = (𝐹‘𝑧)))
13	12	pm4.71rd 565	. . . . 5 ⊢ (𝜑 → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤))))
14	13	exbidv 1922	. . . 4 ⊢ (𝜑 → (∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ ∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤))))
15		fvex 6685	. . . . . 6 ⊢ (𝐹‘𝑧) ∈ V
16		breq2 5072	. . . . . . 7 ⊢ (𝑢 = (𝐹‘𝑧) → (𝑧𝐹𝑢 ↔ 𝑧𝐹(𝐹‘𝑧)))
17		breq1 5071	. . . . . . 7 ⊢ (𝑢 = (𝐹‘𝑧) → (𝑢𝐺𝑤 ↔ (𝐹‘𝑧)𝐺𝑤))
18	16, 17	anbi12d 632	. . . . . 6 ⊢ (𝑢 = (𝐹‘𝑧) → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤)))
19	15, 18	ceqsexv 3543	. . . . 5 ⊢ (∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) ↔ (𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤))
20		funfvbrb 6823	. . . . . . . . 9 ⊢ (Fun 𝐹 → (𝑧 ∈ dom 𝐹 ↔ 𝑧𝐹(𝐹‘𝑧)))
21	6, 20	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑧 ∈ dom 𝐹 ↔ 𝑧𝐹(𝐹‘𝑧)))
22	5	fdmd 6525	. . . . . . . . 9 ⊢ (𝜑 → dom 𝐹 = 𝐴)
23	22	eleq2d 2900	. . . . . . . 8 ⊢ (𝜑 → (𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝐴))
24	21, 23	bitr3d 283	. . . . . . 7 ⊢ (𝜑 → (𝑧𝐹(𝐹‘𝑧) ↔ 𝑧 ∈ 𝐴))
25	3	fveq1d 6674	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝑧) = ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧))
26		fmptco.3	. . . . . . . 8 ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆))
27		eqidd 2824	. . . . . . . 8 ⊢ (𝜑 → 𝑤 = 𝑤)
28	25, 26, 27	breq123d 5082	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘𝑧)𝐺𝑤 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤))
29	24, 28	anbi12d 632	. . . . . 6 ⊢ (𝜑 → ((𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤)))
30		nfcv 2979	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑧
31		nfv 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝜑
32		nffvmpt1 6683	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)
33		nfcv 2979	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐵 ↦ 𝑆)
34		nfcv 2979	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝑤
35	32, 33, 34	nfbr 5115	. . . . . . . . . . 11 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤
36		nfcsb1v 3909	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝑇
37	36	nfeq2 2997	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑤 = ⦋𝑧 / 𝑥⦌𝑇
38	35, 37	nfbi 1904	. . . . . . . . . 10 ⊢ Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)
39	31, 38	nfim 1897	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
40		fveq2 6672	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧))
41	40	breq1d 5078	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤))
42		csbeq1a 3899	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → 𝑇 = ⦋𝑧 / 𝑥⦌𝑇)
43	42	eqeq2d 2834	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝑤 = 𝑇 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
44	41, 43	bibi12d 348	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → ((((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇) ↔ (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
45	44	imbi2d 343	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇)) ↔ (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))))
46		vex 3499	. . . . . . . . . . . 12 ⊢ 𝑤 ∈ V
47		simpl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → 𝑦 = 𝑅)
48	47	eleq1d 2899	. . . . . . . . . . . . . 14 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → (𝑦 ∈ 𝐵 ↔ 𝑅 ∈ 𝐵))
49		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑤 → 𝑢 = 𝑤)
50		fmptco.4	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇)
51	49, 50	eqeqan12rd 2842	. . . . . . . . . . . . . 14 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → (𝑢 = 𝑆 ↔ 𝑤 = 𝑇))
52	48, 51	anbi12d 632	. . . . . . . . . . . . 13 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → ((𝑦 ∈ 𝐵 ∧ 𝑢 = 𝑆) ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
53		df-mpt 5149	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐵 ↦ 𝑆) = {⟨𝑦, 𝑢⟩ ∣ (𝑦 ∈ 𝐵 ∧ 𝑢 = 𝑆)}
54	52, 53	brabga 5423	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ 𝐵 ∧ 𝑤 ∈ V) → (𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
55	4, 46, 54	sylancl 588	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
56		id 22	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
57		eqid 2823	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅)
58	57	fvmpt2 6781	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑅 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅)
59	56, 4, 58	syl2an2 684	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅)
60	59	breq1d 5078	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤))
61	4	biantrurd 535	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑤 = 𝑇 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
62	55, 60, 61	3bitr4d 313	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇))
63	62	expcom 416	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇)))
64	30, 39, 45, 63	vtoclgaf 3575	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
65	64	impcom 410	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
66	65	pm5.32da 581	. . . . . 6 ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
67	29, 66	bitrd 281	. . . . 5 ⊢ (𝜑 → ((𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
68	19, 67	syl5bb 285	. . . 4 ⊢ (𝜑 → (∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
69	14, 68	bitrd 281	. . 3 ⊢ (𝜑 → (∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
70		vex 3499	. . . 4 ⊢ 𝑧 ∈ V
71	70, 46	opelco 5744	. . 3 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝐺 ∘ 𝐹) ↔ ∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤))
72		df-mpt 5149	. . . . 5 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑇) = {⟨𝑥, 𝑣⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)}
73	72	eleq2i 2906	. . . 4 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝑥 ∈ 𝐴 ↦ 𝑇) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)})
74		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐴
75	36	nfeq2 2997	. . . . . 6 ⊢ Ⅎ𝑥 𝑣 = ⦋𝑧 / 𝑥⦌𝑇
76	74, 75	nfan 1900	. . . . 5 ⊢ Ⅎ𝑥(𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇)
77		nfv 1915	. . . . 5 ⊢ Ⅎ𝑣(𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)
78		eleq1w 2897	. . . . . 6 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))
79	42	eqeq2d 2834	. . . . . 6 ⊢ (𝑥 = 𝑧 → (𝑣 = 𝑇 ↔ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇))
80	78, 79	anbi12d 632	. . . . 5 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇)))
81		eqeq1 2827	. . . . . 6 ⊢ (𝑣 = 𝑤 → (𝑣 = ⦋𝑧 / 𝑥⦌𝑇 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
82	81	anbi2d 630	. . . . 5 ⊢ (𝑣 = 𝑤 → ((𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
83	76, 77, 70, 46, 80, 82	opelopabf 5434	. . . 4 ⊢ (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)} ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
84	73, 83	bitri 277	. . 3 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝑥 ∈ 𝐴 ↦ 𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
85	69, 71, 84	3bitr4g 316	. 2 ⊢ (𝜑 → (⟨𝑧, 𝑤⟩ ∈ (𝐺 ∘ 𝐹) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑥 ∈ 𝐴 ↦ 𝑇)))
86	1, 2, 85	eqrelrdv 5667	1 ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537  ∃wex 1780   ∈ wcel 2114  Vcvv 3496  ⦋csb 3885  ⟨cop 4575   class class class wbr 5068  {copab 5130   ↦ cmpt 5148  dom cdm 5557   ∘ ccom 5561  Fun wfun 6351  ‘cfv 6357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-fv 6365

This theorem is referenced by:  fmptcof  6894  cofmpt  6896  fcompt  6897  fcoconst  6898  ofco  7431  ccatco  14199  rlimcn1  14947  rlimdiv  15004  ackbijnn  15185  setcepi  17350  prf1st  17456  prf2nd  17457  hofcllem  17510  prdsidlem  17945  pws0g  17949  pwsco1mhm  17998  pwsco2mhm  17999  smndex1iidm  18068  smndex2dlinvh  18084  pwsinvg  18214  pwssub  18215  galactghm  18534  efginvrel1  18856  frgpup3lem  18905  gsumzf1o  19034  gsumconst  19056  gsummptshft  19058  gsumzmhm  19059  gsummhm2  19061  gsummptmhm  19062  gsumsub  19070  gsum2dlem2  19093  dprdfsub  19145  lmhmvsca  19819  psrass1lem  20159  psrlinv  20179  psrcom  20191  evlslem2  20294  coe1fval3  20378  psropprmul  20408  coe1z  20433  coe1mul2  20439  coe1tm  20443  ply1coe  20466  evls1sca  20488  frgpcyg  20722  evpmodpmf1o  20742  mhmvlin  21010  ofco2  21062  mdetleib2  21199  mdetralt  21219  smadiadetlem3  21279  ptrescn  22249  lmcn2  22259  qtopeu  22326  flfcnp2  22617  tgpconncomp  22723  tsmssub  22759  tsmsxplem1  22763  negfcncf  23529  pcopt  23628  pcopt2  23629  pi1xfrcnvlem  23662  ovolctb  24093  ovolfs2  24174  uniioombllem2  24186  ismbf  24231  mbfconst  24236  limccnp2  24492  limcco  24493  dvcof  24547  dvcj  24549  dvfre  24550  dvmptcj  24567  dvmptco  24571  dvcnvlem  24575  dvlip  24592  dvlipcn  24593  itgsubstlem  24647  plyco  24833  dgrcolem1  24865  dgrcolem2  24866  dgrco  24867  plycjlem  24868  taylply2  24958  logcn  25232  leibpi  25522  efrlim  25549  jensenlem2  25567  amgmlem  25569  ftalem7  25658  dchrisum0  26098  ofcfval4  31366  eulerpartgbij  31632  dstfrvclim1  31737  cvmliftlem6  32539  cvmliftphtlem  32566  cvmlift3lem5  32572  elmsubrn  32777  msubco  32780  circum  32919  mblfinlem2  34932  volsupnfl  34939  itgaddnc  34954  itgmulc2nc  34962  ftc1anclem1  34969  ftc1anclem2  34970  ftc1anclem3  34971  ftc1anclem4  34972  ftc1anclem5  34973  ftc1anclem7  34975  ftc1anclem8  34976  fnopabco  35000  upixp  35006  mendassa  39801  fsovrfovd  40362  fsovcnvlem  40366  cncfcompt  42173  dvcosax  42218  dirkercncflem4  42398  fourierdlem111  42509  meadjiunlem  42754  meadjiun  42755  fundcmpsurbijinjpreimafv  43574  amgmwlem  44910  amgmlemALT  44911