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 ‘ 𝐹 ) 𝑌 ) ‘ 𝑔 ) ) ) ) |