Step | Hyp | Ref
| Expression |
1 | | replim 15008 |
. . . . . 6
โข (๐ด โ โ โ ๐ด = ((โโ๐ด) + (i ยท
(โโ๐ด)))) |
2 | | replim 15008 |
. . . . . 6
โข (๐ต โ โ โ ๐ต = ((โโ๐ต) + (i ยท
(โโ๐ต)))) |
3 | 1, 2 | oveqan12d 7381 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) = (((โโ๐ด) + (i ยท (โโ๐ด))) ยท
((โโ๐ต) + (i
ยท (โโ๐ต))))) |
4 | | recl 15002 |
. . . . . . . . 9
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
5 | 4 | adantr 482 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ด) โ
โ) |
6 | 5 | recnd 11190 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ด) โ
โ) |
7 | | ax-icn 11117 |
. . . . . . . 8
โข i โ
โ |
8 | | imcl 15003 |
. . . . . . . . . 10
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
9 | 8 | adantr 482 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ด) โ
โ) |
10 | 9 | recnd 11190 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ด) โ
โ) |
11 | | mulcl 11142 |
. . . . . . . 8
โข ((i
โ โ โง (โโ๐ด) โ โ) โ (i ยท
(โโ๐ด)) โ
โ) |
12 | 7, 10, 11 | sylancr 588 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (i
ยท (โโ๐ด))
โ โ) |
13 | 6, 12 | addcld 11181 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) + (i
ยท (โโ๐ด))) โ โ) |
14 | | recl 15002 |
. . . . . . . 8
โข (๐ต โ โ โ
(โโ๐ต) โ
โ) |
15 | 14 | adantl 483 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ต) โ
โ) |
16 | 15 | recnd 11190 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ต) โ
โ) |
17 | | imcl 15003 |
. . . . . . . . 9
โข (๐ต โ โ โ
(โโ๐ต) โ
โ) |
18 | 17 | adantl 483 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ต) โ
โ) |
19 | 18 | recnd 11190 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ต) โ
โ) |
20 | | mulcl 11142 |
. . . . . . 7
โข ((i
โ โ โง (โโ๐ต) โ โ) โ (i ยท
(โโ๐ต)) โ
โ) |
21 | 7, 19, 20 | sylancr 588 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (i
ยท (โโ๐ต))
โ โ) |
22 | 13, 16, 21 | adddid 11186 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด) + (i
ยท (โโ๐ด))) ยท ((โโ๐ต) + (i ยท
(โโ๐ต)))) =
((((โโ๐ด) + (i
ยท (โโ๐ด))) ยท (โโ๐ต)) + (((โโ๐ด) + (i ยท (โโ๐ด))) ยท (i ยท
(โโ๐ต))))) |
23 | 6, 12, 16 | adddird 11187 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด) + (i
ยท (โโ๐ด))) ยท (โโ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) + ((i ยท (โโ๐ด)) ยท (โโ๐ต)))) |
24 | 6, 12, 21 | adddird 11187 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด) + (i
ยท (โโ๐ด))) ยท (i ยท
(โโ๐ต))) =
(((โโ๐ด) ยท
(i ยท (โโ๐ต))) + ((i ยท (โโ๐ด)) ยท (i ยท
(โโ๐ต))))) |
25 | 23, 24 | oveq12d 7380 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((โโ๐ด) + (i
ยท (โโ๐ด))) ยท (โโ๐ต)) + (((โโ๐ด) + (i ยท (โโ๐ด))) ยท (i ยท
(โโ๐ต)))) =
((((โโ๐ด)
ยท (โโ๐ต))
+ ((i ยท (โโ๐ด)) ยท (โโ๐ต))) + (((โโ๐ด) ยท (i ยท (โโ๐ต))) + ((i ยท
(โโ๐ด)) ยท
(i ยท (โโ๐ต)))))) |
26 | 5, 15 | remulcld 11192 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) ยท
(โโ๐ต)) โ
โ) |
27 | 26 | recnd 11190 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) ยท
(โโ๐ต)) โ
โ) |
28 | 12, 21 | mulcld 11182 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ((i
ยท (โโ๐ด))
ยท (i ยท (โโ๐ต))) โ โ) |
29 | 12, 16 | mulcld 11182 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ((i
ยท (โโ๐ด))
ยท (โโ๐ต))
โ โ) |
30 | 6, 21 | mulcld 11182 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) ยท
(i ยท (โโ๐ต))) โ โ) |
31 | 27, 28, 29, 30 | add42d 11391 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((โโ๐ด)
ยท (โโ๐ต))
+ ((i ยท (โโ๐ด)) ยท (i ยท (โโ๐ต)))) + (((i ยท
(โโ๐ด)) ยท
(โโ๐ต)) +
((โโ๐ด) ยท
(i ยท (โโ๐ต))))) = ((((โโ๐ด) ยท (โโ๐ต)) + ((i ยท (โโ๐ด)) ยท (โโ๐ต))) + (((โโ๐ด) ยท (i ยท
(โโ๐ต))) + ((i
ยท (โโ๐ด))
ยท (i ยท (โโ๐ต)))))) |
32 | 7 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ i โ
โ) |
33 | 32, 10, 32, 19 | mul4d 11374 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ ((i
ยท (โโ๐ด))
ยท (i ยท (โโ๐ต))) = ((i ยท i) ยท
((โโ๐ด) ยท
(โโ๐ต)))) |
34 | | ixi 11791 |
. . . . . . . . . . . 12
โข (i
ยท i) = -1 |
35 | 34 | oveq1i 7372 |
. . . . . . . . . . 11
โข ((i
ยท i) ยท ((โโ๐ด) ยท (โโ๐ต))) = (-1 ยท ((โโ๐ด) ยท (โโ๐ต))) |
36 | 9, 18 | remulcld 11192 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) ยท
(โโ๐ต)) โ
โ) |
37 | 36 | recnd 11190 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) ยท
(โโ๐ต)) โ
โ) |
38 | 37 | mulm1d 11614 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ (-1
ยท ((โโ๐ด)
ยท (โโ๐ต))) = -((โโ๐ด) ยท (โโ๐ต))) |
39 | 35, 38 | eqtrid 2789 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ ((i
ยท i) ยท ((โโ๐ด) ยท (โโ๐ต))) = -((โโ๐ด) ยท (โโ๐ต))) |
40 | 33, 39 | eqtrd 2777 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ ((i
ยท (โโ๐ด))
ยท (i ยท (โโ๐ต))) = -((โโ๐ด) ยท (โโ๐ต))) |
41 | 40 | oveq2d 7378 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด) ยท
(โโ๐ต)) + ((i
ยท (โโ๐ด))
ยท (i ยท (โโ๐ต)))) = (((โโ๐ด) ยท (โโ๐ต)) + -((โโ๐ด) ยท (โโ๐ต)))) |
42 | 27, 37 | negsubd 11525 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด) ยท
(โโ๐ต)) +
-((โโ๐ด)
ยท (โโ๐ต))) = (((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต)))) |
43 | 41, 42 | eqtrd 2777 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด) ยท
(โโ๐ต)) + ((i
ยท (โโ๐ด))
ยท (i ยท (โโ๐ต)))) = (((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต)))) |
44 | 9, 15 | remulcld 11192 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) ยท
(โโ๐ต)) โ
โ) |
45 | 44 | recnd 11190 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) ยท
(โโ๐ต)) โ
โ) |
46 | | mulcl 11142 |
. . . . . . . . . 10
โข ((i
โ โ โง ((โโ๐ด) ยท (โโ๐ต)) โ โ) โ (i ยท
((โโ๐ด) ยท
(โโ๐ต))) โ
โ) |
47 | 7, 45, 46 | sylancr 588 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (i
ยท ((โโ๐ด)
ยท (โโ๐ต)))
โ โ) |
48 | 5, 18 | remulcld 11192 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) ยท
(โโ๐ต)) โ
โ) |
49 | 48 | recnd 11190 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) ยท
(โโ๐ต)) โ
โ) |
50 | | mulcl 11142 |
. . . . . . . . . 10
โข ((i
โ โ โง ((โโ๐ด) ยท (โโ๐ต)) โ โ) โ (i ยท
((โโ๐ด) ยท
(โโ๐ต))) โ
โ) |
51 | 7, 49, 50 | sylancr 588 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (i
ยท ((โโ๐ด)
ยท (โโ๐ต))) โ โ) |
52 | 47, 51 | addcomd 11364 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ((i
ยท ((โโ๐ด)
ยท (โโ๐ต)))
+ (i ยท ((โโ๐ด) ยท (โโ๐ต)))) = ((i ยท ((โโ๐ด) ยท (โโ๐ต))) + (i ยท
((โโ๐ด) ยท
(โโ๐ต))))) |
53 | 32, 10, 16 | mulassd 11185 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ ((i
ยท (โโ๐ด))
ยท (โโ๐ต))
= (i ยท ((โโ๐ด) ยท (โโ๐ต)))) |
54 | 6, 32, 19 | mul12d 11371 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) ยท
(i ยท (โโ๐ต))) = (i ยท ((โโ๐ด) ยท (โโ๐ต)))) |
55 | 53, 54 | oveq12d 7380 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (((i
ยท (โโ๐ด))
ยท (โโ๐ต))
+ ((โโ๐ด)
ยท (i ยท (โโ๐ต)))) = ((i ยท ((โโ๐ด) ยท (โโ๐ต))) + (i ยท
((โโ๐ด) ยท
(โโ๐ต))))) |
56 | 32, 49, 45 | adddid 11186 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (i
ยท (((โโ๐ด)
ยท (โโ๐ต))
+ ((โโ๐ด)
ยท (โโ๐ต)))) = ((i ยท ((โโ๐ด) ยท (โโ๐ต))) + (i ยท
((โโ๐ด) ยท
(โโ๐ต))))) |
57 | 52, 55, 56 | 3eqtr4d 2787 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (((i
ยท (โโ๐ด))
ยท (โโ๐ต))
+ ((โโ๐ด)
ยท (i ยท (โโ๐ต)))) = (i ยท (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต))))) |
58 | 43, 57 | oveq12d 7380 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((โโ๐ด)
ยท (โโ๐ต))
+ ((i ยท (โโ๐ด)) ยท (i ยท (โโ๐ต)))) + (((i ยท
(โโ๐ด)) ยท
(โโ๐ต)) +
((โโ๐ด) ยท
(i ยท (โโ๐ต))))) = ((((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต))) + (i ยท (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))))) |
59 | 25, 31, 58 | 3eqtr2d 2783 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((โโ๐ด) + (i
ยท (โโ๐ด))) ยท (โโ๐ต)) + (((โโ๐ด) + (i ยท (โโ๐ด))) ยท (i ยท
(โโ๐ต)))) =
((((โโ๐ด)
ยท (โโ๐ต))
โ ((โโ๐ด)
ยท (โโ๐ต))) + (i ยท (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))))) |
60 | 3, 22, 59 | 3eqtrd 2781 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) = ((((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต))) + (i ยท (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))))) |
61 | 60 | fveq2d 6851 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด ยท
๐ต)) =
(โโ((((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต))) + (i ยท (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต))))))) |
62 | 26, 36 | resubcld 11590 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด) ยท
(โโ๐ต)) โ
((โโ๐ด) ยท
(โโ๐ต))) โ
โ) |
63 | 48, 44 | readdcld 11191 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด) ยท
(โโ๐ต)) +
((โโ๐ด) ยท
(โโ๐ต))) โ
โ) |
64 | | crre 15006 |
. . . 4
โข
(((((โโ๐ด)
ยท (โโ๐ต))
โ ((โโ๐ด)
ยท (โโ๐ต))) โ โ โง
(((โโ๐ด) ยท
(โโ๐ต)) +
((โโ๐ด) ยท
(โโ๐ต))) โ
โ) โ (โโ((((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต))) + (i ยท (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))))) = (((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต)))) |
65 | 62, 63, 64 | syl2anc 585 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ((((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต))) + (i ยท (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))))) = (((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต)))) |
66 | 61, 65 | eqtrd 2777 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด ยท
๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต)))) |
67 | 60 | fveq2d 6851 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด ยท
๐ต)) =
(โโ((((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต))) + (i ยท (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต))))))) |
68 | | crim 15007 |
. . . 4
โข
(((((โโ๐ด)
ยท (โโ๐ต))
โ ((โโ๐ด)
ยท (โโ๐ต))) โ โ โง
(((โโ๐ด) ยท
(โโ๐ต)) +
((โโ๐ด) ยท
(โโ๐ต))) โ
โ) โ (โโ((((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต))) + (i ยท (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))))) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))) |
69 | 62, 63, 68 | syl2anc 585 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ((((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต))) + (i ยท (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))))) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))) |
70 | 67, 69 | eqtrd 2777 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด ยท
๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))) |
71 | | mulcl 11142 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) |
72 | | remim 15009 |
. . . 4
โข ((๐ด ยท ๐ต) โ โ โ
(โโ(๐ด ยท
๐ต)) = ((โโ(๐ด ยท ๐ต)) โ (i ยท (โโ(๐ด ยท ๐ต))))) |
73 | 71, 72 | syl 17 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด ยท
๐ต)) = ((โโ(๐ด ยท ๐ต)) โ (i ยท (โโ(๐ด ยท ๐ต))))) |
74 | | remim 15009 |
. . . . 5
โข (๐ด โ โ โ
(โโ๐ด) =
((โโ๐ด) โ
(i ยท (โโ๐ด)))) |
75 | | remim 15009 |
. . . . 5
โข (๐ต โ โ โ
(โโ๐ต) =
((โโ๐ต) โ
(i ยท (โโ๐ต)))) |
76 | 74, 75 | oveqan12d 7381 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด)
ยท (โโ๐ต)) = (((โโ๐ด) โ (i ยท (โโ๐ด))) ยท
((โโ๐ต) โ
(i ยท (โโ๐ต))))) |
77 | 16, 21 | subcld 11519 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ต) โ
(i ยท (โโ๐ต))) โ โ) |
78 | 6, 12, 77 | subdird 11619 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด) โ
(i ยท (โโ๐ด))) ยท ((โโ๐ต) โ (i ยท
(โโ๐ต)))) =
(((โโ๐ด) ยท
((โโ๐ต) โ
(i ยท (โโ๐ต)))) โ ((i ยท
(โโ๐ด)) ยท
((โโ๐ต) โ
(i ยท (โโ๐ต)))))) |
79 | 27, 30, 29, 28 | subadd4d 11567 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((โโ๐ด)
ยท (โโ๐ต))
โ ((โโ๐ด)
ยท (i ยท (โโ๐ต)))) โ (((i ยท
(โโ๐ด)) ยท
(โโ๐ต)) โ
((i ยท (โโ๐ด)) ยท (i ยท (โโ๐ต))))) = ((((โโ๐ด) ยท (โโ๐ต)) + ((i ยท
(โโ๐ด)) ยท
(i ยท (โโ๐ต)))) โ (((โโ๐ด) ยท (i ยท
(โโ๐ต))) + ((i
ยท (โโ๐ด))
ยท (โโ๐ต))))) |
80 | 6, 16, 21 | subdid 11618 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) ยท
((โโ๐ต) โ
(i ยท (โโ๐ต)))) = (((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (i ยท (โโ๐ต))))) |
81 | 12, 16, 21 | subdid 11618 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ((i
ยท (โโ๐ด))
ยท ((โโ๐ต)
โ (i ยท (โโ๐ต)))) = (((i ยท (โโ๐ด)) ยท (โโ๐ต)) โ ((i ยท
(โโ๐ด)) ยท
(i ยท (โโ๐ต))))) |
82 | 80, 81 | oveq12d 7380 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด) ยท
((โโ๐ต) โ
(i ยท (โโ๐ต)))) โ ((i ยท
(โโ๐ด)) ยท
((โโ๐ต) โ
(i ยท (โโ๐ต))))) = ((((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (i ยท (โโ๐ต)))) โ (((i ยท
(โโ๐ด)) ยท
(โโ๐ต)) โ
((i ยท (โโ๐ด)) ยท (i ยท (โโ๐ต)))))) |
83 | 65, 61, 43 | 3eqtr4d 2787 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด ยท
๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) + ((i ยท
(โโ๐ด)) ยท
(i ยท (โโ๐ต))))) |
84 | 70 | oveq2d 7378 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (i
ยท (โโ(๐ด
ยท ๐ต))) = (i ยท
(((โโ๐ด) ยท
(โโ๐ต)) +
((โโ๐ด) ยท
(โโ๐ต))))) |
85 | 54, 53 | oveq12d 7380 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด) ยท
(i ยท (โโ๐ต))) + ((i ยท (โโ๐ด)) ยท (โโ๐ต))) = ((i ยท
((โโ๐ด) ยท
(โโ๐ต))) + (i
ยท ((โโ๐ด)
ยท (โโ๐ต))))) |
86 | 56, 84, 85 | 3eqtr4d 2787 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (i
ยท (โโ(๐ด
ยท ๐ต))) =
(((โโ๐ด) ยท
(i ยท (โโ๐ต))) + ((i ยท (โโ๐ด)) ยท (โโ๐ต)))) |
87 | 83, 86 | oveq12d 7380 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ(๐ด ยท
๐ต)) โ (i ยท
(โโ(๐ด ยท
๐ต)))) =
((((โโ๐ด)
ยท (โโ๐ต))
+ ((i ยท (โโ๐ด)) ยท (i ยท (โโ๐ต)))) โ
(((โโ๐ด) ยท
(i ยท (โโ๐ต))) + ((i ยท (โโ๐ด)) ยท (โโ๐ต))))) |
88 | 79, 82, 87 | 3eqtr4d 2787 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด) ยท
((โโ๐ต) โ
(i ยท (โโ๐ต)))) โ ((i ยท
(โโ๐ด)) ยท
((โโ๐ต) โ
(i ยท (โโ๐ต))))) = ((โโ(๐ด ยท ๐ต)) โ (i ยท (โโ(๐ด ยท ๐ต))))) |
89 | 76, 78, 88 | 3eqtrd 2781 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด)
ยท (โโ๐ต)) = ((โโ(๐ด ยท ๐ต)) โ (i ยท (โโ(๐ด ยท ๐ต))))) |
90 | 73, 89 | eqtr4d 2780 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด ยท
๐ต)) =
((โโ๐ด)
ยท (โโ๐ต))) |
91 | 66, 70, 90 | 3jca 1129 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ(๐ด ยท
๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต))) โง (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต))) โง (โโ(๐ด ยท ๐ต)) = ((โโ๐ด) ยท (โโ๐ต)))) |