Step | Hyp | Ref
| Expression |
1 | | negsub 11454 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + -๐ต) = (๐ด โ ๐ต)) |
2 | | negsub 11454 |
. . 3
โข ((๐ถ โ โ โง ๐ท โ โ) โ (๐ถ + -๐ท) = (๐ถ โ ๐ท)) |
3 | 1, 2 | oveqan12d 7377 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด + -๐ต) ยท (๐ถ + -๐ท)) = ((๐ด โ ๐ต) ยท (๐ถ โ ๐ท))) |
4 | | negcl 11406 |
. . . 4
โข (๐ต โ โ โ -๐ต โ
โ) |
5 | | negcl 11406 |
. . . . 5
โข (๐ท โ โ โ -๐ท โ
โ) |
6 | | muladd 11592 |
. . . . 5
โข (((๐ด โ โ โง -๐ต โ โ) โง (๐ถ โ โ โง -๐ท โ โ)) โ ((๐ด + -๐ต) ยท (๐ถ + -๐ท)) = (((๐ด ยท ๐ถ) + (-๐ท ยท -๐ต)) + ((๐ด ยท -๐ท) + (๐ถ ยท -๐ต)))) |
7 | 5, 6 | sylanr2 682 |
. . . 4
โข (((๐ด โ โ โง -๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด + -๐ต) ยท (๐ถ + -๐ท)) = (((๐ด ยท ๐ถ) + (-๐ท ยท -๐ต)) + ((๐ด ยท -๐ท) + (๐ถ ยท -๐ต)))) |
8 | 4, 7 | sylanl2 680 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด + -๐ต) ยท (๐ถ + -๐ท)) = (((๐ด ยท ๐ถ) + (-๐ท ยท -๐ต)) + ((๐ด ยท -๐ท) + (๐ถ ยท -๐ต)))) |
9 | | mul2neg 11599 |
. . . . . . 7
โข ((๐ท โ โ โง ๐ต โ โ) โ (-๐ท ยท -๐ต) = (๐ท ยท ๐ต)) |
10 | 9 | ancoms 460 |
. . . . . 6
โข ((๐ต โ โ โง ๐ท โ โ) โ (-๐ท ยท -๐ต) = (๐ท ยท ๐ต)) |
11 | 10 | oveq2d 7374 |
. . . . 5
โข ((๐ต โ โ โง ๐ท โ โ) โ ((๐ด ยท ๐ถ) + (-๐ท ยท -๐ต)) = ((๐ด ยท ๐ถ) + (๐ท ยท ๐ต))) |
12 | 11 | ad2ant2l 745 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด ยท ๐ถ) + (-๐ท ยท -๐ต)) = ((๐ด ยท ๐ถ) + (๐ท ยท ๐ต))) |
13 | | mulneg2 11597 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ท โ โ) โ (๐ด ยท -๐ท) = -(๐ด ยท ๐ท)) |
14 | | mulneg2 11597 |
. . . . . . . 8
โข ((๐ถ โ โ โง ๐ต โ โ) โ (๐ถ ยท -๐ต) = -(๐ถ ยท ๐ต)) |
15 | 13, 14 | oveqan12d 7377 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ต โ โ)) โ ((๐ด ยท -๐ท) + (๐ถ ยท -๐ต)) = (-(๐ด ยท ๐ท) + -(๐ถ ยท ๐ต))) |
16 | | mulcl 11140 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ท โ โ) โ (๐ด ยท ๐ท) โ โ) |
17 | | mulcl 11140 |
. . . . . . . 8
โข ((๐ถ โ โ โง ๐ต โ โ) โ (๐ถ ยท ๐ต) โ โ) |
18 | | negdi 11463 |
. . . . . . . 8
โข (((๐ด ยท ๐ท) โ โ โง (๐ถ ยท ๐ต) โ โ) โ -((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) = (-(๐ด ยท ๐ท) + -(๐ถ ยท ๐ต))) |
19 | 16, 17, 18 | syl2an 597 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ต โ โ)) โ
-((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) = (-(๐ด ยท ๐ท) + -(๐ถ ยท ๐ต))) |
20 | 15, 19 | eqtr4d 2776 |
. . . . . 6
โข (((๐ด โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ต โ โ)) โ ((๐ด ยท -๐ท) + (๐ถ ยท -๐ต)) = -((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) |
21 | 20 | ancom2s 649 |
. . . . 5
โข (((๐ด โ โ โง ๐ท โ โ) โง (๐ต โ โ โง ๐ถ โ โ)) โ ((๐ด ยท -๐ท) + (๐ถ ยท -๐ต)) = -((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) |
22 | 21 | an42s 660 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด ยท -๐ท) + (๐ถ ยท -๐ต)) = -((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) |
23 | 12, 22 | oveq12d 7376 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ด ยท ๐ถ) + (-๐ท ยท -๐ต)) + ((๐ด ยท -๐ท) + (๐ถ ยท -๐ต))) = (((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) + -((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)))) |
24 | | mulcl 11140 |
. . . . . 6
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ด ยท ๐ถ) โ โ) |
25 | | mulcl 11140 |
. . . . . . 7
โข ((๐ท โ โ โง ๐ต โ โ) โ (๐ท ยท ๐ต) โ โ) |
26 | 25 | ancoms 460 |
. . . . . 6
โข ((๐ต โ โ โง ๐ท โ โ) โ (๐ท ยท ๐ต) โ โ) |
27 | | addcl 11138 |
. . . . . 6
โข (((๐ด ยท ๐ถ) โ โ โง (๐ท ยท ๐ต) โ โ) โ ((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) โ โ) |
28 | 24, 26, 27 | syl2an 597 |
. . . . 5
โข (((๐ด โ โ โง ๐ถ โ โ) โง (๐ต โ โ โง ๐ท โ โ)) โ ((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) โ โ) |
29 | 28 | an4s 659 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) โ โ) |
30 | 17 | ancoms 460 |
. . . . . 6
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ถ ยท ๐ต) โ โ) |
31 | | addcl 11138 |
. . . . . 6
โข (((๐ด ยท ๐ท) โ โ โง (๐ถ ยท ๐ต) โ โ) โ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) โ โ) |
32 | 16, 30, 31 | syl2an 597 |
. . . . 5
โข (((๐ด โ โ โง ๐ท โ โ) โง (๐ต โ โ โง ๐ถ โ โ)) โ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) โ โ) |
33 | 32 | an42s 660 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) โ โ) |
34 | 29, 33 | negsubd 11523 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) + -((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) = (((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) โ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)))) |
35 | 8, 23, 34 | 3eqtrd 2777 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด + -๐ต) ยท (๐ถ + -๐ท)) = (((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) โ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)))) |
36 | 3, 35 | eqtr3d 2775 |
1
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด โ ๐ต) ยท (๐ถ โ ๐ท)) = (((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) โ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)))) |