Step | Hyp | Ref
| Expression |
1 | | evlfval.e |
. 2
โข ๐ธ = (๐ถ evalF ๐ท) |
2 | | df-evlf 18062 |
. . . 4
โข
evalF = (๐ โ Cat, ๐ โ Cat โฆ โจ(๐ โ (๐ Func ๐), ๐ฅ โ (Baseโ๐) โฆ ((1st โ๐)โ๐ฅ)), (๐ฅ โ ((๐ Func ๐) ร (Baseโ๐)), ๐ฆ โ ((๐ Func ๐) ร (Baseโ๐)) โฆ โฆ(1st
โ๐ฅ) / ๐โฆโฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐(๐ Nat ๐)๐), ๐ โ ((2nd โ๐ฅ)(Hom โ๐)(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ(compโ๐)((1st โ๐)โ(2nd
โ๐ฆ)))(((2nd โ๐ฅ)(2nd โ๐)(2nd โ๐ฆ))โ๐))))โฉ) |
3 | 2 | a1i 11 |
. . 3
โข (๐ โ evalF =
(๐ โ Cat, ๐ โ Cat โฆ โจ(๐ โ (๐ Func ๐), ๐ฅ โ (Baseโ๐) โฆ ((1st โ๐)โ๐ฅ)), (๐ฅ โ ((๐ Func ๐) ร (Baseโ๐)), ๐ฆ โ ((๐ Func ๐) ร (Baseโ๐)) โฆ โฆ(1st
โ๐ฅ) / ๐โฆโฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐(๐ Nat ๐)๐), ๐ โ ((2nd โ๐ฅ)(Hom โ๐)(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ(compโ๐)((1st โ๐)โ(2nd
โ๐ฆ)))(((2nd โ๐ฅ)(2nd โ๐)(2nd โ๐ฆ))โ๐))))โฉ)) |
4 | | simprl 769 |
. . . . . 6
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ ๐ = ๐ถ) |
5 | | simprr 771 |
. . . . . 6
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ ๐ = ๐ท) |
6 | 4, 5 | oveq12d 7369 |
. . . . 5
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ (๐ Func ๐) = (๐ถ Func ๐ท)) |
7 | 4 | fveq2d 6843 |
. . . . . 6
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ (Baseโ๐) = (Baseโ๐ถ)) |
8 | | evlfval.b |
. . . . . 6
โข ๐ต = (Baseโ๐ถ) |
9 | 7, 8 | eqtr4di 2795 |
. . . . 5
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ (Baseโ๐) = ๐ต) |
10 | | eqidd 2738 |
. . . . 5
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ ((1st โ๐)โ๐ฅ) = ((1st โ๐)โ๐ฅ)) |
11 | 6, 9, 10 | mpoeq123dv 7426 |
. . . 4
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ (๐ โ (๐ Func ๐), ๐ฅ โ (Baseโ๐) โฆ ((1st โ๐)โ๐ฅ)) = (๐ โ (๐ถ Func ๐ท), ๐ฅ โ ๐ต โฆ ((1st โ๐)โ๐ฅ))) |
12 | 6, 9 | xpeq12d 5662 |
. . . . 5
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ ((๐ Func ๐) ร (Baseโ๐)) = ((๐ถ Func ๐ท) ร ๐ต)) |
13 | 4, 5 | oveq12d 7369 |
. . . . . . . . . 10
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ (๐ Nat ๐) = (๐ถ Nat ๐ท)) |
14 | | evlfval.n |
. . . . . . . . . 10
โข ๐ = (๐ถ Nat ๐ท) |
15 | 13, 14 | eqtr4di 2795 |
. . . . . . . . 9
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ (๐ Nat ๐) = ๐) |
16 | 15 | oveqd 7368 |
. . . . . . . 8
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ (๐(๐ Nat ๐)๐) = (๐๐๐)) |
17 | 4 | fveq2d 6843 |
. . . . . . . . . 10
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ (Hom โ๐) = (Hom โ๐ถ)) |
18 | | evlfval.h |
. . . . . . . . . 10
โข ๐ป = (Hom โ๐ถ) |
19 | 17, 18 | eqtr4di 2795 |
. . . . . . . . 9
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ (Hom โ๐) = ๐ป) |
20 | 19 | oveqd 7368 |
. . . . . . . 8
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ ((2nd โ๐ฅ)(Hom โ๐)(2nd โ๐ฆ)) = ((2nd โ๐ฅ)๐ป(2nd โ๐ฆ))) |
21 | 5 | fveq2d 6843 |
. . . . . . . . . . 11
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ (compโ๐) = (compโ๐ท)) |
22 | | evlfval.o |
. . . . . . . . . . 11
โข ยท =
(compโ๐ท) |
23 | 21, 22 | eqtr4di 2795 |
. . . . . . . . . 10
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ (compโ๐) = ยท ) |
24 | 23 | oveqd 7368 |
. . . . . . . . 9
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ (โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ(compโ๐)((1st โ๐)โ(2nd
โ๐ฆ))) =
(โจ((1st โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ)))) |
25 | 24 | oveqd 7368 |
. . . . . . . 8
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ(compโ๐)((1st โ๐)โ(2nd
โ๐ฆ)))(((2nd โ๐ฅ)(2nd โ๐)(2nd โ๐ฆ))โ๐)) = ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ)))(((2nd
โ๐ฅ)(2nd
โ๐)(2nd
โ๐ฆ))โ๐))) |
26 | 16, 20, 25 | mpoeq123dv 7426 |
. . . . . . 7
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ (๐ โ (๐(๐ Nat ๐)๐), ๐ โ ((2nd โ๐ฅ)(Hom โ๐)(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ(compโ๐)((1st โ๐)โ(2nd
โ๐ฆ)))(((2nd โ๐ฅ)(2nd โ๐)(2nd โ๐ฆ))โ๐))) = (๐ โ (๐๐๐), ๐ โ ((2nd โ๐ฅ)๐ป(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ)))(((2nd
โ๐ฅ)(2nd
โ๐)(2nd
โ๐ฆ))โ๐)))) |
27 | 26 | csbeq2dv 3860 |
. . . . . 6
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ โฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐(๐ Nat ๐)๐), ๐ โ ((2nd โ๐ฅ)(Hom โ๐)(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ(compโ๐)((1st โ๐)โ(2nd
โ๐ฆ)))(((2nd โ๐ฅ)(2nd โ๐)(2nd โ๐ฆ))โ๐))) = โฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐๐๐), ๐ โ ((2nd โ๐ฅ)๐ป(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ)))(((2nd
โ๐ฅ)(2nd
โ๐)(2nd
โ๐ฆ))โ๐)))) |
28 | 27 | csbeq2dv 3860 |
. . . . 5
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ โฆ(1st
โ๐ฅ) / ๐โฆโฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐(๐ Nat ๐)๐), ๐ โ ((2nd โ๐ฅ)(Hom โ๐)(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ(compโ๐)((1st โ๐)โ(2nd
โ๐ฆ)))(((2nd โ๐ฅ)(2nd โ๐)(2nd โ๐ฆ))โ๐))) = โฆ(1st
โ๐ฅ) / ๐โฆโฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐๐๐), ๐ โ ((2nd โ๐ฅ)๐ป(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ)))(((2nd
โ๐ฅ)(2nd
โ๐)(2nd
โ๐ฆ))โ๐)))) |
29 | 12, 12, 28 | mpoeq123dv 7426 |
. . . 4
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ (๐ฅ โ ((๐ Func ๐) ร (Baseโ๐)), ๐ฆ โ ((๐ Func ๐) ร (Baseโ๐)) โฆ โฆ(1st
โ๐ฅ) / ๐โฆโฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐(๐ Nat ๐)๐), ๐ โ ((2nd โ๐ฅ)(Hom โ๐)(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ(compโ๐)((1st โ๐)โ(2nd
โ๐ฆ)))(((2nd โ๐ฅ)(2nd โ๐)(2nd โ๐ฆ))โ๐)))) = (๐ฅ โ ((๐ถ Func ๐ท) ร ๐ต), ๐ฆ โ ((๐ถ Func ๐ท) ร ๐ต) โฆ โฆ(1st
โ๐ฅ) / ๐โฆโฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐๐๐), ๐ โ ((2nd โ๐ฅ)๐ป(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ)))(((2nd
โ๐ฅ)(2nd
โ๐)(2nd
โ๐ฆ))โ๐))))) |
30 | 11, 29 | opeq12d 4836 |
. . 3
โข ((๐ โง (๐ = ๐ถ โง ๐ = ๐ท)) โ โจ(๐ โ (๐ Func ๐), ๐ฅ โ (Baseโ๐) โฆ ((1st โ๐)โ๐ฅ)), (๐ฅ โ ((๐ Func ๐) ร (Baseโ๐)), ๐ฆ โ ((๐ Func ๐) ร (Baseโ๐)) โฆ โฆ(1st
โ๐ฅ) / ๐โฆโฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐(๐ Nat ๐)๐), ๐ โ ((2nd โ๐ฅ)(Hom โ๐)(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ(compโ๐)((1st โ๐)โ(2nd
โ๐ฆ)))(((2nd โ๐ฅ)(2nd โ๐)(2nd โ๐ฆ))โ๐))))โฉ = โจ(๐ โ (๐ถ Func ๐ท), ๐ฅ โ ๐ต โฆ ((1st โ๐)โ๐ฅ)), (๐ฅ โ ((๐ถ Func ๐ท) ร ๐ต), ๐ฆ โ ((๐ถ Func ๐ท) ร ๐ต) โฆ โฆ(1st
โ๐ฅ) / ๐โฆโฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐๐๐), ๐ โ ((2nd โ๐ฅ)๐ป(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ)))(((2nd
โ๐ฅ)(2nd
โ๐)(2nd
โ๐ฆ))โ๐))))โฉ) |
31 | | evlfval.c |
. . 3
โข (๐ โ ๐ถ โ Cat) |
32 | | evlfval.d |
. . 3
โข (๐ โ ๐ท โ Cat) |
33 | | opex 5419 |
. . . 4
โข
โจ(๐ โ
(๐ถ Func ๐ท), ๐ฅ โ ๐ต โฆ ((1st โ๐)โ๐ฅ)), (๐ฅ โ ((๐ถ Func ๐ท) ร ๐ต), ๐ฆ โ ((๐ถ Func ๐ท) ร ๐ต) โฆ โฆ(1st
โ๐ฅ) / ๐โฆโฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐๐๐), ๐ โ ((2nd โ๐ฅ)๐ป(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ)))(((2nd
โ๐ฅ)(2nd
โ๐)(2nd
โ๐ฆ))โ๐))))โฉ โ
V |
34 | 33 | a1i 11 |
. . 3
โข (๐ โ โจ(๐ โ (๐ถ Func ๐ท), ๐ฅ โ ๐ต โฆ ((1st โ๐)โ๐ฅ)), (๐ฅ โ ((๐ถ Func ๐ท) ร ๐ต), ๐ฆ โ ((๐ถ Func ๐ท) ร ๐ต) โฆ โฆ(1st
โ๐ฅ) / ๐โฆโฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐๐๐), ๐ โ ((2nd โ๐ฅ)๐ป(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ)))(((2nd
โ๐ฅ)(2nd
โ๐)(2nd
โ๐ฆ))โ๐))))โฉ โ
V) |
35 | 3, 30, 31, 32, 34 | ovmpod 7501 |
. 2
โข (๐ โ (๐ถ evalF ๐ท) = โจ(๐ โ (๐ถ Func ๐ท), ๐ฅ โ ๐ต โฆ ((1st โ๐)โ๐ฅ)), (๐ฅ โ ((๐ถ Func ๐ท) ร ๐ต), ๐ฆ โ ((๐ถ Func ๐ท) ร ๐ต) โฆ โฆ(1st
โ๐ฅ) / ๐โฆโฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐๐๐), ๐ โ ((2nd โ๐ฅ)๐ป(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ)))(((2nd
โ๐ฅ)(2nd
โ๐)(2nd
โ๐ฆ))โ๐))))โฉ) |
36 | 1, 35 | eqtrid 2789 |
1
โข (๐ โ ๐ธ = โจ(๐ โ (๐ถ Func ๐ท), ๐ฅ โ ๐ต โฆ ((1st โ๐)โ๐ฅ)), (๐ฅ โ ((๐ถ Func ๐ท) ร ๐ต), ๐ฆ โ ((๐ถ Func ๐ท) ร ๐ต) โฆ โฆ(1st
โ๐ฅ) / ๐โฆโฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐๐๐), ๐ โ ((2nd โ๐ฅ)๐ป(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ)))(((2nd
โ๐ฅ)(2nd
โ๐)(2nd
โ๐ฆ))โ๐))))โฉ) |