Step | Hyp | Ref
| Expression |
1 | | dmadjop 30635 |
. . 3
โข (๐ โ dom
adjโ โ ๐: โโถ โ) |
2 | | homulcl 30506 |
. . 3
โข ((๐ด โ โ โง ๐: โโถ โ)
โ (๐ด
ยทop ๐): โโถ โ) |
3 | 1, 2 | sylan2 594 |
. 2
โข ((๐ด โ โ โง ๐ โ dom
adjโ) โ (๐ด ยทop ๐): โโถ
โ) |
4 | | cjcl 14925 |
. . 3
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
5 | | dmadjrn 30642 |
. . . 4
โข (๐ โ dom
adjโ โ (adjโโ๐) โ dom
adjโ) |
6 | | dmadjop 30635 |
. . . 4
โข
((adjโโ๐) โ dom adjโ โ
(adjโโ๐): โโถ โ) |
7 | 5, 6 | syl 17 |
. . 3
โข (๐ โ dom
adjโ โ (adjโโ๐): โโถ โ) |
8 | | homulcl 30506 |
. . 3
โข
(((โโ๐ด)
โ โ โง (adjโโ๐): โโถ โ) โ
((โโ๐ด)
ยทop (adjโโ๐)): โโถ
โ) |
9 | 4, 7, 8 | syl2an 597 |
. 2
โข ((๐ด โ โ โง ๐ โ dom
adjโ) โ ((โโ๐ด) ยทop
(adjโโ๐)): โโถ
โ) |
10 | | adj2 30681 |
. . . . . . . 8
โข ((๐ โ dom
adjโ โง ๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
((adjโโ๐)โ๐ฆ))) |
11 | 10 | 3expb 1121 |
. . . . . . 7
โข ((๐ โ dom
adjโ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
((adjโโ๐)โ๐ฆ))) |
12 | 11 | adantll 713 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ dom
adjโ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
((adjโโ๐)โ๐ฆ))) |
13 | 12 | oveq2d 7366 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ dom
adjโ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ด ยท ((๐โ๐ฅ) ยทih ๐ฆ)) = (๐ด ยท (๐ฅ ยทih
((adjโโ๐)โ๐ฆ)))) |
14 | 1 | ffvelcdmda 7030 |
. . . . . . . . 9
โข ((๐ โ dom
adjโ โง ๐ฅ โ โ) โ (๐โ๐ฅ) โ โ) |
15 | | ax-his3 29831 |
. . . . . . . . 9
โข ((๐ด โ โ โง (๐โ๐ฅ) โ โ โง ๐ฆ โ โ) โ ((๐ด ยทโ (๐โ๐ฅ)) ยทih ๐ฆ) = (๐ด ยท ((๐โ๐ฅ) ยทih ๐ฆ))) |
16 | 14, 15 | syl3an2 1165 |
. . . . . . . 8
โข ((๐ด โ โ โง (๐ โ dom
adjโ โง ๐ฅ โ โ) โง ๐ฆ โ โ) โ ((๐ด ยทโ (๐โ๐ฅ)) ยทih ๐ฆ) = (๐ด ยท ((๐โ๐ฅ) ยทih ๐ฆ))) |
17 | 16 | 3exp 1120 |
. . . . . . 7
โข (๐ด โ โ โ ((๐ โ dom
adjโ โง ๐ฅ โ โ) โ (๐ฆ โ โ โ ((๐ด ยทโ (๐โ๐ฅ)) ยทih ๐ฆ) = (๐ด ยท ((๐โ๐ฅ) ยทih ๐ฆ))))) |
18 | 17 | expd 417 |
. . . . . 6
โข (๐ด โ โ โ (๐ โ dom
adjโ โ (๐ฅ โ โ โ (๐ฆ โ โ โ ((๐ด ยทโ (๐โ๐ฅ)) ยทih ๐ฆ) = (๐ด ยท ((๐โ๐ฅ) ยทih ๐ฆ)))))) |
19 | 18 | imp43 429 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ dom
adjโ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ด ยทโ (๐โ๐ฅ)) ยทih ๐ฆ) = (๐ด ยท ((๐โ๐ฅ) ยทih ๐ฆ))) |
20 | | simpll 766 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ dom
adjโ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ๐ด โ โ) |
21 | | simprl 770 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ dom
adjโ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ๐ฅ โ โ) |
22 | | adjcl 30679 |
. . . . . . 7
โข ((๐ โ dom
adjโ โง ๐ฆ โ โ) โ
((adjโโ๐)โ๐ฆ) โ โ) |
23 | 22 | ad2ant2l 745 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ dom
adjโ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
((adjโโ๐)โ๐ฆ) โ โ) |
24 | | his52 29834 |
. . . . . 6
โข ((๐ด โ โ โง ๐ฅ โ โ โง
((adjโโ๐)โ๐ฆ) โ โ) โ (๐ฅ ยทih
((โโ๐ด)
ยทโ ((adjโโ๐)โ๐ฆ))) = (๐ด ยท (๐ฅ ยทih
((adjโโ๐)โ๐ฆ)))) |
25 | 20, 21, 23, 24 | syl3anc 1372 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ dom
adjโ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ฅ ยทih
((โโ๐ด)
ยทโ ((adjโโ๐)โ๐ฆ))) = (๐ด ยท (๐ฅ ยทih
((adjโโ๐)โ๐ฆ)))) |
26 | 13, 19, 25 | 3eqtr4d 2788 |
. . . 4
โข (((๐ด โ โ โง ๐ โ dom
adjโ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ด ยทโ (๐โ๐ฅ)) ยทih ๐ฆ) = (๐ฅ ยทih
((โโ๐ด)
ยทโ ((adjโโ๐)โ๐ฆ)))) |
27 | | homval 30488 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐ฅ โ โ) โ
((๐ด
ยทop ๐)โ๐ฅ) = (๐ด ยทโ (๐โ๐ฅ))) |
28 | 1, 27 | syl3an2 1165 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ dom
adjโ โง ๐ฅ โ โ) โ ((๐ด ยทop ๐)โ๐ฅ) = (๐ด ยทโ (๐โ๐ฅ))) |
29 | 28 | 3expa 1119 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ dom
adjโ) โง ๐ฅ โ โ) โ ((๐ด ยทop ๐)โ๐ฅ) = (๐ด ยทโ (๐โ๐ฅ))) |
30 | 29 | adantrr 716 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ dom
adjโ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ด ยทop ๐)โ๐ฅ) = (๐ด ยทโ (๐โ๐ฅ))) |
31 | 30 | oveq1d 7365 |
. . . 4
โข (((๐ด โ โ โง ๐ โ dom
adjโ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (((๐ด ยทop ๐)โ๐ฅ) ยทih ๐ฆ) = ((๐ด ยทโ (๐โ๐ฅ)) ยทih ๐ฆ)) |
32 | | id 22 |
. . . . . . . 8
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
33 | | homval 30488 |
. . . . . . . 8
โข
(((โโ๐ด)
โ โ โง (adjโโ๐): โโถ โ โง ๐ฆ โ โ) โ
(((โโ๐ด)
ยทop (adjโโ๐))โ๐ฆ) = ((โโ๐ด) ยทโ
((adjโโ๐)โ๐ฆ))) |
34 | 4, 7, 32, 33 | syl3an 1161 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ dom
adjโ โง ๐ฆ โ โ) โ
(((โโ๐ด)
ยทop (adjโโ๐))โ๐ฆ) = ((โโ๐ด) ยทโ
((adjโโ๐)โ๐ฆ))) |
35 | 34 | 3expa 1119 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ dom
adjโ) โง ๐ฆ โ โ) โ
(((โโ๐ด)
ยทop (adjโโ๐))โ๐ฆ) = ((โโ๐ด) ยทโ
((adjโโ๐)โ๐ฆ))) |
36 | 35 | adantrl 715 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ dom
adjโ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
(((โโ๐ด)
ยทop (adjโโ๐))โ๐ฆ) = ((โโ๐ด) ยทโ
((adjโโ๐)โ๐ฆ))) |
37 | 36 | oveq2d 7366 |
. . . 4
โข (((๐ด โ โ โง ๐ โ dom
adjโ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ฅ ยทih
(((โโ๐ด)
ยทop (adjโโ๐))โ๐ฆ)) = (๐ฅ ยทih
((โโ๐ด)
ยทโ ((adjโโ๐)โ๐ฆ)))) |
38 | 26, 31, 37 | 3eqtr4d 2788 |
. . 3
โข (((๐ด โ โ โง ๐ โ dom
adjโ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (((๐ด ยทop ๐)โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
(((โโ๐ด)
ยทop (adjโโ๐))โ๐ฆ))) |
39 | 38 | ralrimivva 3196 |
. 2
โข ((๐ด โ โ โง ๐ โ dom
adjโ) โ โ๐ฅ โ โ โ๐ฆ โ โ (((๐ด ยทop ๐)โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
(((โโ๐ด)
ยทop (adjโโ๐))โ๐ฆ))) |
40 | | adjeq 30682 |
. 2
โข (((๐ด ยทop
๐): โโถ โ
โง ((โโ๐ด)
ยทop (adjโโ๐)): โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(((๐ด
ยทop ๐)โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
(((โโ๐ด)
ยทop (adjโโ๐))โ๐ฆ))) โ
(adjโโ(๐ด ยทop ๐)) = ((โโ๐ด) ยทop
(adjโโ๐))) |
41 | 3, 9, 39, 40 | syl3anc 1372 |
1
โข ((๐ด โ โ โง ๐ โ dom
adjโ) โ (adjโโ(๐ด ยทop ๐)) = ((โโ๐ด) ยทop
(adjโโ๐))) |