Metamath Proof Explorer


Theorem natfval

Description: Value of the function giving natural transformations between two categories. (Contributed by Mario Carneiro, 6-Jan-2017) (Proof shortened by AV, 1-Mar-2024)

Ref Expression
Hypotheses natfval.1 โŠข ๐‘ = ( ๐ถ Nat ๐ท )
natfval.b โŠข ๐ต = ( Base โ€˜ ๐ถ )
natfval.h โŠข ๐ป = ( Hom โ€˜ ๐ถ )
natfval.j โŠข ๐ฝ = ( Hom โ€˜ ๐ท )
natfval.o โŠข ยท = ( comp โ€˜ ๐ท )
Assertion natfval ๐‘ = ( ๐‘“ โˆˆ ( ๐ถ Func ๐ท ) , ๐‘” โˆˆ ( ๐ถ Func ๐ท ) โ†ฆ โฆ‹ ( 1st โ€˜ ๐‘“ ) / ๐‘Ÿ โฆŒ โฆ‹ ( 1st โ€˜ ๐‘” ) / ๐‘  โฆŒ { ๐‘Ž โˆˆ X ๐‘ฅ โˆˆ ๐ต ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ๐ฝ ( ๐‘  โ€˜ ๐‘ฅ ) ) โˆฃ โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ๐ป ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) } )

Proof

Step Hyp Ref Expression
1 natfval.1 โŠข ๐‘ = ( ๐ถ Nat ๐ท )
2 natfval.b โŠข ๐ต = ( Base โ€˜ ๐ถ )
3 natfval.h โŠข ๐ป = ( Hom โ€˜ ๐ถ )
4 natfval.j โŠข ๐ฝ = ( Hom โ€˜ ๐ท )
5 natfval.o โŠข ยท = ( comp โ€˜ ๐ท )
6 oveq12 โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ( ๐‘ก Func ๐‘ข ) = ( ๐ถ Func ๐ท ) )
7 simpl โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ๐‘ก = ๐ถ )
8 7 fveq2d โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ( Base โ€˜ ๐‘ก ) = ( Base โ€˜ ๐ถ ) )
9 8 2 eqtr4di โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ( Base โ€˜ ๐‘ก ) = ๐ต )
10 9 ixpeq1d โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ X ๐‘ฅ โˆˆ ( Base โ€˜ ๐‘ก ) ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ( Hom โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฅ ) ) = X ๐‘ฅ โˆˆ ๐ต ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ( Hom โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฅ ) ) )
11 simpr โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ๐‘ข = ๐ท )
12 11 fveq2d โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ( Hom โ€˜ ๐‘ข ) = ( Hom โ€˜ ๐ท ) )
13 12 4 eqtr4di โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ( Hom โ€˜ ๐‘ข ) = ๐ฝ )
14 13 oveqd โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ( Hom โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฅ ) ) = ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ๐ฝ ( ๐‘  โ€˜ ๐‘ฅ ) ) )
15 14 ixpeq2dv โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ X ๐‘ฅ โˆˆ ๐ต ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ( Hom โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฅ ) ) = X ๐‘ฅ โˆˆ ๐ต ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ๐ฝ ( ๐‘  โ€˜ ๐‘ฅ ) ) )
16 10 15 eqtrd โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ X ๐‘ฅ โˆˆ ( Base โ€˜ ๐‘ก ) ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ( Hom โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฅ ) ) = X ๐‘ฅ โˆˆ ๐ต ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ๐ฝ ( ๐‘  โ€˜ ๐‘ฅ ) ) )
17 7 fveq2d โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ( Hom โ€˜ ๐‘ก ) = ( Hom โ€˜ ๐ถ ) )
18 17 3 eqtr4di โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ( Hom โ€˜ ๐‘ก ) = ๐ป )
19 18 oveqd โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ( ๐‘ฅ ( Hom โ€˜ ๐‘ก ) ๐‘ฆ ) = ( ๐‘ฅ ๐ป ๐‘ฆ ) )
20 11 fveq2d โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ( comp โ€˜ ๐‘ข ) = ( comp โ€˜ ๐ท ) )
21 20 5 eqtr4di โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ( comp โ€˜ ๐‘ข ) = ยท )
22 21 oveqd โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) = ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) )
23 22 oveqd โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) )
24 21 oveqd โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) = ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) )
25 24 oveqd โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) )
26 23 25 eqeq12d โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ( ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) โ†” ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) ) )
27 19 26 raleqbidv โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ( โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ( Hom โ€˜ ๐‘ก ) ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) โ†” โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ๐ป ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) ) )
28 9 27 raleqbidv โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ( โˆ€ ๐‘ฆ โˆˆ ( Base โ€˜ ๐‘ก ) โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ( Hom โ€˜ ๐‘ก ) ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) โ†” โˆ€ ๐‘ฆ โˆˆ ๐ต โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ๐ป ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) ) )
29 9 28 raleqbidv โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ( โˆ€ ๐‘ฅ โˆˆ ( Base โ€˜ ๐‘ก ) โˆ€ ๐‘ฆ โˆˆ ( Base โ€˜ ๐‘ก ) โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ( Hom โ€˜ ๐‘ก ) ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) โ†” โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ๐ป ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) ) )
30 16 29 rabeqbidv โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ { ๐‘Ž โˆˆ X ๐‘ฅ โˆˆ ( Base โ€˜ ๐‘ก ) ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ( Hom โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฅ ) ) โˆฃ โˆ€ ๐‘ฅ โˆˆ ( Base โ€˜ ๐‘ก ) โˆ€ ๐‘ฆ โˆˆ ( Base โ€˜ ๐‘ก ) โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ( Hom โ€˜ ๐‘ก ) ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) } = { ๐‘Ž โˆˆ X ๐‘ฅ โˆˆ ๐ต ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ๐ฝ ( ๐‘  โ€˜ ๐‘ฅ ) ) โˆฃ โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ๐ป ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) } )
31 30 csbeq2dv โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ โฆ‹ ( 1st โ€˜ ๐‘” ) / ๐‘  โฆŒ { ๐‘Ž โˆˆ X ๐‘ฅ โˆˆ ( Base โ€˜ ๐‘ก ) ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ( Hom โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฅ ) ) โˆฃ โˆ€ ๐‘ฅ โˆˆ ( Base โ€˜ ๐‘ก ) โˆ€ ๐‘ฆ โˆˆ ( Base โ€˜ ๐‘ก ) โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ( Hom โ€˜ ๐‘ก ) ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) } = โฆ‹ ( 1st โ€˜ ๐‘” ) / ๐‘  โฆŒ { ๐‘Ž โˆˆ X ๐‘ฅ โˆˆ ๐ต ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ๐ฝ ( ๐‘  โ€˜ ๐‘ฅ ) ) โˆฃ โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ๐ป ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) } )
32 31 csbeq2dv โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ โฆ‹ ( 1st โ€˜ ๐‘“ ) / ๐‘Ÿ โฆŒ โฆ‹ ( 1st โ€˜ ๐‘” ) / ๐‘  โฆŒ { ๐‘Ž โˆˆ X ๐‘ฅ โˆˆ ( Base โ€˜ ๐‘ก ) ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ( Hom โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฅ ) ) โˆฃ โˆ€ ๐‘ฅ โˆˆ ( Base โ€˜ ๐‘ก ) โˆ€ ๐‘ฆ โˆˆ ( Base โ€˜ ๐‘ก ) โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ( Hom โ€˜ ๐‘ก ) ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) } = โฆ‹ ( 1st โ€˜ ๐‘“ ) / ๐‘Ÿ โฆŒ โฆ‹ ( 1st โ€˜ ๐‘” ) / ๐‘  โฆŒ { ๐‘Ž โˆˆ X ๐‘ฅ โˆˆ ๐ต ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ๐ฝ ( ๐‘  โ€˜ ๐‘ฅ ) ) โˆฃ โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ๐ป ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) } )
33 6 6 32 mpoeq123dv โŠข ( ( ๐‘ก = ๐ถ โˆง ๐‘ข = ๐ท ) โ†’ ( ๐‘“ โˆˆ ( ๐‘ก Func ๐‘ข ) , ๐‘” โˆˆ ( ๐‘ก Func ๐‘ข ) โ†ฆ โฆ‹ ( 1st โ€˜ ๐‘“ ) / ๐‘Ÿ โฆŒ โฆ‹ ( 1st โ€˜ ๐‘” ) / ๐‘  โฆŒ { ๐‘Ž โˆˆ X ๐‘ฅ โˆˆ ( Base โ€˜ ๐‘ก ) ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ( Hom โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฅ ) ) โˆฃ โˆ€ ๐‘ฅ โˆˆ ( Base โ€˜ ๐‘ก ) โˆ€ ๐‘ฆ โˆˆ ( Base โ€˜ ๐‘ก ) โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ( Hom โ€˜ ๐‘ก ) ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) } ) = ( ๐‘“ โˆˆ ( ๐ถ Func ๐ท ) , ๐‘” โˆˆ ( ๐ถ Func ๐ท ) โ†ฆ โฆ‹ ( 1st โ€˜ ๐‘“ ) / ๐‘Ÿ โฆŒ โฆ‹ ( 1st โ€˜ ๐‘” ) / ๐‘  โฆŒ { ๐‘Ž โˆˆ X ๐‘ฅ โˆˆ ๐ต ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ๐ฝ ( ๐‘  โ€˜ ๐‘ฅ ) ) โˆฃ โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ๐ป ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) } ) )
34 df-nat โŠข Nat = ( ๐‘ก โˆˆ Cat , ๐‘ข โˆˆ Cat โ†ฆ ( ๐‘“ โˆˆ ( ๐‘ก Func ๐‘ข ) , ๐‘” โˆˆ ( ๐‘ก Func ๐‘ข ) โ†ฆ โฆ‹ ( 1st โ€˜ ๐‘“ ) / ๐‘Ÿ โฆŒ โฆ‹ ( 1st โ€˜ ๐‘” ) / ๐‘  โฆŒ { ๐‘Ž โˆˆ X ๐‘ฅ โˆˆ ( Base โ€˜ ๐‘ก ) ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ( Hom โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฅ ) ) โˆฃ โˆ€ ๐‘ฅ โˆˆ ( Base โ€˜ ๐‘ก ) โˆ€ ๐‘ฆ โˆˆ ( Base โ€˜ ๐‘ก ) โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ( Hom โ€˜ ๐‘ก ) ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ( comp โ€˜ ๐‘ข ) ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) } ) )
35 ovex โŠข ( ๐ถ Func ๐ท ) โˆˆ V
36 35 35 mpoex โŠข ( ๐‘“ โˆˆ ( ๐ถ Func ๐ท ) , ๐‘” โˆˆ ( ๐ถ Func ๐ท ) โ†ฆ โฆ‹ ( 1st โ€˜ ๐‘“ ) / ๐‘Ÿ โฆŒ โฆ‹ ( 1st โ€˜ ๐‘” ) / ๐‘  โฆŒ { ๐‘Ž โˆˆ X ๐‘ฅ โˆˆ ๐ต ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ๐ฝ ( ๐‘  โ€˜ ๐‘ฅ ) ) โˆฃ โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ๐ป ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) } ) โˆˆ V
37 33 34 36 ovmpoa โŠข ( ( ๐ถ โˆˆ Cat โˆง ๐ท โˆˆ Cat ) โ†’ ( ๐ถ Nat ๐ท ) = ( ๐‘“ โˆˆ ( ๐ถ Func ๐ท ) , ๐‘” โˆˆ ( ๐ถ Func ๐ท ) โ†ฆ โฆ‹ ( 1st โ€˜ ๐‘“ ) / ๐‘Ÿ โฆŒ โฆ‹ ( 1st โ€˜ ๐‘” ) / ๐‘  โฆŒ { ๐‘Ž โˆˆ X ๐‘ฅ โˆˆ ๐ต ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ๐ฝ ( ๐‘  โ€˜ ๐‘ฅ ) ) โˆฃ โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ๐ป ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) } ) )
38 34 mpondm0 โŠข ( ยฌ ( ๐ถ โˆˆ Cat โˆง ๐ท โˆˆ Cat ) โ†’ ( ๐ถ Nat ๐ท ) = โˆ… )
39 funcrcl โŠข ( ๐‘“ โˆˆ ( ๐ถ Func ๐ท ) โ†’ ( ๐ถ โˆˆ Cat โˆง ๐ท โˆˆ Cat ) )
40 39 con3i โŠข ( ยฌ ( ๐ถ โˆˆ Cat โˆง ๐ท โˆˆ Cat ) โ†’ ยฌ ๐‘“ โˆˆ ( ๐ถ Func ๐ท ) )
41 40 eq0rdv โŠข ( ยฌ ( ๐ถ โˆˆ Cat โˆง ๐ท โˆˆ Cat ) โ†’ ( ๐ถ Func ๐ท ) = โˆ… )
42 41 olcd โŠข ( ยฌ ( ๐ถ โˆˆ Cat โˆง ๐ท โˆˆ Cat ) โ†’ ( ( ๐ถ Func ๐ท ) = โˆ… โˆจ ( ๐ถ Func ๐ท ) = โˆ… ) )
43 0mpo0 โŠข ( ( ( ๐ถ Func ๐ท ) = โˆ… โˆจ ( ๐ถ Func ๐ท ) = โˆ… ) โ†’ ( ๐‘“ โˆˆ ( ๐ถ Func ๐ท ) , ๐‘” โˆˆ ( ๐ถ Func ๐ท ) โ†ฆ โฆ‹ ( 1st โ€˜ ๐‘“ ) / ๐‘Ÿ โฆŒ โฆ‹ ( 1st โ€˜ ๐‘” ) / ๐‘  โฆŒ { ๐‘Ž โˆˆ X ๐‘ฅ โˆˆ ๐ต ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ๐ฝ ( ๐‘  โ€˜ ๐‘ฅ ) ) โˆฃ โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ๐ป ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) } ) = โˆ… )
44 42 43 syl โŠข ( ยฌ ( ๐ถ โˆˆ Cat โˆง ๐ท โˆˆ Cat ) โ†’ ( ๐‘“ โˆˆ ( ๐ถ Func ๐ท ) , ๐‘” โˆˆ ( ๐ถ Func ๐ท ) โ†ฆ โฆ‹ ( 1st โ€˜ ๐‘“ ) / ๐‘Ÿ โฆŒ โฆ‹ ( 1st โ€˜ ๐‘” ) / ๐‘  โฆŒ { ๐‘Ž โˆˆ X ๐‘ฅ โˆˆ ๐ต ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ๐ฝ ( ๐‘  โ€˜ ๐‘ฅ ) ) โˆฃ โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ๐ป ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) } ) = โˆ… )
45 38 44 eqtr4d โŠข ( ยฌ ( ๐ถ โˆˆ Cat โˆง ๐ท โˆˆ Cat ) โ†’ ( ๐ถ Nat ๐ท ) = ( ๐‘“ โˆˆ ( ๐ถ Func ๐ท ) , ๐‘” โˆˆ ( ๐ถ Func ๐ท ) โ†ฆ โฆ‹ ( 1st โ€˜ ๐‘“ ) / ๐‘Ÿ โฆŒ โฆ‹ ( 1st โ€˜ ๐‘” ) / ๐‘  โฆŒ { ๐‘Ž โˆˆ X ๐‘ฅ โˆˆ ๐ต ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ๐ฝ ( ๐‘  โ€˜ ๐‘ฅ ) ) โˆฃ โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ๐ป ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) } ) )
46 37 45 pm2.61i โŠข ( ๐ถ Nat ๐ท ) = ( ๐‘“ โˆˆ ( ๐ถ Func ๐ท ) , ๐‘” โˆˆ ( ๐ถ Func ๐ท ) โ†ฆ โฆ‹ ( 1st โ€˜ ๐‘“ ) / ๐‘Ÿ โฆŒ โฆ‹ ( 1st โ€˜ ๐‘” ) / ๐‘  โฆŒ { ๐‘Ž โˆˆ X ๐‘ฅ โˆˆ ๐ต ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ๐ฝ ( ๐‘  โ€˜ ๐‘ฅ ) ) โˆฃ โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ๐ป ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) } )
47 1 46 eqtri โŠข ๐‘ = ( ๐‘“ โˆˆ ( ๐ถ Func ๐ท ) , ๐‘” โˆˆ ( ๐ถ Func ๐ท ) โ†ฆ โฆ‹ ( 1st โ€˜ ๐‘“ ) / ๐‘Ÿ โฆŒ โฆ‹ ( 1st โ€˜ ๐‘” ) / ๐‘  โฆŒ { ๐‘Ž โˆˆ X ๐‘ฅ โˆˆ ๐ต ( ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ๐ฝ ( ๐‘  โ€˜ ๐‘ฅ ) ) โˆฃ โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต โˆ€ โ„Ž โˆˆ ( ๐‘ฅ ๐ป ๐‘ฆ ) ( ( ๐‘Ž โ€˜ ๐‘ฆ ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘Ÿ โ€˜ ๐‘ฆ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘“ ) ๐‘ฆ ) โ€˜ โ„Ž ) ) = ( ( ( ๐‘ฅ ( 2nd โ€˜ ๐‘” ) ๐‘ฆ ) โ€˜ โ„Ž ) ( โŸจ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) , ( ๐‘  โ€˜ ๐‘ฅ ) โŸฉ ยท ( ๐‘  โ€˜ ๐‘ฆ ) ) ( ๐‘Ž โ€˜ ๐‘ฅ ) ) } )