Step | Hyp | Ref
| Expression |
1 | | adj1 31224 |
. . . 4
โข ((๐ โ dom
adjโ โง ๐ต โ โ โง ๐ด โ โ) โ (๐ต ยทih (๐โ๐ด)) = (((adjโโ๐)โ๐ต) ยทih ๐ด)) |
2 | | simp2 1137 |
. . . . 5
โข ((๐ โ dom
adjโ โง ๐ต โ โ โง ๐ด โ โ) โ ๐ต โ โ) |
3 | | dmadjop 31179 |
. . . . . . 7
โข (๐ โ dom
adjโ โ ๐: โโถ โ) |
4 | 3 | ffvelcdmda 7086 |
. . . . . 6
โข ((๐ โ dom
adjโ โง ๐ด โ โ) โ (๐โ๐ด) โ โ) |
5 | 4 | 3adant2 1131 |
. . . . 5
โข ((๐ โ dom
adjโ โง ๐ต โ โ โง ๐ด โ โ) โ (๐โ๐ด) โ โ) |
6 | | ax-his1 30373 |
. . . . 5
โข ((๐ต โ โ โง (๐โ๐ด) โ โ) โ (๐ต ยทih (๐โ๐ด)) = (โโ((๐โ๐ด) ยทih ๐ต))) |
7 | 2, 5, 6 | syl2anc 584 |
. . . 4
โข ((๐ โ dom
adjโ โง ๐ต โ โ โง ๐ด โ โ) โ (๐ต ยทih (๐โ๐ด)) = (โโ((๐โ๐ด) ยทih ๐ต))) |
8 | | adjcl 31223 |
. . . . . 6
โข ((๐ โ dom
adjโ โง ๐ต โ โ) โ
((adjโโ๐)โ๐ต) โ โ) |
9 | 8 | 3adant3 1132 |
. . . . 5
โข ((๐ โ dom
adjโ โง ๐ต โ โ โง ๐ด โ โ) โ
((adjโโ๐)โ๐ต) โ โ) |
10 | | simp3 1138 |
. . . . 5
โข ((๐ โ dom
adjโ โง ๐ต โ โ โง ๐ด โ โ) โ ๐ด โ โ) |
11 | | ax-his1 30373 |
. . . . 5
โข
((((adjโโ๐)โ๐ต) โ โ โง ๐ด โ โ) โ
(((adjโโ๐)โ๐ต) ยทih ๐ด) = (โโ(๐ด
ยทih ((adjโโ๐)โ๐ต)))) |
12 | 9, 10, 11 | syl2anc 584 |
. . . 4
โข ((๐ โ dom
adjโ โง ๐ต โ โ โง ๐ด โ โ) โ
(((adjโโ๐)โ๐ต) ยทih ๐ด) = (โโ(๐ด
ยทih ((adjโโ๐)โ๐ต)))) |
13 | 1, 7, 12 | 3eqtr3d 2780 |
. . 3
โข ((๐ โ dom
adjโ โง ๐ต โ โ โง ๐ด โ โ) โ
(โโ((๐โ๐ด) ยทih ๐ต)) = (โโ(๐ด
ยทih ((adjโโ๐)โ๐ต)))) |
14 | | hicl 30371 |
. . . . 5
โข (((๐โ๐ด) โ โ โง ๐ต โ โ) โ ((๐โ๐ด) ยทih ๐ต) โ
โ) |
15 | 5, 2, 14 | syl2anc 584 |
. . . 4
โข ((๐ โ dom
adjโ โง ๐ต โ โ โง ๐ด โ โ) โ ((๐โ๐ด) ยทih ๐ต) โ
โ) |
16 | | hicl 30371 |
. . . . 5
โข ((๐ด โ โ โง
((adjโโ๐)โ๐ต) โ โ) โ (๐ด ยทih
((adjโโ๐)โ๐ต)) โ โ) |
17 | 10, 9, 16 | syl2anc 584 |
. . . 4
โข ((๐ โ dom
adjโ โง ๐ต โ โ โง ๐ด โ โ) โ (๐ด ยทih
((adjโโ๐)โ๐ต)) โ โ) |
18 | | cj11 15111 |
. . . 4
โข ((((๐โ๐ด) ยทih ๐ต) โ โ โง (๐ด
ยทih ((adjโโ๐)โ๐ต)) โ โ) โ
((โโ((๐โ๐ด) ยทih ๐ต)) = (โโ(๐ด
ยทih ((adjโโ๐)โ๐ต))) โ ((๐โ๐ด) ยทih ๐ต) = (๐ด ยทih
((adjโโ๐)โ๐ต)))) |
19 | 15, 17, 18 | syl2anc 584 |
. . 3
โข ((๐ โ dom
adjโ โง ๐ต โ โ โง ๐ด โ โ) โ
((โโ((๐โ๐ด) ยทih ๐ต)) = (โโ(๐ด
ยทih ((adjโโ๐)โ๐ต))) โ ((๐โ๐ด) ยทih ๐ต) = (๐ด ยทih
((adjโโ๐)โ๐ต)))) |
20 | 13, 19 | mpbid 231 |
. 2
โข ((๐ โ dom
adjโ โง ๐ต โ โ โง ๐ด โ โ) โ ((๐โ๐ด) ยทih ๐ต) = (๐ด ยทih
((adjโโ๐)โ๐ต))) |
21 | 20 | 3com23 1126 |
1
โข ((๐ โ dom
adjโ โง ๐ด โ โ โง ๐ต โ โ) โ ((๐โ๐ด) ยทih ๐ต) = (๐ด ยทih
((adjโโ๐)โ๐ต))) |