Step | Hyp | Ref
| Expression |
1 | | dmadjop 30872 |
. . . . 5
โข (๐ โ dom
adjโ โ ๐: โโถ โ) |
2 | 1 | biantrurd 534 |
. . . 4
โข (๐ โ dom
adjโ โ ((๐ข: โโถ โ โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) โ (๐: โโถ โ โง (๐ข: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ))))) |
3 | | ax-hilex 29983 |
. . . . . 6
โข โ
โ V |
4 | 3, 3 | elmap 8816 |
. . . . 5
โข (๐ข โ ( โ
โm โ) โ ๐ข: โโถ โ) |
5 | 4 | anbi1i 625 |
. . . 4
โข ((๐ข โ ( โ
โm โ) โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) โ (๐ข: โโถ โ โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ))) |
6 | | 3anass 1096 |
. . . 4
โข ((๐: โโถ โ โง
๐ข: โโถ โ
โง โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) โ (๐: โโถ โ โง (๐ข: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)))) |
7 | 2, 5, 6 | 3bitr4g 314 |
. . 3
โข (๐ โ dom
adjโ โ ((๐ข โ ( โ โm โ)
โง โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) โ (๐: โโถ โ โง ๐ข: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)))) |
8 | 7 | iotabidv 6485 |
. 2
โข (๐ โ dom
adjโ โ (โฉ๐ข(๐ข โ ( โ โm โ)
โง โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ))) = (โฉ๐ข(๐: โโถ โ โง ๐ข: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)))) |
9 | | df-riota 7318 |
. . 3
โข
(โฉ๐ข
โ ( โ โm โ)โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) = (โฉ๐ข(๐ข โ ( โ โm โ)
โง โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ))) |
10 | 9 | a1i 11 |
. 2
โข (๐ โ dom
adjโ โ (โฉ๐ข โ ( โ โm
โ)โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) = (โฉ๐ข(๐ข โ ( โ โm โ)
โง โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)))) |
11 | | dfadj2 30869 |
. . 3
โข
adjโ = {โจ๐ก, ๐ขโฉ โฃ (๐ก: โโถ โ โง ๐ข: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐กโ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ))} |
12 | | feq1 6654 |
. . . 4
โข (๐ก = ๐ โ (๐ก: โโถ โ โ ๐: โโถ
โ)) |
13 | | fveq1 6846 |
. . . . . . 7
โข (๐ก = ๐ โ (๐กโ๐ฆ) = (๐โ๐ฆ)) |
14 | 13 | oveq2d 7378 |
. . . . . 6
โข (๐ก = ๐ โ (๐ฅ ยทih (๐กโ๐ฆ)) = (๐ฅ ยทih (๐โ๐ฆ))) |
15 | 14 | eqeq1d 2739 |
. . . . 5
โข (๐ก = ๐ โ ((๐ฅ ยทih (๐กโ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ) โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ))) |
16 | 15 | 2ralbidv 3213 |
. . . 4
โข (๐ก = ๐ โ (โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐กโ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ))) |
17 | 12, 16 | 3anbi13d 1439 |
. . 3
โข (๐ก = ๐ โ ((๐ก: โโถ โ โง ๐ข: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐กโ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) โ (๐: โโถ โ โง ๐ข: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)))) |
18 | 11, 17 | fvopab5 6985 |
. 2
โข (๐ โ dom
adjโ โ (adjโโ๐) = (โฉ๐ข(๐: โโถ โ โง ๐ข: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)))) |
19 | 8, 10, 18 | 3eqtr4rd 2788 |
1
โข (๐ โ dom
adjโ โ (adjโโ๐) = (โฉ๐ข โ ( โ โm
โ)โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ))) |