Step | Hyp | Ref
| Expression |
1 | | df-adjh 31370 |
. 2
โข
adjโ = {โจ๐ก, ๐ขโฉ โฃ (๐ก: โโถ โ โง ๐ข: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
((๐กโ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐ขโ๐ฆ)))} |
2 | | eqcom 2738 |
. . . . . . 7
โข (((๐กโ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih (๐ขโ๐ฆ)) โ (๐ฅ ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)) |
3 | 2 | 2ralbii 3127 |
. . . . . 6
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐กโ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐ขโ๐ฆ)) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)) |
4 | | adjsym 31354 |
. . . . . 6
โข ((๐ก: โโถ โ โง
๐ข: โโถ โ)
โ (โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐กโ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐ขโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ))) |
5 | 3, 4 | bitr4id 290 |
. . . . 5
โข ((๐ก: โโถ โ โง
๐ข: โโถ โ)
โ (โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐กโ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐ขโ๐ฆ)) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐กโ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ))) |
6 | 5 | pm5.32i 574 |
. . . 4
โข (((๐ก: โโถ โ โง
๐ข: โโถ โ)
โง โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐กโ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐ขโ๐ฆ))) โ ((๐ก: โโถ โ โง ๐ข: โโถ โ) โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐กโ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ))) |
7 | | df-3an 1088 |
. . . 4
โข ((๐ก: โโถ โ โง
๐ข: โโถ โ
โง โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐กโ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐ขโ๐ฆ))) โ ((๐ก: โโถ โ โง ๐ข: โโถ โ) โง
โ๐ฅ โ โ
โ๐ฆ โ โ
((๐กโ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐ขโ๐ฆ)))) |
8 | | df-3an 1088 |
. . . 4
โข ((๐ก: โโถ โ โง
๐ข: โโถ โ
โง โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐กโ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) โ ((๐ก: โโถ โ โง ๐ข: โโถ โ) โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐กโ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ))) |
9 | 6, 7, 8 | 3bitr4i 303 |
. . 3
โข ((๐ก: โโถ โ โง
๐ข: โโถ โ
โง โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐กโ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐ขโ๐ฆ))) โ (๐ก: โโถ โ โง ๐ข: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐กโ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ))) |
10 | 9 | opabbii 5215 |
. 2
โข
{โจ๐ก, ๐ขโฉ โฃ (๐ก: โโถ โ โง
๐ข: โโถ โ
โง โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐กโ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐ขโ๐ฆ)))} = {โจ๐ก, ๐ขโฉ โฃ (๐ก: โโถ โ โง ๐ข: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐กโ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ))} |
11 | 1, 10 | eqtri 2759 |
1
โข
adjโ = {โจ๐ก, ๐ขโฉ โฃ (๐ก: โโถ โ โง ๐ข: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐กโ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ))} |