Step | Hyp | Ref
| Expression |
1 | | adjcl 30703 |
. . 3
โข ((๐ โ dom
adjโ โง ๐ด โ โ) โ
((adjโโ๐)โ๐ด) โ โ) |
2 | | eqcom 2744 |
. . . . . . 7
โข (((๐โ๐ฅ) ยทih ๐ด) = (๐ฅ ยทih ๐ค) โ (๐ฅ ยทih ๐ค) = ((๐โ๐ฅ) ยทih ๐ด)) |
3 | | adj2 30705 |
. . . . . . . . . 10
โข ((๐ โ dom
adjโ โง ๐ฅ โ โ โง ๐ด โ โ) โ ((๐โ๐ฅ) ยทih ๐ด) = (๐ฅ ยทih
((adjโโ๐)โ๐ด))) |
4 | 3 | 3com23 1126 |
. . . . . . . . 9
โข ((๐ โ dom
adjโ โง ๐ด โ โ โง ๐ฅ โ โ) โ ((๐โ๐ฅ) ยทih ๐ด) = (๐ฅ ยทih
((adjโโ๐)โ๐ด))) |
5 | 4 | 3expa 1118 |
. . . . . . . 8
โข (((๐ โ dom
adjโ โง ๐ด โ โ) โง ๐ฅ โ โ) โ ((๐โ๐ฅ) ยทih ๐ด) = (๐ฅ ยทih
((adjโโ๐)โ๐ด))) |
6 | 5 | eqeq2d 2748 |
. . . . . . 7
โข (((๐ โ dom
adjโ โง ๐ด โ โ) โง ๐ฅ โ โ) โ ((๐ฅ ยทih ๐ค) = ((๐โ๐ฅ) ยทih ๐ด) โ (๐ฅ ยทih ๐ค) = (๐ฅ ยทih
((adjโโ๐)โ๐ด)))) |
7 | 2, 6 | bitrid 282 |
. . . . . 6
โข (((๐ โ dom
adjโ โง ๐ด โ โ) โง ๐ฅ โ โ) โ (((๐โ๐ฅ) ยทih ๐ด) = (๐ฅ ยทih ๐ค) โ (๐ฅ ยทih ๐ค) = (๐ฅ ยทih
((adjโโ๐)โ๐ด)))) |
8 | 7 | ralbidva 3170 |
. . . . 5
โข ((๐ โ dom
adjโ โง ๐ด โ โ) โ (โ๐ฅ โ โ ((๐โ๐ฅ) ยทih ๐ด) = (๐ฅ ยทih ๐ค) โ โ๐ฅ โ โ (๐ฅ
ยทih ๐ค) = (๐ฅ ยทih
((adjโโ๐)โ๐ด)))) |
9 | 8 | adantr 481 |
. . . 4
โข (((๐ โ dom
adjโ โง ๐ด โ โ) โง ๐ค โ โ) โ (โ๐ฅ โ โ ((๐โ๐ฅ) ยทih ๐ด) = (๐ฅ ยทih ๐ค) โ โ๐ฅ โ โ (๐ฅ
ยทih ๐ค) = (๐ฅ ยทih
((adjโโ๐)โ๐ด)))) |
10 | | simpr 485 |
. . . . 5
โข (((๐ โ dom
adjโ โง ๐ด โ โ) โง ๐ค โ โ) โ ๐ค โ โ) |
11 | 1 | adantr 481 |
. . . . 5
โข (((๐ โ dom
adjโ โง ๐ด โ โ) โง ๐ค โ โ) โ
((adjโโ๐)โ๐ด) โ โ) |
12 | | hial2eq2 29878 |
. . . . 5
โข ((๐ค โ โ โง
((adjโโ๐)โ๐ด) โ โ) โ (โ๐ฅ โ โ (๐ฅ
ยทih ๐ค) = (๐ฅ ยทih
((adjโโ๐)โ๐ด)) โ ๐ค = ((adjโโ๐)โ๐ด))) |
13 | 10, 11, 12 | syl2anc 584 |
. . . 4
โข (((๐ โ dom
adjโ โง ๐ด โ โ) โง ๐ค โ โ) โ (โ๐ฅ โ โ (๐ฅ
ยทih ๐ค) = (๐ฅ ยทih
((adjโโ๐)โ๐ด)) โ ๐ค = ((adjโโ๐)โ๐ด))) |
14 | 9, 13 | bitrd 278 |
. . 3
โข (((๐ โ dom
adjโ โง ๐ด โ โ) โง ๐ค โ โ) โ (โ๐ฅ โ โ ((๐โ๐ฅ) ยทih ๐ด) = (๐ฅ ยทih ๐ค) โ ๐ค = ((adjโโ๐)โ๐ด))) |
15 | 1, 14 | riota5 7337 |
. 2
โข ((๐ โ dom
adjโ โง ๐ด โ โ) โ (โฉ๐ค โ โ โ๐ฅ โ โ ((๐โ๐ฅ) ยทih ๐ด) = (๐ฅ ยทih ๐ค)) =
((adjโโ๐)โ๐ด)) |
16 | 15 | eqcomd 2743 |
1
โข ((๐ โ dom
adjโ โง ๐ด โ โ) โ
((adjโโ๐)โ๐ด) = (โฉ๐ค โ โ โ๐ฅ โ โ ((๐โ๐ฅ) ยทih ๐ด) = (๐ฅ ยทih ๐ค))) |