Step | Hyp | Ref
| Expression |
1 | | cnvopab 6139 |
. . 3
โข โก{โจ๐ข, ๐กโฉ โฃ (๐ข: โโถ โ โง ๐ก: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))} = {โจ๐ก, ๐ขโฉ โฃ (๐ข: โโถ โ โง ๐ก: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))} |
2 | | 3ancoma 1099 |
. . . . 5
โข ((๐ข: โโถ โ โง
๐ก: โโถ โ
โง โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)) โ (๐ก: โโถ โ โง ๐ข: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))) |
3 | | ffvelcdm 7084 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ข: โโถ โ โง
๐ฆ โ โ) โ
(๐ขโ๐ฆ) โ โ) |
4 | | ax-his1 30335 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ขโ๐ฆ) โ โ โง ๐ฅ โ โ) โ ((๐ขโ๐ฆ) ยทih ๐ฅ) = (โโ(๐ฅ
ยทih (๐ขโ๐ฆ)))) |
5 | 3, 4 | sylan 581 |
. . . . . . . . . . . . . . . . 17
โข (((๐ข: โโถ โ โง
๐ฆ โ โ) โง
๐ฅ โ โ) โ
((๐ขโ๐ฆ)
ยทih ๐ฅ) = (โโ(๐ฅ ยทih (๐ขโ๐ฆ)))) |
6 | 5 | adantrl 715 |
. . . . . . . . . . . . . . . 16
โข (((๐ข: โโถ โ โง
๐ฆ โ โ) โง
(๐ก: โโถ โ
โง ๐ฅ โ โ))
โ ((๐ขโ๐ฆ)
ยทih ๐ฅ) = (โโ(๐ฅ ยทih (๐ขโ๐ฆ)))) |
7 | | ffvelcdm 7084 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ก: โโถ โ โง
๐ฅ โ โ) โ
(๐กโ๐ฅ) โ โ) |
8 | | ax-his1 30335 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ โง (๐กโ๐ฅ) โ โ) โ (๐ฆ ยทih (๐กโ๐ฅ)) = (โโ((๐กโ๐ฅ) ยทih ๐ฆ))) |
9 | 7, 8 | sylan2 594 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ โง (๐ก: โโถ โ โง
๐ฅ โ โ)) โ
(๐ฆ
ยทih (๐กโ๐ฅ)) = (โโ((๐กโ๐ฅ) ยทih ๐ฆ))) |
10 | 9 | adantll 713 |
. . . . . . . . . . . . . . . 16
โข (((๐ข: โโถ โ โง
๐ฆ โ โ) โง
(๐ก: โโถ โ
โง ๐ฅ โ โ))
โ (๐ฆ
ยทih (๐กโ๐ฅ)) = (โโ((๐กโ๐ฅ) ยทih ๐ฆ))) |
11 | 6, 10 | eqeq12d 2749 |
. . . . . . . . . . . . . . 15
โข (((๐ข: โโถ โ โง
๐ฆ โ โ) โง
(๐ก: โโถ โ
โง ๐ฅ โ โ))
โ (((๐ขโ๐ฆ)
ยทih ๐ฅ) = (๐ฆ ยทih (๐กโ๐ฅ)) โ (โโ(๐ฅ ยทih (๐ขโ๐ฆ))) = (โโ((๐กโ๐ฅ) ยทih ๐ฆ)))) |
12 | 11 | ancoms 460 |
. . . . . . . . . . . . . 14
โข (((๐ก: โโถ โ โง
๐ฅ โ โ) โง
(๐ข: โโถ โ
โง ๐ฆ โ โ))
โ (((๐ขโ๐ฆ)
ยทih ๐ฅ) = (๐ฆ ยทih (๐กโ๐ฅ)) โ (โโ(๐ฅ ยทih (๐ขโ๐ฆ))) = (โโ((๐กโ๐ฅ) ยทih ๐ฆ)))) |
13 | | hicl 30333 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฅ โ โ โง (๐ขโ๐ฆ) โ โ) โ (๐ฅ ยทih (๐ขโ๐ฆ)) โ โ) |
14 | 3, 13 | sylan2 594 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โ โ โง (๐ข: โโถ โ โง
๐ฆ โ โ)) โ
(๐ฅ
ยทih (๐ขโ๐ฆ)) โ โ) |
15 | 14 | adantll 713 |
. . . . . . . . . . . . . . 15
โข (((๐ก: โโถ โ โง
๐ฅ โ โ) โง
(๐ข: โโถ โ
โง ๐ฆ โ โ))
โ (๐ฅ
ยทih (๐ขโ๐ฆ)) โ โ) |
16 | | hicl 30333 |
. . . . . . . . . . . . . . . . 17
โข (((๐กโ๐ฅ) โ โ โง ๐ฆ โ โ) โ ((๐กโ๐ฅ) ยทih ๐ฆ) โ
โ) |
17 | 7, 16 | sylan 581 |
. . . . . . . . . . . . . . . 16
โข (((๐ก: โโถ โ โง
๐ฅ โ โ) โง
๐ฆ โ โ) โ
((๐กโ๐ฅ)
ยทih ๐ฆ) โ โ) |
18 | 17 | adantrl 715 |
. . . . . . . . . . . . . . 15
โข (((๐ก: โโถ โ โง
๐ฅ โ โ) โง
(๐ข: โโถ โ
โง ๐ฆ โ โ))
โ ((๐กโ๐ฅ)
ยทih ๐ฆ) โ โ) |
19 | | cj11 15109 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ
ยทih (๐ขโ๐ฆ)) โ โ โง ((๐กโ๐ฅ) ยทih ๐ฆ) โ โ) โ
((โโ(๐ฅ
ยทih (๐ขโ๐ฆ))) = (โโ((๐กโ๐ฅ) ยทih ๐ฆ)) โ (๐ฅ ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))) |
20 | 15, 18, 19 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข (((๐ก: โโถ โ โง
๐ฅ โ โ) โง
(๐ข: โโถ โ
โง ๐ฆ โ โ))
โ ((โโ(๐ฅ
ยทih (๐ขโ๐ฆ))) = (โโ((๐กโ๐ฅ) ยทih ๐ฆ)) โ (๐ฅ ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))) |
21 | 12, 20 | bitr2d 280 |
. . . . . . . . . . . . 13
โข (((๐ก: โโถ โ โง
๐ฅ โ โ) โง
(๐ข: โโถ โ
โง ๐ฆ โ โ))
โ ((๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) โ ((๐ขโ๐ฆ) ยทih ๐ฅ) = (๐ฆ ยทih (๐กโ๐ฅ)))) |
22 | 21 | an4s 659 |
. . . . . . . . . . . 12
โข (((๐ก: โโถ โ โง
๐ข: โโถ โ)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โ ((๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) โ ((๐ขโ๐ฆ) ยทih ๐ฅ) = (๐ฆ ยทih (๐กโ๐ฅ)))) |
23 | 22 | anassrs 469 |
. . . . . . . . . . 11
โข ((((๐ก: โโถ โ โง
๐ข: โโถ โ)
โง ๐ฅ โ โ)
โง ๐ฆ โ โ)
โ ((๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) โ ((๐ขโ๐ฆ) ยทih ๐ฅ) = (๐ฆ ยทih (๐กโ๐ฅ)))) |
24 | | eqcom 2740 |
. . . . . . . . . . 11
โข (((๐ขโ๐ฆ) ยทih ๐ฅ) = (๐ฆ ยทih (๐กโ๐ฅ)) โ (๐ฆ ยทih (๐กโ๐ฅ)) = ((๐ขโ๐ฆ) ยทih ๐ฅ)) |
25 | 23, 24 | bitrdi 287 |
. . . . . . . . . 10
โข ((((๐ก: โโถ โ โง
๐ข: โโถ โ)
โง ๐ฅ โ โ)
โง ๐ฆ โ โ)
โ ((๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) โ (๐ฆ ยทih (๐กโ๐ฅ)) = ((๐ขโ๐ฆ) ยทih ๐ฅ))) |
26 | 25 | ralbidva 3176 |
. . . . . . . . 9
โข (((๐ก: โโถ โ โง
๐ข: โโถ โ)
โง ๐ฅ โ โ)
โ (โ๐ฆ โ
โ (๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) โ โ๐ฆ โ โ (๐ฆ
ยทih (๐กโ๐ฅ)) = ((๐ขโ๐ฆ) ยทih ๐ฅ))) |
27 | 26 | ralbidva 3176 |
. . . . . . . 8
โข ((๐ก: โโถ โ โง
๐ข: โโถ โ)
โ (โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฆ
ยทih (๐กโ๐ฅ)) = ((๐ขโ๐ฆ) ยทih ๐ฅ))) |
28 | | ralcom 3287 |
. . . . . . . 8
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฆ
ยทih (๐กโ๐ฅ)) = ((๐ขโ๐ฆ) ยทih ๐ฅ) โ โ๐ฆ โ โ โ๐ฅ โ โ (๐ฆ
ยทih (๐กโ๐ฅ)) = ((๐ขโ๐ฆ) ยทih ๐ฅ)) |
29 | 27, 28 | bitrdi 287 |
. . . . . . 7
โข ((๐ก: โโถ โ โง
๐ข: โโถ โ)
โ (โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) โ โ๐ฆ โ โ โ๐ฅ โ โ (๐ฆ
ยทih (๐กโ๐ฅ)) = ((๐ขโ๐ฆ) ยทih ๐ฅ))) |
30 | 29 | pm5.32i 576 |
. . . . . 6
โข (((๐ก: โโถ โ โง
๐ข: โโถ โ)
โง โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)) โ ((๐ก: โโถ โ โง ๐ข: โโถ โ) โง
โ๐ฆ โ โ
โ๐ฅ โ โ
(๐ฆ
ยทih (๐กโ๐ฅ)) = ((๐ขโ๐ฆ) ยทih ๐ฅ))) |
31 | | df-3an 1090 |
. . . . . 6
โข ((๐ก: โโถ โ โง
๐ข: โโถ โ
โง โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)) โ ((๐ก: โโถ โ โง ๐ข: โโถ โ) โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))) |
32 | | df-3an 1090 |
. . . . . 6
โข ((๐ก: โโถ โ โง
๐ข: โโถ โ
โง โ๐ฆ โ
โ โ๐ฅ โ
โ (๐ฆ
ยทih (๐กโ๐ฅ)) = ((๐ขโ๐ฆ) ยทih ๐ฅ)) โ ((๐ก: โโถ โ โง ๐ข: โโถ โ) โง
โ๐ฆ โ โ
โ๐ฅ โ โ
(๐ฆ
ยทih (๐กโ๐ฅ)) = ((๐ขโ๐ฆ) ยทih ๐ฅ))) |
33 | 30, 31, 32 | 3bitr4i 303 |
. . . . 5
โข ((๐ก: โโถ โ โง
๐ข: โโถ โ
โง โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)) โ (๐ก: โโถ โ โง ๐ข: โโถ โ โง
โ๐ฆ โ โ
โ๐ฅ โ โ
(๐ฆ
ยทih (๐กโ๐ฅ)) = ((๐ขโ๐ฆ) ยทih ๐ฅ))) |
34 | 2, 33 | bitri 275 |
. . . 4
โข ((๐ข: โโถ โ โง
๐ก: โโถ โ
โง โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)) โ (๐ก: โโถ โ โง ๐ข: โโถ โ โง
โ๐ฆ โ โ
โ๐ฅ โ โ
(๐ฆ
ยทih (๐กโ๐ฅ)) = ((๐ขโ๐ฆ) ยทih ๐ฅ))) |
35 | 34 | opabbii 5216 |
. . 3
โข
{โจ๐ก, ๐ขโฉ โฃ (๐ข: โโถ โ โง
๐ก: โโถ โ
โง โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))} = {โจ๐ก, ๐ขโฉ โฃ (๐ก: โโถ โ โง ๐ข: โโถ โ โง
โ๐ฆ โ โ
โ๐ฅ โ โ
(๐ฆ
ยทih (๐กโ๐ฅ)) = ((๐ขโ๐ฆ) ยทih ๐ฅ))} |
36 | 1, 35 | eqtri 2761 |
. 2
โข โก{โจ๐ข, ๐กโฉ โฃ (๐ข: โโถ โ โง ๐ก: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))} = {โจ๐ก, ๐ขโฉ โฃ (๐ก: โโถ โ โง ๐ข: โโถ โ โง
โ๐ฆ โ โ
โ๐ฅ โ โ
(๐ฆ
ยทih (๐กโ๐ฅ)) = ((๐ขโ๐ฆ) ยทih ๐ฅ))} |
37 | | dfadj2 31138 |
. . 3
โข
adjโ = {โจ๐ข, ๐กโฉ โฃ (๐ข: โโถ โ โง ๐ก: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))} |
38 | 37 | cnveqi 5875 |
. 2
โข โกadjโ = โก{โจ๐ข, ๐กโฉ โฃ (๐ข: โโถ โ โง ๐ก: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))} |
39 | | dfadj2 31138 |
. 2
โข
adjโ = {โจ๐ก, ๐ขโฉ โฃ (๐ก: โโถ โ โง ๐ข: โโถ โ โง
โ๐ฆ โ โ
โ๐ฅ โ โ
(๐ฆ
ยทih (๐กโ๐ฅ)) = ((๐ขโ๐ฆ) ยทih ๐ฅ))} |
40 | 36, 38, 39 | 3eqtr4i 2771 |
1
โข โกadjโ =
adjโ |