Theorem evlf2 17936

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 17935	. . . 4 ⊢ (𝜑 → 𝐸 = ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))⟩)
10		ovex 7308	. . . . . 6 ⊢ (𝐶 Func 𝐷) ∈ V
11	5	fvexi 6788	. . . . . 6 ⊢ 𝐵 ∈ V
12	10, 11	mpoex 7920	. . . . 5 ⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)) ∈ V
13	10, 11	xpex 7603	. . . . . 6 ⊢ ((𝐶 Func 𝐷) × 𝐵) ∈ V
14	13, 13	mpoex 7920	. . . . 5 ⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))) ∈ V
15	12, 14	op2ndd 7842	. . . 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 6789	. . . 4 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → (1st ‘𝑥) ∈ V)
18		simprl 768	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → 𝑥 = ⟨𝐹, 𝑋⟩)
19	18	fveq2d 6778	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → (1st ‘𝑥) = (1st ‘⟨𝐹, 𝑋⟩))
20		evlf2.f	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
21		evlf2.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
22		op1stg 7843	. . . . . . 7 ⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ 𝐵) → (1st ‘⟨𝐹, 𝑋⟩) = 𝐹)
23	20, 21, 22	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (1st ‘⟨𝐹, 𝑋⟩) = 𝐹)
24	23	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → (1st ‘⟨𝐹, 𝑋⟩) = 𝐹)
25	19, 24	eqtrd 2778	. . . 4 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → (1st ‘𝑥) = 𝐹)
26		fvexd 6789	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) ∈ V)
27		simplrr 775	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → 𝑦 = ⟨𝐺, 𝑌⟩)
28	27	fveq2d 6778	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) = (1st ‘⟨𝐺, 𝑌⟩))
29		evlf2.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷))
30		evlf2.y	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
31		op1stg 7843	. . . . . . . 8 ⊢ ((𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ 𝐵) → (1st ‘⟨𝐺, 𝑌⟩) = 𝐺)
32	29, 30, 31	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (1st ‘⟨𝐺, 𝑌⟩) = 𝐺)
33	32	ad2antrr 723	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → (1st ‘⟨𝐺, 𝑌⟩) = 𝐺)
34	28, 33	eqtrd 2778	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) = 𝐺)
35		simplr 766	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑚 = 𝐹)
36		simpr 485	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑛 = 𝐺)
37	35, 36	oveq12d 7293	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑚𝑁𝑛) = (𝐹𝑁𝐺))
38	18	ad2antrr 723	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑥 = ⟨𝐹, 𝑋⟩)
39	38	fveq2d 6778	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑥) = (2nd ‘⟨𝐹, 𝑋⟩))
40		op2ndg 7844	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ 𝐵) → (2nd ‘⟨𝐹, 𝑋⟩) = 𝑋)
41	20, 21, 40	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (2nd ‘⟨𝐹, 𝑋⟩) = 𝑋)
42	41	ad3antrrr 727	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘⟨𝐹, 𝑋⟩) = 𝑋)
43	39, 42	eqtrd 2778	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑥) = 𝑋)
44	27	adantr 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑦 = ⟨𝐺, 𝑌⟩)
45	44	fveq2d 6778	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑦) = (2nd ‘⟨𝐺, 𝑌⟩))
46		op2ndg 7844	. . . . . . . . . 10 ⊢ ((𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ 𝐵) → (2nd ‘⟨𝐺, 𝑌⟩) = 𝑌)
47	29, 30, 46	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (2nd ‘⟨𝐺, 𝑌⟩) = 𝑌)
48	47	ad3antrrr 727	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘⟨𝐺, 𝑌⟩) = 𝑌)
49	45, 48	eqtrd 2778	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑦) = 𝑌)
50	43, 49	oveq12d 7293	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) = (𝑋𝐻𝑌))
51	35	fveq2d 6778	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (1st ‘𝑚) = (1st ‘𝐹))
52	51, 43	fveq12d 6781	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑚)‘(2nd ‘𝑥)) = ((1st ‘𝐹)‘𝑋))
53	51, 49	fveq12d 6781	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑚)‘(2nd ‘𝑦)) = ((1st ‘𝐹)‘𝑌))
54	52, 53	opeq12d 4812	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ = ⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩)
55	36	fveq2d 6778	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (1st ‘𝑛) = (1st ‘𝐺))
56	55, 49	fveq12d 6781	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑛)‘(2nd ‘𝑦)) = ((1st ‘𝐺)‘𝑌))
57	54, 56	oveq12d 7293	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦))) = (⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌)))
58	49	fveq2d 6778	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑎‘(2nd ‘𝑦)) = (𝑎‘𝑌))
59	35	fveq2d 6778	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑚) = (2nd ‘𝐹))
60	59, 43, 49	oveq123d 7296	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦)) = (𝑋(2nd ‘𝐹)𝑌))
61	60	fveq1d 6776	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔) = ((𝑋(2nd ‘𝐹)𝑌)‘𝑔))
62	57, 58, 61	oveq123d 7296	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)) = ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))
63	37, 50, 62	mpoeq123dv 7350	. . . . 5 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))
64	26, 34, 63	csbied2 3872	. . . 4 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → ⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))
65	17, 25, 64	csbied2 3872	. . 3 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))
66	20, 21	opelxpd 5627	. . 3 ⊢ (𝜑 → ⟨𝐹, 𝑋⟩ ∈ ((𝐶 Func 𝐷) × 𝐵))
67	29, 30	opelxpd 5627	. . 3 ⊢ (𝜑 → ⟨𝐺, 𝑌⟩ ∈ ((𝐶 Func 𝐷) × 𝐵))
68		ovex 7308	. . . . 5 ⊢ (𝐹𝑁𝐺) ∈ V
69		ovex 7308	. . . . 5 ⊢ (𝑋𝐻𝑌) ∈ V
70	68, 69	mpoex 7920	. . . 4 ⊢ (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))) ∈ V
71	70	a1i 11	. . 3 ⊢ (𝜑 → (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))) ∈ V)
72	16, 65, 66, 67, 71	ovmpod 7425	. 2 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐺, 𝑌⟩) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))
73	1, 72	eqtrid 2790	1 ⊢ (𝜑 → 𝐿 = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106  Vcvv 3432  ⦋csb 3832  ⟨cop 4567   × cxp 5587  ‘cfv 6433  (class class class)co 7275   ∈ cmpo 7277  1^st c1st 7829  2^nd c2nd 7830  Basecbs 16912  Hom chom 16973  compcco 16974  Catccat 17373   Func cfunc 17569   Nat cnat 17657   eval_F cevlf 17927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-1st 7831  df-2nd 7832  df-evlf 17931

This theorem is referenced by:  evlf2val  17937  evlfcl  17940