Theorem fmptco 7126

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 6111	. 2 ⊢ Rel (𝐺 ∘ 𝐹)
2		mptrel 5813	. 2 ⊢ Rel (𝑥 ∈ 𝐴 ↦ 𝑇)
3		fmptco.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅))
4		fmptco.1	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝐵)
5	3, 4	fmpt3d 7112	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
6	5	ffund 6711	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝐹)
7		funbrfv 6930	. . . . . . . . . . 11 ⊢ (Fun 𝐹 → (𝑧𝐹𝑢 → (𝐹‘𝑧) = 𝑢))
8	7	imp 411	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ 𝑧𝐹𝑢) → (𝐹‘𝑧) = 𝑢)
9	6, 8	sylan 591	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → (𝐹‘𝑧) = 𝑢)
10	9	eqcomd 2775	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → 𝑢 = (𝐹‘𝑧))
11	10	a1d 26	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → (𝑢𝐺𝑤 → 𝑢 = (𝐹‘𝑧)))
12	11	expimpd 458	. . . . . 6 ⊢ (𝜑 → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) → 𝑢 = (𝐹‘𝑧)))
13	12	pm4.71rd 571	. . . . 5 ⊢ (𝜑 → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤))))
14	13	exbidv 1948	. . . 4 ⊢ (𝜑 → (∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ ∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤))))
15		fvex 6895	. . . . . 6 ⊢ (𝐹‘𝑧) ∈ V
16		breq2 5117	. . . . . . 7 ⊢ (𝑢 = (𝐹‘𝑧) → (𝑧𝐹𝑢 ↔ 𝑧𝐹(𝐹‘𝑧)))
17		breq1 5116	. . . . . . 7 ⊢ (𝑢 = (𝐹‘𝑧) → (𝑢𝐺𝑤 ↔ (𝐹‘𝑧)𝐺𝑤))
18	16, 17	anbi12d 643	. . . . . 6 ⊢ (𝑢 = (𝐹‘𝑧) → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤)))
19	15, 18	ceqsexv 3511	. . . . 5 ⊢ (∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) ↔ (𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤))
20		funfvbrb 7047	. . . . . . . . 9 ⊢ (Fun 𝐹 → (𝑧 ∈ dom 𝐹 ↔ 𝑧𝐹(𝐹‘𝑧)))
21	6, 20	syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝑧 ∈ dom 𝐹 ↔ 𝑧𝐹(𝐹‘𝑧)))
22	5	fdmd 6717	. . . . . . . . 9 ⊢ (𝜑 → dom 𝐹 = 𝐴)
23	22	eleq2d 2855	. . . . . . . 8 ⊢ (𝜑 → (𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝐴))
24	21, 23	bitr3d 284	. . . . . . 7 ⊢ (𝜑 → (𝑧𝐹(𝐹‘𝑧) ↔ 𝑧 ∈ 𝐴))
25	3	fveq1d 6884	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝑧) = ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧))
26		fmptco.3	. . . . . . . 8 ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆))
27		eqidd 2770	. . . . . . . 8 ⊢ (𝜑 → 𝑤 = 𝑤)
28	25, 26, 27	breq123d 5127	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘𝑧)𝐺𝑤 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤))
29	24, 28	anbi12d 643	. . . . . 6 ⊢ (𝜑 → ((𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤)))
30		nfcv 2931	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑧
31		nfv 1941	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝜑
32		nffvmpt1 6893	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)
33		nfcv 2931	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐵 ↦ 𝑆)
34		nfcv 2931	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝑤
35	32, 33, 34	nfbr 5162	. . . . . . . . . . 11 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤
36		nfcsb1v 3885	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝑇
37	36	nfeq2 2948	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑤 = ⦋𝑧 / 𝑥⦌𝑇
38	35, 37	nfbi 1930	. . . . . . . . . 10 ⊢ Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)
39	31, 38	nfim 1923	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
40		fveq2 6882	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧))
41	40	breq1d 5123	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤))
42		csbeq1a 3875	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → 𝑇 = ⦋𝑧 / 𝑥⦌𝑇)
43	42	eqeq2d 2780	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝑤 = 𝑇 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
44	41, 43	bibi12d 348	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → ((((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇) ↔ (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
45	44	imbi2d 343	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇)) ↔ (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))))
46		vex 3467	. . . . . . . . . . . 12 ⊢ 𝑤 ∈ V
47		simpl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → 𝑦 = 𝑅)
48	47	eleq1d 2854	. . . . . . . . . . . . . 14 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → (𝑦 ∈ 𝐵 ↔ 𝑅 ∈ 𝐵))
49		id 23	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑤 → 𝑢 = 𝑤)
50		fmptco.4	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇)
51	49, 50	eqeqan12rd 2784	. . . . . . . . . . . . . 14 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → (𝑢 = 𝑆 ↔ 𝑤 = 𝑇))
52	48, 51	anbi12d 643	. . . . . . . . . . . . 13 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → ((𝑦 ∈ 𝐵 ∧ 𝑢 = 𝑆) ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
53		df-mpt 5197	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐵 ↦ 𝑆) = {⟨𝑦, 𝑢⟩ ∣ (𝑦 ∈ 𝐵 ∧ 𝑢 = 𝑆)}
54	52, 53	brabga 5519	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ 𝐵 ∧ 𝑤 ∈ V) → (𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
55	4, 46, 54	sylancl 597	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
56		id 23	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
57		eqid 2769	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅)
58	57	fvmpt2 7002	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑅 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅)
59	56, 4, 58	syl2an2 698	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅)
60	59	breq1d 5123	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤))
61	4	biantrurd 541	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑤 = 𝑇 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
62	55, 60, 61	3bitr4d 314	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇))
63	62	expcom 418	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇)))
64	30, 39, 45, 63	vtoclgaf 3549	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
65	64	impcom 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
66	65	pm5.32da 589	. . . . . 6 ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
67	29, 66	bitrd 282	. . . . 5 ⊢ (𝜑 → ((𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
68	19, 67	bitrid 286	. . . 4 ⊢ (𝜑 → (∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
69	14, 68	bitrd 282	. . 3 ⊢ (𝜑 → (∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
70		vex 3467	. . . 4 ⊢ 𝑧 ∈ V
71	70, 46	opelco 5858	. . 3 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝐺 ∘ 𝐹) ↔ ∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤))
72		df-mpt 5197	. . . . 5 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑇) = {⟨𝑥, 𝑣⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)}
73	72	eleq2i 2861	. . . 4 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝑥 ∈ 𝐴 ↦ 𝑇) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)})
74		nfv 1941	. . . . . 6 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐴
75	36	nfeq2 2948	. . . . . 6 ⊢ Ⅎ𝑥 𝑣 = ⦋𝑧 / 𝑥⦌𝑇
76	74, 75	nfan 1926	. . . . 5 ⊢ Ⅎ𝑥(𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇)
77		nfv 1941	. . . . 5 ⊢ Ⅎ𝑣(𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)
78		eleq1w 2852	. . . . . 6 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))
79	42	eqeq2d 2780	. . . . . 6 ⊢ (𝑥 = 𝑧 → (𝑣 = 𝑇 ↔ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇))
80	78, 79	anbi12d 643	. . . . 5 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇)))
81		eqeq1 2773	. . . . . 6 ⊢ (𝑣 = 𝑤 → (𝑣 = ⦋𝑧 / 𝑥⦌𝑇 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
82	81	anbi2d 641	. . . . 5 ⊢ (𝑣 = 𝑤 → ((𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
83	76, 77, 70, 46, 80, 82	opelopabf 5531	. . . 4 ⊢ (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)} ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
84	73, 83	bitri 278	. . 3 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝑥 ∈ 𝐴 ↦ 𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
85	69, 71, 84	3bitr4g 317	. 2 ⊢ (𝜑 → (⟨𝑧, 𝑤⟩ ∈ (𝐺 ∘ 𝐹) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑥 ∈ 𝐴 ↦ 𝑇)))
86	1, 2, 85	eqrelrdv 5779	1 ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567  ∃wex 1806   ∈ wcel 2149  Vcvv 3463  ⦋csb 3861  ⟨cop 4600   class class class wbr 5113  {copab 5177   ↦ cmpt 5196  dom cdm 5662   ∘ ccom 5666  Fun wfun 6531  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545

This theorem is referenced by:  fmptcof  7127  cofmpt  7129  fcompt  7130  fcoconst  7131  ofco  7700  ccatco  14871  rlimcn1  15638  rlimdiv  15696  ackbijnn  15881  setcepi  18144  prf1st  18259  prf2nd  18260  hofcllem  18313  prdsidlem  18826  pws0g  18830  mhmvlin  18858  pwsco1mhm  18890  pwsco2mhm  18891  smndex1iidm  18959  smndex2dlinvh  18978  pwsinvg  19118  pwssub  19119  ghmquskerco  19353  galactghm  19473  efginvrel1  19797  frgpup3lem  19846  gsumzf1o  19981  gsumconst  20003  gsummptshft  20005  gsumzmhm  20006  gsummhm2  20008  gsummptmhm  20009  gsumsub  20017  gsum2dlem2  20040  dprdfsub  20092  lmhmvsca  21143  frgpcyg  21691  evpmodpmf1o  21714  psrass1lem  22051  psrlinv  22073  psrcom  22085  evlslem2  22198  selvvvval  22261  psdmplcl  22293  psdmul  22297  coe1fval3  22336  psropprmul  22365  coe1z  22392  coe1mul2  22398  coe1tm  22402  ply1coe  22426  evls1sca  22451  ofco2  22576  mdetleib2  22713  mdetralt  22733  smadiadetlem3  22793  ptrescn  23764  lmcn2  23774  qtopeu  23841  flfcnp2  24132  tgpconncomp  24238  tsmssub  24274  tsmsxplem1  24278  negfcncf  25050  pcopt  25149  pcopt2  25150  pi1xfrcnvlem  25183  ovolctb  25617  ovolfs2  25698  uniioombllem2  25710  ismbf  25755  mbfconst  25760  limccnp2  26019  limcco  26020  dvcof  26075  dvcj  26077  dvfre  26078  dvmptcj  26095  dvmptco  26099  dvcnvlem  26103  dvlip  26120  dvlipcn  26121  itgsubstlem  26175  plyco  26366  dgrcolem1  26398  dgrcolem2  26399  dgrco  26400  plycjlem  26401  taylply2  26496  logcn  26777  leibpi  27072  efrlim  27099  jensenlem2  27117  amgmlem  27119  ftalem7  27208  dchrisum0  27649  gsumwrd2dccat  33338  mplvrpmfgalem  33878  psrmonprod  33886  esplyfval0  33898  esplyfvaln  33908  ofcfval4  34439  eulerpartgbij  34706  dstfrvclim1  34812  cvmliftlem6  35680  cvmliftphtlem  35707  cvmlift3lem5  35713  elmsubrn  35918  msubco  35921  circum  36064  mblfinlem2  38196  volsupnfl  38203  itgaddnc  38218  itgmulc2nc  38226  ftc1anclem1  38231  ftc1anclem2  38232  ftc1anclem3  38233  ftc1anclem4  38234  ftc1anclem5  38235  ftc1anclem7  38237  ftc1anclem8  38238  fnopabco  38261  upixp  38267  aks6d1c6lem4  42829  evlselv  43212  mendassa  43808  fsovrfovd  44626  fsovcnvlem  44630  cncfcompt  46488  dvcosax  46531  dirkercncflem4  46711  fourierdlem111  46822  meadjiunlem  47070  meadjiun  47071  fundcmpsurbijinjpreimafv  48044  itcovalpclem2  49335  itcovalt2lem2  49340  amgmwlem  50475  amgmlemALT  50476