Theorem fmptco 7163

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 6138	. 2 ⊢ Rel (𝐺 ∘ 𝐹)
2		mptrel 5849	. 2 ⊢ Rel (𝑥 ∈ 𝐴 ↦ 𝑇)
3		fmptco.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅))
4		fmptco.1	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝐵)
5	3, 4	fmpt3d 7150	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
6	5	ffund 6751	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝐹)
7		funbrfv 6971	. . . . . . . . . . 11 ⊢ (Fun 𝐹 → (𝑧𝐹𝑢 → (𝐹‘𝑧) = 𝑢))
8	7	imp 406	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ 𝑧𝐹𝑢) → (𝐹‘𝑧) = 𝑢)
9	6, 8	sylan 579	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → (𝐹‘𝑧) = 𝑢)
10	9	eqcomd 2746	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → 𝑢 = (𝐹‘𝑧))
11	10	a1d 25	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → (𝑢𝐺𝑤 → 𝑢 = (𝐹‘𝑧)))
12	11	expimpd 453	. . . . . 6 ⊢ (𝜑 → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) → 𝑢 = (𝐹‘𝑧)))
13	12	pm4.71rd 562	. . . . 5 ⊢ (𝜑 → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤))))
14	13	exbidv 1920	. . . 4 ⊢ (𝜑 → (∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ ∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤))))
15		fvex 6933	. . . . . 6 ⊢ (𝐹‘𝑧) ∈ V
16		breq2 5170	. . . . . . 7 ⊢ (𝑢 = (𝐹‘𝑧) → (𝑧𝐹𝑢 ↔ 𝑧𝐹(𝐹‘𝑧)))
17		breq1 5169	. . . . . . 7 ⊢ (𝑢 = (𝐹‘𝑧) → (𝑢𝐺𝑤 ↔ (𝐹‘𝑧)𝐺𝑤))
18	16, 17	anbi12d 631	. . . . . 6 ⊢ (𝑢 = (𝐹‘𝑧) → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤)))
19	15, 18	ceqsexv 3542	. . . . 5 ⊢ (∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) ↔ (𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤))
20		funfvbrb 7084	. . . . . . . . 9 ⊢ (Fun 𝐹 → (𝑧 ∈ dom 𝐹 ↔ 𝑧𝐹(𝐹‘𝑧)))
21	6, 20	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑧 ∈ dom 𝐹 ↔ 𝑧𝐹(𝐹‘𝑧)))
22	5	fdmd 6757	. . . . . . . . 9 ⊢ (𝜑 → dom 𝐹 = 𝐴)
23	22	eleq2d 2830	. . . . . . . 8 ⊢ (𝜑 → (𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝐴))
24	21, 23	bitr3d 281	. . . . . . 7 ⊢ (𝜑 → (𝑧𝐹(𝐹‘𝑧) ↔ 𝑧 ∈ 𝐴))
25	3	fveq1d 6922	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝑧) = ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧))
26		fmptco.3	. . . . . . . 8 ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆))
27		eqidd 2741	. . . . . . . 8 ⊢ (𝜑 → 𝑤 = 𝑤)
28	25, 26, 27	breq123d 5180	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘𝑧)𝐺𝑤 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤))
29	24, 28	anbi12d 631	. . . . . 6 ⊢ (𝜑 → ((𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤)))
30		nfcv 2908	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑧
31		nfv 1913	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝜑
32		nffvmpt1 6931	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)
33		nfcv 2908	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐵 ↦ 𝑆)
34		nfcv 2908	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝑤
35	32, 33, 34	nfbr 5213	. . . . . . . . . . 11 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤
36		nfcsb1v 3946	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝑇
37	36	nfeq2 2926	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑤 = ⦋𝑧 / 𝑥⦌𝑇
38	35, 37	nfbi 1902	. . . . . . . . . 10 ⊢ Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)
39	31, 38	nfim 1895	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
40		fveq2 6920	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧))
41	40	breq1d 5176	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤))
42		csbeq1a 3935	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → 𝑇 = ⦋𝑧 / 𝑥⦌𝑇)
43	42	eqeq2d 2751	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝑤 = 𝑇 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
44	41, 43	bibi12d 345	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → ((((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇) ↔ (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
45	44	imbi2d 340	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇)) ↔ (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))))
46		vex 3492	. . . . . . . . . . . 12 ⊢ 𝑤 ∈ V
47		simpl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → 𝑦 = 𝑅)
48	47	eleq1d 2829	. . . . . . . . . . . . . 14 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → (𝑦 ∈ 𝐵 ↔ 𝑅 ∈ 𝐵))
49		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑤 → 𝑢 = 𝑤)
50		fmptco.4	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇)
51	49, 50	eqeqan12rd 2755	. . . . . . . . . . . . . 14 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → (𝑢 = 𝑆 ↔ 𝑤 = 𝑇))
52	48, 51	anbi12d 631	. . . . . . . . . . . . 13 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → ((𝑦 ∈ 𝐵 ∧ 𝑢 = 𝑆) ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
53		df-mpt 5250	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐵 ↦ 𝑆) = {⟨𝑦, 𝑢⟩ ∣ (𝑦 ∈ 𝐵 ∧ 𝑢 = 𝑆)}
54	52, 53	brabga 5553	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ 𝐵 ∧ 𝑤 ∈ V) → (𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
55	4, 46, 54	sylancl 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
56		id 22	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
57		eqid 2740	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅)
58	57	fvmpt2 7040	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑅 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅)
59	56, 4, 58	syl2an2 685	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅)
60	59	breq1d 5176	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤))
61	4	biantrurd 532	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑤 = 𝑇 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
62	55, 60, 61	3bitr4d 311	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇))
63	62	expcom 413	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇)))
64	30, 39, 45, 63	vtoclgaf 3588	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
65	64	impcom 407	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
66	65	pm5.32da 578	. . . . . 6 ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
67	29, 66	bitrd 279	. . . . 5 ⊢ (𝜑 → ((𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
68	19, 67	bitrid 283	. . . 4 ⊢ (𝜑 → (∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
69	14, 68	bitrd 279	. . 3 ⊢ (𝜑 → (∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
70		vex 3492	. . . 4 ⊢ 𝑧 ∈ V
71	70, 46	opelco 5896	. . 3 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝐺 ∘ 𝐹) ↔ ∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤))
72		df-mpt 5250	. . . . 5 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑇) = {⟨𝑥, 𝑣⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)}
73	72	eleq2i 2836	. . . 4 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝑥 ∈ 𝐴 ↦ 𝑇) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)})
74		nfv 1913	. . . . . 6 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐴
75	36	nfeq2 2926	. . . . . 6 ⊢ Ⅎ𝑥 𝑣 = ⦋𝑧 / 𝑥⦌𝑇
76	74, 75	nfan 1898	. . . . 5 ⊢ Ⅎ𝑥(𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇)
77		nfv 1913	. . . . 5 ⊢ Ⅎ𝑣(𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)
78		eleq1w 2827	. . . . . 6 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))
79	42	eqeq2d 2751	. . . . . 6 ⊢ (𝑥 = 𝑧 → (𝑣 = 𝑇 ↔ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇))
80	78, 79	anbi12d 631	. . . . 5 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇)))
81		eqeq1 2744	. . . . . 6 ⊢ (𝑣 = 𝑤 → (𝑣 = ⦋𝑧 / 𝑥⦌𝑇 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
82	81	anbi2d 629	. . . . 5 ⊢ (𝑣 = 𝑤 → ((𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
83	76, 77, 70, 46, 80, 82	opelopabf 5564	. . . 4 ⊢ (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)} ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
84	73, 83	bitri 275	. . 3 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝑥 ∈ 𝐴 ↦ 𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
85	69, 71, 84	3bitr4g 314	. 2 ⊢ (𝜑 → (⟨𝑧, 𝑤⟩ ∈ (𝐺 ∘ 𝐹) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑥 ∈ 𝐴 ↦ 𝑇)))
86	1, 2, 85	eqrelrdv 5816	1 ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537  ∃wex 1777   ∈ wcel 2108  Vcvv 3488  ⦋csb 3921  ⟨cop 4654   class class class wbr 5166  {copab 5228   ↦ cmpt 5249  dom cdm 5700   ∘ ccom 5704  Fun wfun 6567  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581

This theorem is referenced by:  fmptcof  7164  cofmpt  7166  fcompt  7167  fcoconst  7168  ofco  7738  ccatco  14884  rlimcn1  15634  rlimdiv  15694  ackbijnn  15876  setcepi  18155  prf1st  18273  prf2nd  18274  hofcllem  18328  prdsidlem  18804  pws0g  18808  mhmvlin  18836  pwsco1mhm  18867  pwsco2mhm  18868  smndex1iidm  18936  smndex2dlinvh  18952  pwsinvg  19093  pwssub  19094  ghmquskerco  19324  galactghm  19446  efginvrel1  19770  frgpup3lem  19819  gsumzf1o  19954  gsumconst  19976  gsummptshft  19978  gsumzmhm  19979  gsummhm2  19981  gsummptmhm  19982  gsumsub  19990  gsum2dlem2  20013  dprdfsub  20065  lmhmvsca  21067  frgpcyg  21615  evpmodpmf1o  21637  psrass1lem  21975  psrlinv  21998  psrcom  22011  evlslem2  22126  psdmplcl  22189  psdmul  22193  coe1fval3  22231  psropprmul  22260  coe1z  22287  coe1mul2  22293  coe1tm  22297  ply1coe  22323  evls1sca  22348  ofco2  22478  mdetleib2  22615  mdetralt  22635  smadiadetlem3  22695  ptrescn  23668  lmcn2  23678  qtopeu  23745  flfcnp2  24036  tgpconncomp  24142  tsmssub  24178  tsmsxplem1  24182  negfcncf  24969  pcopt  25074  pcopt2  25075  pi1xfrcnvlem  25108  ovolctb  25544  ovolfs2  25625  uniioombllem2  25637  ismbf  25682  mbfconst  25687  limccnp2  25947  limcco  25948  dvcof  26006  dvcj  26008  dvfre  26009  dvmptcj  26026  dvmptco  26030  dvcnvlem  26034  dvlip  26052  dvlipcn  26053  itgsubstlem  26109  plyco  26300  dgrcolem1  26333  dgrcolem2  26334  dgrco  26335  plycjlem  26336  taylply2  26427  taylply2OLD  26428  logcn  26707  leibpi  27003  efrlim  27030  efrlimOLD  27031  jensenlem2  27049  amgmlem  27051  ftalem7  27140  dchrisum0  27582  ofcfval4  34069  eulerpartgbij  34337  dstfrvclim1  34442  cvmliftlem6  35258  cvmliftphtlem  35285  cvmlift3lem5  35291  elmsubrn  35496  msubco  35499  circum  35642  mblfinlem2  37618  volsupnfl  37625  itgaddnc  37640  itgmulc2nc  37648  ftc1anclem1  37653  ftc1anclem2  37654  ftc1anclem3  37655  ftc1anclem4  37656  ftc1anclem5  37657  ftc1anclem7  37659  ftc1anclem8  37660  fnopabco  37683  upixp  37689  aks6d1c6lem4  42130  selvvvval  42540  evlselv  42542  mendassa  43151  fsovrfovd  43971  fsovcnvlem  43975  cncfcompt  45804  dvcosax  45847  dirkercncflem4  46027  fourierdlem111  46138  meadjiunlem  46386  meadjiun  46387  fundcmpsurbijinjpreimafv  47281  itcovalpclem2  48405  itcovalt2lem2  48410  amgmwlem  48896  amgmlemALT  48897