Step | Hyp | Ref
| Expression |
1 | | natixp.2 |
. . . 4
โข (๐ โ ๐ด โ (โจ๐น, ๐บโฉ๐โจ๐พ, ๐ฟโฉ)) |
2 | | natrcl.1 |
. . . . 5
โข ๐ = (๐ถ Nat ๐ท) |
3 | | natixp.b |
. . . . 5
โข ๐ต = (Baseโ๐ถ) |
4 | | nati.h |
. . . . 5
โข ๐ป = (Hom โ๐ถ) |
5 | | eqid 2733 |
. . . . 5
โข (Hom
โ๐ท) = (Hom
โ๐ท) |
6 | | nati.o |
. . . . 5
โข ยท =
(compโ๐ท) |
7 | 2 | natrcl 17842 |
. . . . . . . 8
โข (๐ด โ (โจ๐น, ๐บโฉ๐โจ๐พ, ๐ฟโฉ) โ (โจ๐น, ๐บโฉ โ (๐ถ Func ๐ท) โง โจ๐พ, ๐ฟโฉ โ (๐ถ Func ๐ท))) |
8 | 1, 7 | syl 17 |
. . . . . . 7
โข (๐ โ (โจ๐น, ๐บโฉ โ (๐ถ Func ๐ท) โง โจ๐พ, ๐ฟโฉ โ (๐ถ Func ๐ท))) |
9 | 8 | simpld 496 |
. . . . . 6
โข (๐ โ โจ๐น, ๐บโฉ โ (๐ถ Func ๐ท)) |
10 | | df-br 5107 |
. . . . . 6
โข (๐น(๐ถ Func ๐ท)๐บ โ โจ๐น, ๐บโฉ โ (๐ถ Func ๐ท)) |
11 | 9, 10 | sylibr 233 |
. . . . 5
โข (๐ โ ๐น(๐ถ Func ๐ท)๐บ) |
12 | 8 | simprd 497 |
. . . . . 6
โข (๐ โ โจ๐พ, ๐ฟโฉ โ (๐ถ Func ๐ท)) |
13 | | df-br 5107 |
. . . . . 6
โข (๐พ(๐ถ Func ๐ท)๐ฟ โ โจ๐พ, ๐ฟโฉ โ (๐ถ Func ๐ท)) |
14 | 12, 13 | sylibr 233 |
. . . . 5
โข (๐ โ ๐พ(๐ถ Func ๐ท)๐ฟ) |
15 | 2, 3, 4, 5, 6, 11,
14 | isnat 17839 |
. . . 4
โข (๐ โ (๐ด โ (โจ๐น, ๐บโฉ๐โจ๐พ, ๐ฟโฉ) โ (๐ด โ X๐ฅ โ ๐ต ((๐นโ๐ฅ)(Hom โ๐ท)(๐พโ๐ฅ)) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)((๐ดโ๐ฆ)(โจ(๐นโ๐ฅ), (๐นโ๐ฆ)โฉ ยท (๐พโ๐ฆ))((๐ฅ๐บ๐ฆ)โ๐)) = (((๐ฅ๐ฟ๐ฆ)โ๐)(โจ(๐นโ๐ฅ), (๐พโ๐ฅ)โฉ ยท (๐พโ๐ฆ))(๐ดโ๐ฅ))))) |
16 | 1, 15 | mpbid 231 |
. . 3
โข (๐ โ (๐ด โ X๐ฅ โ ๐ต ((๐นโ๐ฅ)(Hom โ๐ท)(๐พโ๐ฅ)) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)((๐ดโ๐ฆ)(โจ(๐นโ๐ฅ), (๐นโ๐ฆ)โฉ ยท (๐พโ๐ฆ))((๐ฅ๐บ๐ฆ)โ๐)) = (((๐ฅ๐ฟ๐ฆ)โ๐)(โจ(๐นโ๐ฅ), (๐พโ๐ฅ)โฉ ยท (๐พโ๐ฆ))(๐ดโ๐ฅ)))) |
17 | 16 | simprd 497 |
. 2
โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)((๐ดโ๐ฆ)(โจ(๐นโ๐ฅ), (๐นโ๐ฆ)โฉ ยท (๐พโ๐ฆ))((๐ฅ๐บ๐ฆ)โ๐)) = (((๐ฅ๐ฟ๐ฆ)โ๐)(โจ(๐นโ๐ฅ), (๐พโ๐ฅ)โฉ ยท (๐พโ๐ฆ))(๐ดโ๐ฅ))) |
18 | | nati.x |
. . 3
โข (๐ โ ๐ โ ๐ต) |
19 | | nati.y |
. . . . 5
โข (๐ โ ๐ โ ๐ต) |
20 | 19 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฅ = ๐) โ ๐ โ ๐ต) |
21 | | nati.r |
. . . . . . 7
โข (๐ โ ๐
โ (๐๐ป๐)) |
22 | 21 | ad2antrr 725 |
. . . . . 6
โข (((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โ ๐
โ (๐๐ป๐)) |
23 | | simplr 768 |
. . . . . . 7
โข (((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โ ๐ฅ = ๐) |
24 | | simpr 486 |
. . . . . . 7
โข (((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โ ๐ฆ = ๐) |
25 | 23, 24 | oveq12d 7376 |
. . . . . 6
โข (((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โ (๐ฅ๐ป๐ฆ) = (๐๐ป๐)) |
26 | 22, 25 | eleqtrrd 2837 |
. . . . 5
โข (((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โ ๐
โ (๐ฅ๐ป๐ฆ)) |
27 | | simpllr 775 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โง ๐ = ๐
) โ ๐ฅ = ๐) |
28 | 27 | fveq2d 6847 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โง ๐ = ๐
) โ (๐นโ๐ฅ) = (๐นโ๐)) |
29 | | simplr 768 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โง ๐ = ๐
) โ ๐ฆ = ๐) |
30 | 29 | fveq2d 6847 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โง ๐ = ๐
) โ (๐นโ๐ฆ) = (๐นโ๐)) |
31 | 28, 30 | opeq12d 4839 |
. . . . . . . 8
โข ((((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โง ๐ = ๐
) โ โจ(๐นโ๐ฅ), (๐นโ๐ฆ)โฉ = โจ(๐นโ๐), (๐นโ๐)โฉ) |
32 | 29 | fveq2d 6847 |
. . . . . . . 8
โข ((((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โง ๐ = ๐
) โ (๐พโ๐ฆ) = (๐พโ๐)) |
33 | 31, 32 | oveq12d 7376 |
. . . . . . 7
โข ((((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โง ๐ = ๐
) โ (โจ(๐นโ๐ฅ), (๐นโ๐ฆ)โฉ ยท (๐พโ๐ฆ)) = (โจ(๐นโ๐), (๐นโ๐)โฉ ยท (๐พโ๐))) |
34 | 29 | fveq2d 6847 |
. . . . . . 7
โข ((((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โง ๐ = ๐
) โ (๐ดโ๐ฆ) = (๐ดโ๐)) |
35 | 27, 29 | oveq12d 7376 |
. . . . . . . 8
โข ((((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โง ๐ = ๐
) โ (๐ฅ๐บ๐ฆ) = (๐๐บ๐)) |
36 | | simpr 486 |
. . . . . . . 8
โข ((((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โง ๐ = ๐
) โ ๐ = ๐
) |
37 | 35, 36 | fveq12d 6850 |
. . . . . . 7
โข ((((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โง ๐ = ๐
) โ ((๐ฅ๐บ๐ฆ)โ๐) = ((๐๐บ๐)โ๐
)) |
38 | 33, 34, 37 | oveq123d 7379 |
. . . . . 6
โข ((((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โง ๐ = ๐
) โ ((๐ดโ๐ฆ)(โจ(๐นโ๐ฅ), (๐นโ๐ฆ)โฉ ยท (๐พโ๐ฆ))((๐ฅ๐บ๐ฆ)โ๐)) = ((๐ดโ๐)(โจ(๐นโ๐), (๐นโ๐)โฉ ยท (๐พโ๐))((๐๐บ๐)โ๐
))) |
39 | 27 | fveq2d 6847 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โง ๐ = ๐
) โ (๐พโ๐ฅ) = (๐พโ๐)) |
40 | 28, 39 | opeq12d 4839 |
. . . . . . . 8
โข ((((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โง ๐ = ๐
) โ โจ(๐นโ๐ฅ), (๐พโ๐ฅ)โฉ = โจ(๐นโ๐), (๐พโ๐)โฉ) |
41 | 40, 32 | oveq12d 7376 |
. . . . . . 7
โข ((((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โง ๐ = ๐
) โ (โจ(๐นโ๐ฅ), (๐พโ๐ฅ)โฉ ยท (๐พโ๐ฆ)) = (โจ(๐นโ๐), (๐พโ๐)โฉ ยท (๐พโ๐))) |
42 | 27, 29 | oveq12d 7376 |
. . . . . . . 8
โข ((((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โง ๐ = ๐
) โ (๐ฅ๐ฟ๐ฆ) = (๐๐ฟ๐)) |
43 | 42, 36 | fveq12d 6850 |
. . . . . . 7
โข ((((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โง ๐ = ๐
) โ ((๐ฅ๐ฟ๐ฆ)โ๐) = ((๐๐ฟ๐)โ๐
)) |
44 | 27 | fveq2d 6847 |
. . . . . . 7
โข ((((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โง ๐ = ๐
) โ (๐ดโ๐ฅ) = (๐ดโ๐)) |
45 | 41, 43, 44 | oveq123d 7379 |
. . . . . 6
โข ((((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โง ๐ = ๐
) โ (((๐ฅ๐ฟ๐ฆ)โ๐)(โจ(๐นโ๐ฅ), (๐พโ๐ฅ)โฉ ยท (๐พโ๐ฆ))(๐ดโ๐ฅ)) = (((๐๐ฟ๐)โ๐
)(โจ(๐นโ๐), (๐พโ๐)โฉ ยท (๐พโ๐))(๐ดโ๐))) |
46 | 38, 45 | eqeq12d 2749 |
. . . . 5
โข ((((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โง ๐ = ๐
) โ (((๐ดโ๐ฆ)(โจ(๐นโ๐ฅ), (๐นโ๐ฆ)โฉ ยท (๐พโ๐ฆ))((๐ฅ๐บ๐ฆ)โ๐)) = (((๐ฅ๐ฟ๐ฆ)โ๐)(โจ(๐นโ๐ฅ), (๐พโ๐ฅ)โฉ ยท (๐พโ๐ฆ))(๐ดโ๐ฅ)) โ ((๐ดโ๐)(โจ(๐นโ๐), (๐นโ๐)โฉ ยท (๐พโ๐))((๐๐บ๐)โ๐
)) = (((๐๐ฟ๐)โ๐
)(โจ(๐นโ๐), (๐พโ๐)โฉ ยท (๐พโ๐))(๐ดโ๐)))) |
47 | 26, 46 | rspcdv 3572 |
. . . 4
โข (((๐ โง ๐ฅ = ๐) โง ๐ฆ = ๐) โ (โ๐ โ (๐ฅ๐ป๐ฆ)((๐ดโ๐ฆ)(โจ(๐นโ๐ฅ), (๐นโ๐ฆ)โฉ ยท (๐พโ๐ฆ))((๐ฅ๐บ๐ฆ)โ๐)) = (((๐ฅ๐ฟ๐ฆ)โ๐)(โจ(๐นโ๐ฅ), (๐พโ๐ฅ)โฉ ยท (๐พโ๐ฆ))(๐ดโ๐ฅ)) โ ((๐ดโ๐)(โจ(๐นโ๐), (๐นโ๐)โฉ ยท (๐พโ๐))((๐๐บ๐)โ๐
)) = (((๐๐ฟ๐)โ๐
)(โจ(๐นโ๐), (๐พโ๐)โฉ ยท (๐พโ๐))(๐ดโ๐)))) |
48 | 20, 47 | rspcimdv 3570 |
. . 3
โข ((๐ โง ๐ฅ = ๐) โ (โ๐ฆ โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)((๐ดโ๐ฆ)(โจ(๐นโ๐ฅ), (๐นโ๐ฆ)โฉ ยท (๐พโ๐ฆ))((๐ฅ๐บ๐ฆ)โ๐)) = (((๐ฅ๐ฟ๐ฆ)โ๐)(โจ(๐นโ๐ฅ), (๐พโ๐ฅ)โฉ ยท (๐พโ๐ฆ))(๐ดโ๐ฅ)) โ ((๐ดโ๐)(โจ(๐นโ๐), (๐นโ๐)โฉ ยท (๐พโ๐))((๐๐บ๐)โ๐
)) = (((๐๐ฟ๐)โ๐
)(โจ(๐นโ๐), (๐พโ๐)โฉ ยท (๐พโ๐))(๐ดโ๐)))) |
49 | 18, 48 | rspcimdv 3570 |
. 2
โข (๐ โ (โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)((๐ดโ๐ฆ)(โจ(๐นโ๐ฅ), (๐นโ๐ฆ)โฉ ยท (๐พโ๐ฆ))((๐ฅ๐บ๐ฆ)โ๐)) = (((๐ฅ๐ฟ๐ฆ)โ๐)(โจ(๐นโ๐ฅ), (๐พโ๐ฅ)โฉ ยท (๐พโ๐ฆ))(๐ดโ๐ฅ)) โ ((๐ดโ๐)(โจ(๐นโ๐), (๐นโ๐)โฉ ยท (๐พโ๐))((๐๐บ๐)โ๐
)) = (((๐๐ฟ๐)โ๐
)(โจ(๐นโ๐), (๐พโ๐)โฉ ยท (๐พโ๐))(๐ดโ๐)))) |
50 | 17, 49 | mpd 15 |
1
โข (๐ โ ((๐ดโ๐)(โจ(๐นโ๐), (๐นโ๐)โฉ ยท (๐พโ๐))((๐๐บ๐)โ๐
)) = (((๐๐ฟ๐)โ๐
)(โจ(๐นโ๐), (๐พโ๐)โฉ ยท (๐พโ๐))(๐ดโ๐))) |