Theorem evlf2 18210

Description: Value of the evaluation functor at a morphism. (Contributed by Mario Carneiro, 12-Jan-2017.)

Hypotheses

Ref	Expression
evlfval.e	⊢ 𝐸 = (𝐶 evalF 𝐷)
evlfval.c	⊢ (𝜑 → 𝐶 ∈ Cat)
evlfval.d	⊢ (𝜑 → 𝐷 ∈ Cat)
evlfval.b	⊢ 𝐵 = (Base‘𝐶)
evlfval.h	⊢ 𝐻 = (Hom ‘𝐶)
evlfval.o	⊢ · = (comp‘𝐷)
evlfval.n	⊢ 𝑁 = (𝐶 Nat 𝐷)
evlf2.f	⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
evlf2.g	⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷))
evlf2.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
evlf2.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)
evlf2.l	⊢ 𝐿 = (⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐺, 𝑌⟩)

Assertion

Ref	Expression
evlf2	⊢ (𝜑 → 𝐿 = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))

Distinct variable groups:   𝑔,𝑎,𝐶   𝐷,𝑎,𝑔   𝑔,𝐻   𝐹,𝑎,𝑔   𝑁,𝑎,𝑔   𝐺,𝑎,𝑔   𝜑,𝑎,𝑔   · ,𝑎,𝑔   𝑋,𝑎,𝑔   𝑌,𝑎,𝑔

Allowed substitution hints:   𝐵(𝑔,𝑎)   𝐸(𝑔,𝑎)   𝐻(𝑎)   𝐿(𝑔,𝑎)

Proof of Theorem evlf2

Dummy variables 𝑓 𝑚 𝑛 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		evlf2.l	. 2 ⊢ 𝐿 = (⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐺, 𝑌⟩)
2		evlfval.e	. . . . 5 ⊢ 𝐸 = (𝐶 evalF 𝐷)
3		evlfval.c	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ Cat)
4		evlfval.d	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ Cat)
5		evlfval.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐶)
6		evlfval.h	. . . . 5 ⊢ 𝐻 = (Hom ‘𝐶)
7		evlfval.o	. . . . 5 ⊢ · = (comp‘𝐷)
8		evlfval.n	. . . . 5 ⊢ 𝑁 = (𝐶 Nat 𝐷)
9	2, 3, 4, 5, 6, 7, 8	evlfval 18209	. . . 4 ⊢ (𝜑 → 𝐸 = ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))⟩)
10		ovex 7453	. . . . . 6 ⊢ (𝐶 Func 𝐷) ∈ V
11	5	fvexi 6911	. . . . . 6 ⊢ 𝐵 ∈ V
12	10, 11	mpoex 8084	. . . . 5 ⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)) ∈ V
13	10, 11	xpex 7755	. . . . . 6 ⊢ ((𝐶 Func 𝐷) × 𝐵) ∈ V
14	13, 13	mpoex 8084	. . . . 5 ⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))) ∈ V
15	12, 14	op2ndd 8004	. . . 4 ⊢ (𝐸 = ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))⟩ → (2nd ‘𝐸) = (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))))
16	9, 15	syl 17	. . 3 ⊢ (𝜑 → (2nd ‘𝐸) = (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))))
17		fvexd 6912	. . . 4 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → (1st ‘𝑥) ∈ V)
18		simprl 770	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → 𝑥 = ⟨𝐹, 𝑋⟩)
19	18	fveq2d 6901	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → (1st ‘𝑥) = (1st ‘⟨𝐹, 𝑋⟩))
20		evlf2.f	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
21		evlf2.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
22		op1stg 8005	. . . . . . 7 ⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ 𝐵) → (1st ‘⟨𝐹, 𝑋⟩) = 𝐹)
23	20, 21, 22	syl2anc 583	. . . . . 6 ⊢ (𝜑 → (1st ‘⟨𝐹, 𝑋⟩) = 𝐹)
24	23	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → (1st ‘⟨𝐹, 𝑋⟩) = 𝐹)
25	19, 24	eqtrd 2768	. . . 4 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → (1st ‘𝑥) = 𝐹)
26		fvexd 6912	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) ∈ V)
27		simplrr 777	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → 𝑦 = ⟨𝐺, 𝑌⟩)
28	27	fveq2d 6901	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) = (1st ‘⟨𝐺, 𝑌⟩))
29		evlf2.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷))
30		evlf2.y	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
31		op1stg 8005	. . . . . . . 8 ⊢ ((𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ 𝐵) → (1st ‘⟨𝐺, 𝑌⟩) = 𝐺)
32	29, 30, 31	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → (1st ‘⟨𝐺, 𝑌⟩) = 𝐺)
33	32	ad2antrr 725	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → (1st ‘⟨𝐺, 𝑌⟩) = 𝐺)
34	28, 33	eqtrd 2768	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) = 𝐺)
35		simplr 768	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑚 = 𝐹)
36		simpr 484	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑛 = 𝐺)
37	35, 36	oveq12d 7438	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑚𝑁𝑛) = (𝐹𝑁𝐺))
38	18	ad2antrr 725	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑥 = ⟨𝐹, 𝑋⟩)
39	38	fveq2d 6901	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑥) = (2nd ‘⟨𝐹, 𝑋⟩))
40		op2ndg 8006	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ 𝐵) → (2nd ‘⟨𝐹, 𝑋⟩) = 𝑋)
41	20, 21, 40	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → (2nd ‘⟨𝐹, 𝑋⟩) = 𝑋)
42	41	ad3antrrr 729	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘⟨𝐹, 𝑋⟩) = 𝑋)
43	39, 42	eqtrd 2768	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑥) = 𝑋)
44	27	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑦 = ⟨𝐺, 𝑌⟩)
45	44	fveq2d 6901	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑦) = (2nd ‘⟨𝐺, 𝑌⟩))
46		op2ndg 8006	. . . . . . . . . 10 ⊢ ((𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ 𝐵) → (2nd ‘⟨𝐺, 𝑌⟩) = 𝑌)
47	29, 30, 46	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → (2nd ‘⟨𝐺, 𝑌⟩) = 𝑌)
48	47	ad3antrrr 729	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘⟨𝐺, 𝑌⟩) = 𝑌)
49	45, 48	eqtrd 2768	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑦) = 𝑌)
50	43, 49	oveq12d 7438	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) = (𝑋𝐻𝑌))
51	35	fveq2d 6901	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (1st ‘𝑚) = (1st ‘𝐹))
52	51, 43	fveq12d 6904	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑚)‘(2nd ‘𝑥)) = ((1st ‘𝐹)‘𝑋))
53	51, 49	fveq12d 6904	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑚)‘(2nd ‘𝑦)) = ((1st ‘𝐹)‘𝑌))
54	52, 53	opeq12d 4882	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ = ⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩)
55	36	fveq2d 6901	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (1st ‘𝑛) = (1st ‘𝐺))
56	55, 49	fveq12d 6904	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑛)‘(2nd ‘𝑦)) = ((1st ‘𝐺)‘𝑌))
57	54, 56	oveq12d 7438	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦))) = (⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌)))
58	49	fveq2d 6901	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑎‘(2nd ‘𝑦)) = (𝑎‘𝑌))
59	35	fveq2d 6901	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑚) = (2nd ‘𝐹))
60	59, 43, 49	oveq123d 7441	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦)) = (𝑋(2nd ‘𝐹)𝑌))
61	60	fveq1d 6899	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔) = ((𝑋(2nd ‘𝐹)𝑌)‘𝑔))
62	57, 58, 61	oveq123d 7441	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)) = ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))
63	37, 50, 62	mpoeq123dv 7495	. . . . 5 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))
64	26, 34, 63	csbied2 3932	. . . 4 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → ⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))
65	17, 25, 64	csbied2 3932	. . 3 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))
66	20, 21	opelxpd 5717	. . 3 ⊢ (𝜑 → ⟨𝐹, 𝑋⟩ ∈ ((𝐶 Func 𝐷) × 𝐵))
67	29, 30	opelxpd 5717	. . 3 ⊢ (𝜑 → ⟨𝐺, 𝑌⟩ ∈ ((𝐶 Func 𝐷) × 𝐵))
68		ovex 7453	. . . . 5 ⊢ (𝐹𝑁𝐺) ∈ V
69		ovex 7453	. . . . 5 ⊢ (𝑋𝐻𝑌) ∈ V
70	68, 69	mpoex 8084	. . . 4 ⊢ (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))) ∈ V
71	70	a1i 11	. . 3 ⊢ (𝜑 → (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))) ∈ V)
72	16, 65, 66, 67, 71	ovmpod 7573	. 2 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐺, 𝑌⟩) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))
73	1, 72	eqtrid 2780	1 ⊢ (𝜑 → 𝐿 = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1534   ∈ wcel 2099  Vcvv 3471  ⦋csb 3892  ⟨cop 4635   × cxp 5676  ‘cfv 6548  (class class class)co 7420   ∈ cmpo 7422  1^st c1st 7991  2^nd c2nd 7992  Basecbs 17180  Hom chom 17244  compcco 17245  Catccat 17644   Func cfunc 17840   Nat cnat 17931   eval_F cevlf 18201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-ov 7423  df-oprab 7424  df-mpo 7425  df-1st 7993  df-2nd 7994  df-evlf 18205

This theorem is referenced by:  evlf2val  18211  evlfcl  18214