Step | Hyp | Ref
| Expression |
1 | | funadj 30633 |
. . . . . . 7
โข Fun
adjโ |
2 | | funfvop 6996 |
. . . . . . 7
โข ((Fun
adjโ โง ๐ โ dom adjโ) โ
โจ๐,
(adjโโ๐)โฉ โ
adjโ) |
3 | 1, 2 | mpan 689 |
. . . . . 6
โข (๐ โ dom
adjโ โ โจ๐, (adjโโ๐)โฉ โ
adjโ) |
4 | | dfadj2 30632 |
. . . . . 6
โข
adjโ = {โจ๐ง, ๐คโฉ โฃ (๐ง: โโถ โ โง ๐ค: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐งโ๐ฆ)) = ((๐คโ๐ฅ) ยทih ๐ฆ))} |
5 | 3, 4 | eleqtrdi 2849 |
. . . . 5
โข (๐ โ dom
adjโ โ โจ๐, (adjโโ๐)โฉ โ {โจ๐ง, ๐คโฉ โฃ (๐ง: โโถ โ โง ๐ค: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐งโ๐ฆ)) = ((๐คโ๐ฅ) ยทih ๐ฆ))}) |
6 | | fvex 6851 |
. . . . . 6
โข
(adjโโ๐) โ V |
7 | | feq1 6645 |
. . . . . . . 8
โข (๐ง = ๐ โ (๐ง: โโถ โ โ ๐: โโถ
โ)) |
8 | | fveq1 6837 |
. . . . . . . . . . 11
โข (๐ง = ๐ โ (๐งโ๐ฆ) = (๐โ๐ฆ)) |
9 | 8 | oveq2d 7366 |
. . . . . . . . . 10
โข (๐ง = ๐ โ (๐ฅ ยทih (๐งโ๐ฆ)) = (๐ฅ ยทih (๐โ๐ฆ))) |
10 | 9 | eqeq1d 2740 |
. . . . . . . . 9
โข (๐ง = ๐ โ ((๐ฅ ยทih (๐งโ๐ฆ)) = ((๐คโ๐ฅ) ยทih ๐ฆ) โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐คโ๐ฅ) ยทih ๐ฆ))) |
11 | 10 | 2ralbidv 3211 |
. . . . . . . 8
โข (๐ง = ๐ โ (โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐งโ๐ฆ)) = ((๐คโ๐ฅ) ยทih ๐ฆ) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐คโ๐ฅ) ยทih ๐ฆ))) |
12 | 7, 11 | 3anbi13d 1439 |
. . . . . . 7
โข (๐ง = ๐ โ ((๐ง: โโถ โ โง ๐ค: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐งโ๐ฆ)) = ((๐คโ๐ฅ) ยทih ๐ฆ)) โ (๐: โโถ โ โง ๐ค: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐คโ๐ฅ) ยทih ๐ฆ)))) |
13 | | feq1 6645 |
. . . . . . . 8
โข (๐ค =
(adjโโ๐) โ (๐ค: โโถ โ โ
(adjโโ๐): โโถ
โ)) |
14 | | fveq1 6837 |
. . . . . . . . . . 11
โข (๐ค =
(adjโโ๐) โ (๐คโ๐ฅ) = ((adjโโ๐)โ๐ฅ)) |
15 | 14 | oveq1d 7365 |
. . . . . . . . . 10
โข (๐ค =
(adjโโ๐) โ ((๐คโ๐ฅ) ยทih ๐ฆ) =
(((adjโโ๐)โ๐ฅ) ยทih ๐ฆ)) |
16 | 15 | eqeq2d 2749 |
. . . . . . . . 9
โข (๐ค =
(adjโโ๐) โ ((๐ฅ ยทih (๐โ๐ฆ)) = ((๐คโ๐ฅ) ยทih ๐ฆ) โ (๐ฅ ยทih (๐โ๐ฆ)) = (((adjโโ๐)โ๐ฅ) ยทih ๐ฆ))) |
17 | 16 | 2ralbidv 3211 |
. . . . . . . 8
โข (๐ค =
(adjโโ๐) โ (โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐คโ๐ฅ) ยทih ๐ฆ) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = (((adjโโ๐)โ๐ฅ) ยทih ๐ฆ))) |
18 | 13, 17 | 3anbi23d 1440 |
. . . . . . 7
โข (๐ค =
(adjโโ๐) โ ((๐: โโถ โ โง ๐ค: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐คโ๐ฅ) ยทih ๐ฆ)) โ (๐: โโถ โ โง
(adjโโ๐): โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = (((adjโโ๐)โ๐ฅ) ยทih ๐ฆ)))) |
19 | 12, 18 | opelopabg 5493 |
. . . . . 6
โข ((๐ โ dom
adjโ โง (adjโโ๐) โ V) โ (โจ๐, (adjโโ๐)โฉ โ {โจ๐ง, ๐คโฉ โฃ (๐ง: โโถ โ โง ๐ค: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐งโ๐ฆ)) = ((๐คโ๐ฅ) ยทih ๐ฆ))} โ (๐: โโถ โ โง
(adjโโ๐): โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = (((adjโโ๐)โ๐ฅ) ยทih ๐ฆ)))) |
20 | 6, 19 | mpan2 690 |
. . . . 5
โข (๐ โ dom
adjโ โ (โจ๐, (adjโโ๐)โฉ โ {โจ๐ง, ๐คโฉ โฃ (๐ง: โโถ โ โง ๐ค: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐งโ๐ฆ)) = ((๐คโ๐ฅ) ยทih ๐ฆ))} โ (๐: โโถ โ โง
(adjโโ๐): โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = (((adjโโ๐)โ๐ฅ) ยทih ๐ฆ)))) |
21 | 5, 20 | mpbid 231 |
. . . 4
โข (๐ โ dom
adjโ โ (๐: โโถ โ โง
(adjโโ๐): โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = (((adjโโ๐)โ๐ฅ) ยทih ๐ฆ))) |
22 | 21 | simp3d 1145 |
. . 3
โข (๐ โ dom
adjโ โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = (((adjโโ๐)โ๐ฅ) ยทih ๐ฆ)) |
23 | | oveq1 7357 |
. . . . 5
โข (๐ฅ = ๐ด โ (๐ฅ ยทih (๐โ๐ฆ)) = (๐ด ยทih (๐โ๐ฆ))) |
24 | | fveq2 6838 |
. . . . . 6
โข (๐ฅ = ๐ด โ ((adjโโ๐)โ๐ฅ) = ((adjโโ๐)โ๐ด)) |
25 | 24 | oveq1d 7365 |
. . . . 5
โข (๐ฅ = ๐ด โ
(((adjโโ๐)โ๐ฅ) ยทih ๐ฆ) =
(((adjโโ๐)โ๐ด) ยทih ๐ฆ)) |
26 | 23, 25 | eqeq12d 2754 |
. . . 4
โข (๐ฅ = ๐ด โ ((๐ฅ ยทih (๐โ๐ฆ)) = (((adjโโ๐)โ๐ฅ) ยทih ๐ฆ) โ (๐ด ยทih (๐โ๐ฆ)) = (((adjโโ๐)โ๐ด) ยทih ๐ฆ))) |
27 | | fveq2 6838 |
. . . . . 6
โข (๐ฆ = ๐ต โ (๐โ๐ฆ) = (๐โ๐ต)) |
28 | 27 | oveq2d 7366 |
. . . . 5
โข (๐ฆ = ๐ต โ (๐ด ยทih (๐โ๐ฆ)) = (๐ด ยทih (๐โ๐ต))) |
29 | | oveq2 7358 |
. . . . 5
โข (๐ฆ = ๐ต โ
(((adjโโ๐)โ๐ด) ยทih ๐ฆ) =
(((adjโโ๐)โ๐ด) ยทih ๐ต)) |
30 | 28, 29 | eqeq12d 2754 |
. . . 4
โข (๐ฆ = ๐ต โ ((๐ด ยทih (๐โ๐ฆ)) = (((adjโโ๐)โ๐ด) ยทih ๐ฆ) โ (๐ด ยทih (๐โ๐ต)) = (((adjโโ๐)โ๐ด) ยทih ๐ต))) |
31 | 26, 30 | rspc2v 3589 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = (((adjโโ๐)โ๐ฅ) ยทih ๐ฆ) โ (๐ด ยทih (๐โ๐ต)) = (((adjโโ๐)โ๐ด) ยทih ๐ต))) |
32 | 22, 31 | syl5com 31 |
. 2
โข (๐ โ dom
adjโ โ ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยทih (๐โ๐ต)) = (((adjโโ๐)โ๐ด) ยทih ๐ต))) |
33 | 32 | 3impib 1117 |
1
โข ((๐ โ dom
adjโ โง ๐ด โ โ โง ๐ต โ โ) โ (๐ด ยทih (๐โ๐ต)) = (((adjโโ๐)โ๐ด) ยทih ๐ต)) |