Theorem evlf2 18175

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 18174	. . . 4 ⊢ (𝜑 → 𝐸 = ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))⟩)
10		ovex 7389	. . . . . 6 ⊢ (𝐶 Func 𝐷) ∈ V
11	5	fvexi 6841	. . . . . 6 ⊢ 𝐵 ∈ V
12	10, 11	mpoex 8021	. . . . 5 ⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)) ∈ V
13	10, 11	xpex 7696	. . . . . 6 ⊢ ((𝐶 Func 𝐷) × 𝐵) ∈ V
14	13, 13	mpoex 8021	. . . . 5 ⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))) ∈ V
15	12, 14	op2ndd 7942	. . . 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 6842	. . . 4 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → (1st ‘𝑥) ∈ V)
18		simprl 776	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → 𝑥 = ⟨𝐹, 𝑋⟩)
19	18	fveq2d 6831	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → (1st ‘𝑥) = (1st ‘⟨𝐹, 𝑋⟩))
20		evlf2.f	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
21		evlf2.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
22		op1stg 7943	. . . . . . 7 ⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ 𝐵) → (1st ‘⟨𝐹, 𝑋⟩) = 𝐹)
23	20, 21, 22	syl2anc 590	. . . . . 6 ⊢ (𝜑 → (1st ‘⟨𝐹, 𝑋⟩) = 𝐹)
24	23	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → (1st ‘⟨𝐹, 𝑋⟩) = 𝐹)
25	19, 24	eqtrd 2774	. . . 4 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → (1st ‘𝑥) = 𝐹)
26		fvexd 6842	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) ∈ V)
27		simplrr 783	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → 𝑦 = ⟨𝐺, 𝑌⟩)
28	27	fveq2d 6831	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) = (1st ‘⟨𝐺, 𝑌⟩))
29		evlf2.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷))
30		evlf2.y	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
31		op1stg 7943	. . . . . . . 8 ⊢ ((𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ 𝐵) → (1st ‘⟨𝐺, 𝑌⟩) = 𝐺)
32	29, 30, 31	syl2anc 590	. . . . . . 7 ⊢ (𝜑 → (1st ‘⟨𝐺, 𝑌⟩) = 𝐺)
33	32	ad2antrr 732	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → (1st ‘⟨𝐺, 𝑌⟩) = 𝐺)
34	28, 33	eqtrd 2774	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) = 𝐺)
35		simplr 774	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑚 = 𝐹)
36		simpr 485	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑛 = 𝐺)
37	35, 36	oveq12d 7374	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑚𝑁𝑛) = (𝐹𝑁𝐺))
38	18	ad2antrr 732	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑥 = ⟨𝐹, 𝑋⟩)
39	38	fveq2d 6831	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑥) = (2nd ‘⟨𝐹, 𝑋⟩))
40		op2ndg 7944	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ 𝐵) → (2nd ‘⟨𝐹, 𝑋⟩) = 𝑋)
41	20, 21, 40	syl2anc 590	. . . . . . . . 9 ⊢ (𝜑 → (2nd ‘⟨𝐹, 𝑋⟩) = 𝑋)
42	41	ad3antrrr 736	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘⟨𝐹, 𝑋⟩) = 𝑋)
43	39, 42	eqtrd 2774	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑥) = 𝑋)
44	27	adantr 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑦 = ⟨𝐺, 𝑌⟩)
45	44	fveq2d 6831	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑦) = (2nd ‘⟨𝐺, 𝑌⟩))
46		op2ndg 7944	. . . . . . . . . 10 ⊢ ((𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ 𝐵) → (2nd ‘⟨𝐺, 𝑌⟩) = 𝑌)
47	29, 30, 46	syl2anc 590	. . . . . . . . 9 ⊢ (𝜑 → (2nd ‘⟨𝐺, 𝑌⟩) = 𝑌)
48	47	ad3antrrr 736	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘⟨𝐺, 𝑌⟩) = 𝑌)
49	45, 48	eqtrd 2774	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑦) = 𝑌)
50	43, 49	oveq12d 7374	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) = (𝑋𝐻𝑌))
51	35	fveq2d 6831	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (1st ‘𝑚) = (1st ‘𝐹))
52	51, 43	fveq12d 6834	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑚)‘(2nd ‘𝑥)) = ((1st ‘𝐹)‘𝑋))
53	51, 49	fveq12d 6834	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑚)‘(2nd ‘𝑦)) = ((1st ‘𝐹)‘𝑌))
54	52, 53	opeq12d 4812	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ = ⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩)
55	36	fveq2d 6831	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (1st ‘𝑛) = (1st ‘𝐺))
56	55, 49	fveq12d 6834	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑛)‘(2nd ‘𝑦)) = ((1st ‘𝐺)‘𝑌))
57	54, 56	oveq12d 7374	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦))) = (⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌)))
58	49	fveq2d 6831	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑎‘(2nd ‘𝑦)) = (𝑎‘𝑌))
59	35	fveq2d 6831	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑚) = (2nd ‘𝐹))
60	59, 43, 49	oveq123d 7377	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦)) = (𝑋(2nd ‘𝐹)𝑌))
61	60	fveq1d 6829	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔) = ((𝑋(2nd ‘𝐹)𝑌)‘𝑔))
62	57, 58, 61	oveq123d 7377	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)) = ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))
63	37, 50, 62	mpoeq123dv 7431	. . . . 5 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))
64	26, 34, 63	csbied2 3868	. . . 4 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → ⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))
65	17, 25, 64	csbied2 3868	. . 3 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))
66	20, 21	opelxpd 5657	. . 3 ⊢ (𝜑 → ⟨𝐹, 𝑋⟩ ∈ ((𝐶 Func 𝐷) × 𝐵))
67	29, 30	opelxpd 5657	. . 3 ⊢ (𝜑 → ⟨𝐺, 𝑌⟩ ∈ ((𝐶 Func 𝐷) × 𝐵))
68		ovex 7389	. . . . 5 ⊢ (𝐹𝑁𝐺) ∈ V
69		ovex 7389	. . . . 5 ⊢ (𝑋𝐻𝑌) ∈ V
70	68, 69	mpoex 8021	. . . 4 ⊢ (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))) ∈ V
71	70	a1i 11	. . 3 ⊢ (𝜑 → (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))) ∈ V)
72	16, 65, 66, 67, 71	ovmpod 7508	. 2 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐺, 𝑌⟩) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))
73	1, 72	eqtrid 2786	1 ⊢ (𝜑 → 𝐿 = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  Vcvv 3431  ⦋csb 3831  ⟨cop 4561   × cxp 5616  ‘cfv 6485  (class class class)co 7356   ∈ cmpo 7358  1^st c1st 7929  2^nd c2nd 7930  Basecbs 17170  Hom chom 17222  compcco 17223  Catccat 17621   Func cfunc 17812   Nat cnat 17902   eval_F cevlf 18166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932  df-evlf 18170

This theorem is referenced by:  evlf2val  18176  evlfcl  18179