Theorem evlf2 17460

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 17459	. . . 4 ⊢ (𝜑 → 𝐸 = ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))⟩)
10		ovex 7168	. . . . . 6 ⊢ (𝐶 Func 𝐷) ∈ V
11	5	fvexi 6659	. . . . . 6 ⊢ 𝐵 ∈ V
12	10, 11	mpoex 7760	. . . . 5 ⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)) ∈ V
13	10, 11	xpex 7456	. . . . . 6 ⊢ ((𝐶 Func 𝐷) × 𝐵) ∈ V
14	13, 13	mpoex 7760	. . . . 5 ⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))) ∈ V
15	12, 14	op2ndd 7682	. . . 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 6660	. . . 4 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → (1st ‘𝑥) ∈ V)
18		simprl 770	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → 𝑥 = ⟨𝐹, 𝑋⟩)
19	18	fveq2d 6649	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → (1st ‘𝑥) = (1st ‘⟨𝐹, 𝑋⟩))
20		evlf2.f	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
21		evlf2.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
22		op1stg 7683	. . . . . . 7 ⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ 𝐵) → (1st ‘⟨𝐹, 𝑋⟩) = 𝐹)
23	20, 21, 22	syl2anc 587	. . . . . 6 ⊢ (𝜑 → (1st ‘⟨𝐹, 𝑋⟩) = 𝐹)
24	23	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → (1st ‘⟨𝐹, 𝑋⟩) = 𝐹)
25	19, 24	eqtrd 2833	. . . 4 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → (1st ‘𝑥) = 𝐹)
26		fvexd 6660	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) ∈ V)
27		simplrr 777	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → 𝑦 = ⟨𝐺, 𝑌⟩)
28	27	fveq2d 6649	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) = (1st ‘⟨𝐺, 𝑌⟩))
29		evlf2.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷))
30		evlf2.y	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
31		op1stg 7683	. . . . . . . 8 ⊢ ((𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ 𝐵) → (1st ‘⟨𝐺, 𝑌⟩) = 𝐺)
32	29, 30, 31	syl2anc 587	. . . . . . 7 ⊢ (𝜑 → (1st ‘⟨𝐺, 𝑌⟩) = 𝐺)
33	32	ad2antrr 725	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → (1st ‘⟨𝐺, 𝑌⟩) = 𝐺)
34	28, 33	eqtrd 2833	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) = 𝐺)
35		simplr 768	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑚 = 𝐹)
36		simpr 488	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑛 = 𝐺)
37	35, 36	oveq12d 7153	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑚𝑁𝑛) = (𝐹𝑁𝐺))
38	18	ad2antrr 725	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑥 = ⟨𝐹, 𝑋⟩)
39	38	fveq2d 6649	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑥) = (2nd ‘⟨𝐹, 𝑋⟩))
40		op2ndg 7684	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ 𝐵) → (2nd ‘⟨𝐹, 𝑋⟩) = 𝑋)
41	20, 21, 40	syl2anc 587	. . . . . . . . 9 ⊢ (𝜑 → (2nd ‘⟨𝐹, 𝑋⟩) = 𝑋)
42	41	ad3antrrr 729	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘⟨𝐹, 𝑋⟩) = 𝑋)
43	39, 42	eqtrd 2833	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑥) = 𝑋)
44	27	adantr 484	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑦 = ⟨𝐺, 𝑌⟩)
45	44	fveq2d 6649	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑦) = (2nd ‘⟨𝐺, 𝑌⟩))
46		op2ndg 7684	. . . . . . . . . 10 ⊢ ((𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ 𝐵) → (2nd ‘⟨𝐺, 𝑌⟩) = 𝑌)
47	29, 30, 46	syl2anc 587	. . . . . . . . 9 ⊢ (𝜑 → (2nd ‘⟨𝐺, 𝑌⟩) = 𝑌)
48	47	ad3antrrr 729	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘⟨𝐺, 𝑌⟩) = 𝑌)
49	45, 48	eqtrd 2833	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑦) = 𝑌)
50	43, 49	oveq12d 7153	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) = (𝑋𝐻𝑌))
51	35	fveq2d 6649	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (1st ‘𝑚) = (1st ‘𝐹))
52	51, 43	fveq12d 6652	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑚)‘(2nd ‘𝑥)) = ((1st ‘𝐹)‘𝑋))
53	51, 49	fveq12d 6652	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑚)‘(2nd ‘𝑦)) = ((1st ‘𝐹)‘𝑌))
54	52, 53	opeq12d 4773	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ = ⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩)
55	36	fveq2d 6649	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (1st ‘𝑛) = (1st ‘𝐺))
56	55, 49	fveq12d 6652	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑛)‘(2nd ‘𝑦)) = ((1st ‘𝐺)‘𝑌))
57	54, 56	oveq12d 7153	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦))) = (⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌)))
58	49	fveq2d 6649	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑎‘(2nd ‘𝑦)) = (𝑎‘𝑌))
59	35	fveq2d 6649	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑚) = (2nd ‘𝐹))
60	59, 43, 49	oveq123d 7156	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦)) = (𝑋(2nd ‘𝐹)𝑌))
61	60	fveq1d 6647	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔) = ((𝑋(2nd ‘𝐹)𝑌)‘𝑔))
62	57, 58, 61	oveq123d 7156	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)) = ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))
63	37, 50, 62	mpoeq123dv 7208	. . . . 5 ⊢ ((((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))
64	26, 34, 63	csbied2 3865	. . . 4 ⊢ (((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) ∧ 𝑚 = 𝐹) → ⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))
65	17, 25, 64	csbied2 3865	. . 3 ⊢ ((𝜑 ∧ (𝑥 = ⟨𝐹, 𝑋⟩ ∧ 𝑦 = ⟨𝐺, 𝑌⟩)) → ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))
66	20, 21	opelxpd 5557	. . 3 ⊢ (𝜑 → ⟨𝐹, 𝑋⟩ ∈ ((𝐶 Func 𝐷) × 𝐵))
67	29, 30	opelxpd 5557	. . 3 ⊢ (𝜑 → ⟨𝐺, 𝑌⟩ ∈ ((𝐶 Func 𝐷) × 𝐵))
68		ovex 7168	. . . . 5 ⊢ (𝐹𝑁𝐺) ∈ V
69		ovex 7168	. . . . 5 ⊢ (𝑋𝐻𝑌) ∈ V
70	68, 69	mpoex 7760	. . . 4 ⊢ (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))) ∈ V
71	70	a1i 11	. . 3 ⊢ (𝜑 → (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))) ∈ V)
72	16, 65, 66, 67, 71	ovmpod 7281	. 2 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐺, 𝑌⟩) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))
73	1, 72	syl5eq 2845	1 ⊢ (𝜑 → 𝐿 = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  Vcvv 3441  ⦋csb 3828  ⟨cop 4531   × cxp 5517  ‘cfv 6324  (class class class)co 7135   ∈ cmpo 7137  1^st c1st 7669  2^nd c2nd 7670  Basecbs 16475  Hom chom 16568  compcco 16569  Catccat 16927   Func cfunc 17116   Nat cnat 17203   eval_F cevlf 17451

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-oprab 7139  df-mpo 7140  df-1st 7671  df-2nd 7672  df-evlf 17455

This theorem is referenced by:  evlf2val  17461  evlfcl  17464