Step | Hyp | Ref
| Expression |
1 | | simplr 768 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ๐ต โ
โ) |
2 | | simprl 770 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ๐ถ โ
โ) |
3 | 1, 2 | mulcld 11180 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ต ยท ๐ถ) โ โ) |
4 | | subaddmulsub 11623 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ) โง (๐ต ยท ๐ถ) โ โ) โ ((๐ต ยท ๐ถ) โ ((๐ด + ๐ต) ยท (๐ถ โ ๐ท))) = ((((๐ต ยท ๐ถ) โ (๐ด ยท ๐ถ)) โ (๐ต ยท ๐ถ)) + ((๐ด ยท ๐ท) + (๐ต ยท ๐ท)))) |
5 | 3, 4 | mpd3an3 1463 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ต ยท ๐ถ) โ ((๐ด + ๐ต) ยท (๐ถ โ ๐ท))) = ((((๐ต ยท ๐ถ) โ (๐ด ยท ๐ถ)) โ (๐ต ยท ๐ถ)) + ((๐ด ยท ๐ท) + (๐ต ยท ๐ท)))) |
6 | | simpll 766 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ๐ด โ
โ) |
7 | 6, 2 | mulcld 11180 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ด ยท ๐ถ) โ โ) |
8 | 3, 7, 3 | sub32d 11549 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ต ยท ๐ถ) โ (๐ด ยท ๐ถ)) โ (๐ต ยท ๐ถ)) = (((๐ต ยท ๐ถ) โ (๐ต ยท ๐ถ)) โ (๐ด ยท ๐ถ))) |
9 | 3 | subidd 11505 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ต ยท ๐ถ) โ (๐ต ยท ๐ถ)) = 0) |
10 | 9 | oveq1d 7373 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ต ยท ๐ถ) โ (๐ต ยท ๐ถ)) โ (๐ด ยท ๐ถ)) = (0 โ (๐ด ยท ๐ถ))) |
11 | 8, 10 | eqtrd 2773 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ต ยท ๐ถ) โ (๐ด ยท ๐ถ)) โ (๐ต ยท ๐ถ)) = (0 โ (๐ด ยท ๐ถ))) |
12 | | df-neg 11393 |
. . . . 5
โข -(๐ด ยท ๐ถ) = (0 โ (๐ด ยท ๐ถ)) |
13 | 11, 12 | eqtr4di 2791 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ต ยท ๐ถ) โ (๐ด ยท ๐ถ)) โ (๐ต ยท ๐ถ)) = -(๐ด ยท ๐ถ)) |
14 | 13 | oveq1d 7373 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
((((๐ต ยท ๐ถ) โ (๐ด ยท ๐ถ)) โ (๐ต ยท ๐ถ)) + ((๐ด ยท ๐ท) + (๐ต ยท ๐ท))) = (-(๐ด ยท ๐ถ) + ((๐ด ยท ๐ท) + (๐ต ยท ๐ท)))) |
15 | 7 | negcld 11504 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ -(๐ด ยท ๐ถ) โ โ) |
16 | | simprr 772 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ๐ท โ
โ) |
17 | 6, 16 | mulcld 11180 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ด ยท ๐ท) โ โ) |
18 | 1, 16 | mulcld 11180 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ต ยท ๐ท) โ โ) |
19 | 17, 18 | addcld 11179 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด ยท ๐ท) + (๐ต ยท ๐ท)) โ โ) |
20 | 15, 19 | addcomd 11362 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(-(๐ด ยท ๐ถ) + ((๐ด ยท ๐ท) + (๐ต ยท ๐ท))) = (((๐ด ยท ๐ท) + (๐ต ยท ๐ท)) + -(๐ด ยท ๐ถ))) |
21 | 19, 7 | negsubd 11523 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ด ยท ๐ท) + (๐ต ยท ๐ท)) + -(๐ด ยท ๐ถ)) = (((๐ด ยท ๐ท) + (๐ต ยท ๐ท)) โ (๐ด ยท ๐ถ))) |
22 | 20, 21 | eqtrd 2773 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(-(๐ด ยท ๐ถ) + ((๐ด ยท ๐ท) + (๐ต ยท ๐ท))) = (((๐ด ยท ๐ท) + (๐ต ยท ๐ท)) โ (๐ด ยท ๐ถ))) |
23 | 14, 22 | eqtrd 2773 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
((((๐ต ยท ๐ถ) โ (๐ด ยท ๐ถ)) โ (๐ต ยท ๐ถ)) + ((๐ด ยท ๐ท) + (๐ต ยท ๐ท))) = (((๐ด ยท ๐ท) + (๐ต ยท ๐ท)) โ (๐ด ยท ๐ถ))) |
24 | 5, 23 | eqtrd 2773 |
1
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ต ยท ๐ถ) โ ((๐ด + ๐ต) ยท (๐ถ โ ๐ท))) = (((๐ด ยท ๐ท) + (๐ต ยท ๐ท)) โ (๐ด ยท ๐ถ))) |