Theorem fmptco 7135

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 6106	. 2 ⊢ Rel (𝐺 ∘ 𝐹)
2		mptrel 5804	. 2 ⊢ Rel (𝑥 ∈ 𝐴 ↦ 𝑇)
3		fmptco.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅))
4		fmptco.1	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝐵)
5	3, 4	fmpt3d 7121	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
6	5	ffund 6719	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝐹)
7		funbrfv 6938	. . . . . . . . . . 11 ⊢ (Fun 𝐹 → (𝑧𝐹𝑢 → (𝐹‘𝑧) = 𝑢))
8	7	imp 412	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ 𝑧𝐹𝑢) → (𝐹‘𝑧) = 𝑢)
9	6, 8	sylan 592	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → (𝐹‘𝑧) = 𝑢)
10	9	eqcomd 2766	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → 𝑢 = (𝐹‘𝑧))
11	10	a1d 26	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → (𝑢𝐺𝑤 → 𝑢 = (𝐹‘𝑧)))
12	11	expimpd 459	. . . . . 6 ⊢ (𝜑 → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) → 𝑢 = (𝐹‘𝑧)))
13	12	pm4.71rd 572	. . . . 5 ⊢ (𝜑 → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤))))
14	13	exbidv 1953	. . . 4 ⊢ (𝜑 → (∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ ∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤))))
15		fvex 6903	. . . . . 6 ⊢ (𝐹‘𝑧) ∈ V
16		breq2 5106	. . . . . . 7 ⊢ (𝑢 = (𝐹‘𝑧) → (𝑧𝐹𝑢 ↔ 𝑧𝐹(𝐹‘𝑧)))
17		breq1 5105	. . . . . . 7 ⊢ (𝑢 = (𝐹‘𝑧) → (𝑢𝐺𝑤 ↔ (𝐹‘𝑧)𝐺𝑤))
18	16, 17	anbi12d 644	. . . . . 6 ⊢ (𝑢 = (𝐹‘𝑧) → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤)))
19	15, 18	ceqsexv 3498	. . . . 5 ⊢ (∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) ↔ (𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤))
20		funfvbrb 7055	. . . . . . . . 9 ⊢ (Fun 𝐹 → (𝑧 ∈ dom 𝐹 ↔ 𝑧𝐹(𝐹‘𝑧)))
21	6, 20	syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝑧 ∈ dom 𝐹 ↔ 𝑧𝐹(𝐹‘𝑧)))
22	5	fdmd 6725	. . . . . . . . 9 ⊢ (𝜑 → dom 𝐹 = 𝐴)
23	22	eleq2d 2846	. . . . . . . 8 ⊢ (𝜑 → (𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝐴))
24	21, 23	bitr3d 284	. . . . . . 7 ⊢ (𝜑 → (𝑧𝐹(𝐹‘𝑧) ↔ 𝑧 ∈ 𝐴))
25	3	fveq1d 6892	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝑧) = ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧))
26		fmptco.3	. . . . . . . 8 ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆))
27		eqidd 2761	. . . . . . . 8 ⊢ (𝜑 → 𝑤 = 𝑤)
28	25, 26, 27	breq123d 5116	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘𝑧)𝐺𝑤 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤))
29	24, 28	anbi12d 644	. . . . . 6 ⊢ (𝜑 → ((𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤)))
30		nfcv 2922	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑧
31		nfv 1946	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝜑
32		nffvmpt1 6901	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)
33		nfcv 2922	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐵 ↦ 𝑆)
34		nfcv 2922	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝑤
35	32, 33, 34	nfbr 5151	. . . . . . . . . . 11 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤
36		nfcsb1v 3871	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝑇
37	36	nfeq2 2939	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑤 = ⦋𝑧 / 𝑥⦌𝑇
38	35, 37	nfbi 1935	. . . . . . . . . 10 ⊢ Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)
39	31, 38	nfim 1928	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
40		fveq2 6890	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧))
41	40	breq1d 5112	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤))
42		csbeq1a 3861	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → 𝑇 = ⦋𝑧 / 𝑥⦌𝑇)
43	42	eqeq2d 2771	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝑤 = 𝑇 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
44	41, 43	bibi12d 348	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → ((((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇) ↔ (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
45	44	imbi2d 343	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇)) ↔ (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))))
46		vex 3454	. . . . . . . . . . . 12 ⊢ 𝑤 ∈ V
47		simpl 488	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → 𝑦 = 𝑅)
48	47	eleq1d 2845	. . . . . . . . . . . . . 14 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → (𝑦 ∈ 𝐵 ↔ 𝑅 ∈ 𝐵))
49		id 23	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑤 → 𝑢 = 𝑤)
50		fmptco.4	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇)
51	49, 50	eqeqan12rd 2775	. . . . . . . . . . . . . 14 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → (𝑢 = 𝑆 ↔ 𝑤 = 𝑇))
52	48, 51	anbi12d 644	. . . . . . . . . . . . 13 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → ((𝑦 ∈ 𝐵 ∧ 𝑢 = 𝑆) ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
53		df-mpt 5186	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐵 ↦ 𝑆) = {⟨𝑦, 𝑢⟩ ∣ (𝑦 ∈ 𝐵 ∧ 𝑢 = 𝑆)}
54	52, 53	brabga 5508	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ 𝐵 ∧ 𝑤 ∈ V) → (𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
55	4, 46, 54	sylancl 598	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
56		id 23	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
57		eqid 2760	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅)
58	57	fvmpt2 7010	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑅 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅)
59	56, 4, 58	syl2an2 699	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅)
60	59	breq1d 5112	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤))
61	4	biantrurd 542	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑤 = 𝑇 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
62	55, 60, 61	3bitr4d 314	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇))
63	62	expcom 419	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇)))
64	30, 39, 45, 63	vtoclgaf 3535	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
65	64	impcom 413	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
66	65	pm5.32da 590	. . . . . 6 ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
67	29, 66	bitrd 282	. . . . 5 ⊢ (𝜑 → ((𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
68	19, 67	bitrid 286	. . . 4 ⊢ (𝜑 → (∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
69	14, 68	bitrd 282	. . 3 ⊢ (𝜑 → (∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
70		vex 3454	. . . 4 ⊢ 𝑧 ∈ V
71	70, 46	opelco 5850	. . 3 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝐺 ∘ 𝐹) ↔ ∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤))
72		df-mpt 5186	. . . . 5 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑇) = {⟨𝑥, 𝑣⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)}
73	72	eleq2i 2852	. . . 4 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝑥 ∈ 𝐴 ↦ 𝑇) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)})
74		nfv 1946	. . . . . 6 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐴
75	36	nfeq2 2939	. . . . . 6 ⊢ Ⅎ𝑥 𝑣 = ⦋𝑧 / 𝑥⦌𝑇
76	74, 75	nfan 1931	. . . . 5 ⊢ Ⅎ𝑥(𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇)
77		nfv 1946	. . . . 5 ⊢ Ⅎ𝑣(𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)
78		eleq1w 2843	. . . . . 6 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))
79	42	eqeq2d 2771	. . . . . 6 ⊢ (𝑥 = 𝑧 → (𝑣 = 𝑇 ↔ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇))
80	78, 79	anbi12d 644	. . . . 5 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇)))
81		eqeq1 2764	. . . . . 6 ⊢ (𝑣 = 𝑤 → (𝑣 = ⦋𝑧 / 𝑥⦌𝑇 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
82	81	anbi2d 642	. . . . 5 ⊢ (𝑣 = 𝑤 → ((𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
83	76, 77, 70, 46, 80, 82	opelopabf 5520	. . . 4 ⊢ (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)} ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
84	73, 83	bitri 278	. . 3 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝑥 ∈ 𝐴 ↦ 𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
85	69, 71, 84	3bitr4g 317	. 2 ⊢ (𝜑 → (⟨𝑧, 𝑤⟩ ∈ (𝐺 ∘ 𝐹) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑥 ∈ 𝐴 ↦ 𝑇)))
86	1, 2, 85	eqrelrdv 5769	1 ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2144  Vcvv 3450  ⦋csb 3847  ⟨cop 4834   class class class wbr 5102  {copab 5166   ↦ cmpt 5185  dom cdm 5651   ∘ ccom 5655  Fun wfun 6537  ‘cfv 6543

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551

This theorem is used by:  fmptcof  7136  cofmpt  7138  fcompt  7139  fcoconst  7140  ofco  7722  ccatco  14994  rlimcn1  15764  rlimdiv  15822  ackbijnn  16006  setcepi  18272  prf1st  18387  prf2nd  18388  hofcllem  18441  prdsidlem  18972  pws0g  18976  mhmvlin  19005  pwsco1mhm  19037  pwsco2mhm  19038  smndex1iidm  19106  smndex2dlinvh  19125  pwsinvg  19272  pwssub  19273  ghmquskerco  19507  galactghm  19627  efginvrel1  19951  frgpup3lem  20000  gsumzf1o  20135  gsumconst  20157  gsummptshft  20159  gsumzmhm  20160  gsummhm2  20162  gsummptmhm  20163  gsumsub  20171  gsum2dlem2  20194  dprdfsub  20246  lmhmvsca  21329  frgpcyg  21888  evpmodpmf1o  21911  psrass1lem  22250  psrlinv  22272  psrcom  22284  evlslem2  22397  selvvvval  22460  psdmplcl  22492  psdmul  22496  coe1fval3  22535  psropprmul  22564  coe1z  22591  coe1mul2  22597  coe1tm  22601  ply1coe  22625  evls1sca  22650  ofco2  22775  mdetleib2  22912  mdetralt  22932  smadiadetlem3  22992  ptrescn  23967  lmcn2  23977  qtopeu  24044  flfcnp2  24335  tgpconncomp  24441  tsmssub  24477  tsmsxplem1  24481  negfcncf  25253  pcopt  25352  pcopt2  25353  pi1xfrcnvlem  25386  ovolctb  25820  ovolfs2  25901  uniioombllem2  25913  ismbf  25958  mbfconst  25963  limccnp2  26221  limcco  26222  dvcof  26277  dvcj  26279  dvfre  26280  dvmptcj  26297  dvmptco  26301  dvcnvlem  26305  dvlip  26322  dvlipcn  26323  itgsubstlem  26377  plyco  26569  dgrcolem1  26601  dgrcolem2  26602  dgrco  26603  plycjlem  26604  taylply2  26704  logcn  26984  leibpi  27279  efrlim  27306  jensenlem2  27324  amgmlem  27326  ftalem7  27415  dchrisum0  27856  gsumwrd2dccat  33689  mplvrpmfgalem  34226  psrmonprod  34234  esplyfval0  34246  esplyfvaln  34256  ofcfval4  34787  eulerpartgbij  35054  dstfrvclim1  35160  cvmliftlem6  36145  cvmliftphtlem  36172  cvmlift3lem5  36178  elmsubrn  36383  msubco  36386  circum  36529  mblfinlem2  38685  volsupnfl  38692  itgaddnc  38707  itgmulc2nc  38715  ftc1anclem1  38720  ftc1anclem2  38721  ftc1anclem3  38722  ftc1anclem4  38723  ftc1anclem5  38724  ftc1anclem7  38726  ftc1anclem8  38727  fnopabco  38766  upixp  38772  aks6d1c6lem4  43332  evlselv  43726  mendassa  44301  fsovrfovd  45118  fsovcnvlem  45122  cncfcompt  47001  dvcosax  47044  dirkercncflem4  47224  fourierdlem111  47335  meadjiunlem  47583  meadjiun  47584  fundcmpsurbijinjpreimafv  48597  itcovalpclem2  49891  itcovalt2lem2  49896  amgmwlem  51170  amgmlemALT  51171