Step | Hyp | Ref
| Expression |
1 | | hvmulcl 30253 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด
ยทโ ๐ต) โ โ) |
2 | | kbfval 31192 |
. . 3
โข (((๐ด
ยทโ ๐ต) โ โ โง ๐ถ โ โ) โ ((๐ด ยทโ ๐ต) ketbra ๐ถ) = (๐ฅ โ โ โฆ ((๐ฅ ยทih ๐ถ)
ยทโ (๐ด ยทโ ๐ต)))) |
3 | 1, 2 | stoic3 1778 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด
ยทโ ๐ต) ketbra ๐ถ) = (๐ฅ โ โ โฆ ((๐ฅ ยทih ๐ถ)
ยทโ (๐ด ยทโ ๐ต)))) |
4 | | simp2 1137 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ต โ
โ) |
5 | | cjcl 15048 |
. . . . . 6
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
6 | 5 | 3ad2ant1 1133 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
(โโ๐ด) โ
โ) |
7 | | simp3 1138 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ถ โ
โ) |
8 | | hvmulcl 30253 |
. . . . 5
โข
(((โโ๐ด)
โ โ โง ๐ถ
โ โ) โ ((โโ๐ด) ยทโ ๐ถ) โ
โ) |
9 | 6, 7, 8 | syl2anc 584 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
((โโ๐ด)
ยทโ ๐ถ) โ โ) |
10 | | kbfval 31192 |
. . . 4
โข ((๐ต โ โ โง
((โโ๐ด)
ยทโ ๐ถ) โ โ) โ (๐ต ketbra ((โโ๐ด) ยทโ ๐ถ)) = (๐ฅ โ โ โฆ ((๐ฅ ยทih
((โโ๐ด)
ยทโ ๐ถ)) ยทโ ๐ต))) |
11 | 4, 9, 10 | syl2anc 584 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ต ketbra ((โโ๐ด)
ยทโ ๐ถ)) = (๐ฅ โ โ โฆ ((๐ฅ ยทih
((โโ๐ด)
ยทโ ๐ถ)) ยทโ ๐ต))) |
12 | | simpr 485 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ฅ โ โ) โ ๐ฅ โ
โ) |
13 | | simpl3 1193 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ฅ โ โ) โ ๐ถ โ
โ) |
14 | | hicl 30320 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ถ โ โ) โ (๐ฅ
ยทih ๐ถ) โ โ) |
15 | 12, 13, 14 | syl2anc 584 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ฅ โ โ) โ (๐ฅ
ยทih ๐ถ) โ โ) |
16 | | simpl1 1191 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ฅ โ โ) โ ๐ด โ
โ) |
17 | | simpl2 1192 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ฅ โ โ) โ ๐ต โ
โ) |
18 | | ax-hvmulass 30247 |
. . . . . 6
โข (((๐ฅ
ยทih ๐ถ) โ โ โง ๐ด โ โ โง ๐ต โ โ) โ (((๐ฅ
ยทih ๐ถ) ยท ๐ด) ยทโ ๐ต) = ((๐ฅ ยทih ๐ถ)
ยทโ (๐ด ยทโ ๐ต))) |
19 | 15, 16, 17, 18 | syl3anc 1371 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ฅ โ โ) โ (((๐ฅ
ยทih ๐ถ) ยท ๐ด) ยทโ ๐ต) = ((๐ฅ ยทih ๐ถ)
ยทโ (๐ด ยทโ ๐ต))) |
20 | 15, 16 | mulcomd 11231 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ฅ โ โ) โ ((๐ฅ
ยทih ๐ถ) ยท ๐ด) = (๐ด ยท (๐ฅ ยทih ๐ถ))) |
21 | | his52 30327 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ฅ โ โ โง ๐ถ โ โ) โ (๐ฅ
ยทih ((โโ๐ด) ยทโ ๐ถ)) = (๐ด ยท (๐ฅ ยทih ๐ถ))) |
22 | 16, 12, 13, 21 | syl3anc 1371 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ฅ โ โ) โ (๐ฅ
ยทih ((โโ๐ด) ยทโ ๐ถ)) = (๐ด ยท (๐ฅ ยทih ๐ถ))) |
23 | 20, 22 | eqtr4d 2775 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ฅ โ โ) โ ((๐ฅ
ยทih ๐ถ) ยท ๐ด) = (๐ฅ ยทih
((โโ๐ด)
ยทโ ๐ถ))) |
24 | 23 | oveq1d 7420 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ฅ โ โ) โ (((๐ฅ
ยทih ๐ถ) ยท ๐ด) ยทโ ๐ต) = ((๐ฅ ยทih
((โโ๐ด)
ยทโ ๐ถ)) ยทโ ๐ต)) |
25 | 19, 24 | eqtr3d 2774 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ฅ โ โ) โ ((๐ฅ
ยทih ๐ถ) ยทโ (๐ด
ยทโ ๐ต)) = ((๐ฅ ยทih
((โโ๐ด)
ยทโ ๐ถ)) ยทโ ๐ต)) |
26 | 25 | mpteq2dva 5247 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ฅ โ โ โฆ ((๐ฅ
ยทih ๐ถ) ยทโ (๐ด
ยทโ ๐ต))) = (๐ฅ โ โ โฆ ((๐ฅ ยทih
((โโ๐ด)
ยทโ ๐ถ)) ยทโ ๐ต))) |
27 | 11, 26 | eqtr4d 2775 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ต ketbra ((โโ๐ด)
ยทโ ๐ถ)) = (๐ฅ โ โ โฆ ((๐ฅ ยทih ๐ถ)
ยทโ (๐ด ยทโ ๐ต)))) |
28 | 3, 27 | eqtr4d 2775 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด
ยทโ ๐ต) ketbra ๐ถ) = (๐ต ketbra ((โโ๐ด) ยทโ ๐ถ))) |