Metamath Proof Explorer


Theorem evlf2

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

Ref Expression
Hypotheses 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 evlf2 ( 𝜑𝐿 = ( 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) , 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝑎𝑌 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑋 ) , ( ( 1st𝐹 ) ‘ 𝑌 ) ⟩ · ( ( 1st𝐺 ) ‘ 𝑌 ) ) ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ 𝑔 ) ) ) )

Proof

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