Step | Hyp | Ref
| Expression |
1 | | oveq1 7368 |
. . . 4
โข (๐ฅ = ๐ด โ (๐ฅ ยทe ๐ต) = (๐ด ยทe ๐ต)) |
2 | 1 | oveq1d 7376 |
. . 3
โข (๐ฅ = ๐ด โ ((๐ฅ ยทe ๐ต) ยทe ๐ถ) = ((๐ด ยทe ๐ต) ยทe ๐ถ)) |
3 | | oveq1 7368 |
. . 3
โข (๐ฅ = ๐ด โ (๐ฅ ยทe (๐ต ยทe ๐ถ)) = (๐ด ยทe (๐ต ยทe ๐ถ))) |
4 | 2, 3 | eqeq12d 2749 |
. 2
โข (๐ฅ = ๐ด โ (((๐ฅ ยทe ๐ต) ยทe ๐ถ) = (๐ฅ ยทe (๐ต ยทe ๐ถ)) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (๐ด ยทe (๐ต ยทe ๐ถ)))) |
5 | | oveq1 7368 |
. . . 4
โข (๐ฅ = -๐๐ด โ (๐ฅ ยทe ๐ต) = (-๐๐ด ยทe ๐ต)) |
6 | 5 | oveq1d 7376 |
. . 3
โข (๐ฅ = -๐๐ด โ ((๐ฅ ยทe ๐ต) ยทe ๐ถ) = ((-๐๐ด ยทe ๐ต) ยทe ๐ถ)) |
7 | | oveq1 7368 |
. . 3
โข (๐ฅ = -๐๐ด โ (๐ฅ ยทe (๐ต ยทe ๐ถ)) = (-๐๐ด ยทe (๐ต ยทe ๐ถ))) |
8 | 6, 7 | eqeq12d 2749 |
. 2
โข (๐ฅ = -๐๐ด โ (((๐ฅ ยทe ๐ต) ยทe ๐ถ) = (๐ฅ ยทe (๐ต ยทe ๐ถ)) โ ((-๐๐ด ยทe ๐ต) ยทe ๐ถ) = (-๐๐ด ยทe (๐ต ยทe ๐ถ)))) |
9 | | xmulcl 13201 |
. . 3
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ (๐ด ยทe ๐ต) โ
โ*) |
10 | | xmulcl 13201 |
. . 3
โข (((๐ด ยทe ๐ต) โ โ*
โง ๐ถ โ
โ*) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) โ
โ*) |
11 | 9, 10 | stoic3 1779 |
. 2
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) โ
โ*) |
12 | | simp1 1137 |
. . 3
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โ ๐ด โ
โ*) |
13 | | xmulcl 13201 |
. . . 4
โข ((๐ต โ โ*
โง ๐ถ โ
โ*) โ (๐ต ยทe ๐ถ) โ
โ*) |
14 | 13 | 3adant1 1131 |
. . 3
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โ (๐ต ยทe ๐ถ) โ
โ*) |
15 | | xmulcl 13201 |
. . 3
โข ((๐ด โ โ*
โง (๐ต
ยทe ๐ถ)
โ โ*) โ (๐ด ยทe (๐ต ยทe ๐ถ)) โ
โ*) |
16 | 12, 14, 15 | syl2anc 585 |
. 2
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โ (๐ด ยทe (๐ต ยทe ๐ถ)) โ
โ*) |
17 | | oveq2 7369 |
. . . . 5
โข (๐ฆ = ๐ต โ (๐ฅ ยทe ๐ฆ) = (๐ฅ ยทe ๐ต)) |
18 | 17 | oveq1d 7376 |
. . . 4
โข (๐ฆ = ๐ต โ ((๐ฅ ยทe ๐ฆ) ยทe ๐ถ) = ((๐ฅ ยทe ๐ต) ยทe ๐ถ)) |
19 | | oveq1 7368 |
. . . . 5
โข (๐ฆ = ๐ต โ (๐ฆ ยทe ๐ถ) = (๐ต ยทe ๐ถ)) |
20 | 19 | oveq2d 7377 |
. . . 4
โข (๐ฆ = ๐ต โ (๐ฅ ยทe (๐ฆ ยทe ๐ถ)) = (๐ฅ ยทe (๐ต ยทe ๐ถ))) |
21 | 18, 20 | eqeq12d 2749 |
. . 3
โข (๐ฆ = ๐ต โ (((๐ฅ ยทe ๐ฆ) ยทe ๐ถ) = (๐ฅ ยทe (๐ฆ ยทe ๐ถ)) โ ((๐ฅ ยทe ๐ต) ยทe ๐ถ) = (๐ฅ ยทe (๐ต ยทe ๐ถ)))) |
22 | | oveq2 7369 |
. . . . 5
โข (๐ฆ = -๐๐ต โ (๐ฅ ยทe ๐ฆ) = (๐ฅ ยทe
-๐๐ต)) |
23 | 22 | oveq1d 7376 |
. . . 4
โข (๐ฆ = -๐๐ต โ ((๐ฅ ยทe ๐ฆ) ยทe ๐ถ) = ((๐ฅ ยทe
-๐๐ต)
ยทe ๐ถ)) |
24 | | oveq1 7368 |
. . . . 5
โข (๐ฆ = -๐๐ต โ (๐ฆ ยทe ๐ถ) = (-๐๐ต ยทe ๐ถ)) |
25 | 24 | oveq2d 7377 |
. . . 4
โข (๐ฆ = -๐๐ต โ (๐ฅ ยทe (๐ฆ ยทe ๐ถ)) = (๐ฅ ยทe
(-๐๐ต
ยทe ๐ถ))) |
26 | 23, 25 | eqeq12d 2749 |
. . 3
โข (๐ฆ = -๐๐ต โ (((๐ฅ ยทe ๐ฆ) ยทe ๐ถ) = (๐ฅ ยทe (๐ฆ ยทe ๐ถ)) โ ((๐ฅ ยทe
-๐๐ต)
ยทe ๐ถ) =
(๐ฅ ยทe
(-๐๐ต
ยทe ๐ถ)))) |
27 | | simprl 770 |
. . . . 5
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ ๐ฅ โ
โ*) |
28 | | simpl2 1193 |
. . . . 5
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ ๐ต โ
โ*) |
29 | | xmulcl 13201 |
. . . . 5
โข ((๐ฅ โ โ*
โง ๐ต โ
โ*) โ (๐ฅ ยทe ๐ต) โ
โ*) |
30 | 27, 28, 29 | syl2anc 585 |
. . . 4
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ (๐ฅ ยทe ๐ต) โ
โ*) |
31 | | simpl3 1194 |
. . . 4
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ ๐ถ โ
โ*) |
32 | | xmulcl 13201 |
. . . 4
โข (((๐ฅ ยทe ๐ต) โ โ*
โง ๐ถ โ
โ*) โ ((๐ฅ ยทe ๐ต) ยทe ๐ถ) โ
โ*) |
33 | 30, 31, 32 | syl2anc 585 |
. . 3
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ ((๐ฅ ยทe ๐ต) ยทe ๐ถ) โ
โ*) |
34 | 14 | adantr 482 |
. . . 4
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ (๐ต ยทe ๐ถ) โ
โ*) |
35 | | xmulcl 13201 |
. . . 4
โข ((๐ฅ โ โ*
โง (๐ต
ยทe ๐ถ)
โ โ*) โ (๐ฅ ยทe (๐ต ยทe ๐ถ)) โ
โ*) |
36 | 27, 34, 35 | syl2anc 585 |
. . 3
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ (๐ฅ ยทe (๐ต ยทe ๐ถ)) โ
โ*) |
37 | | oveq2 7369 |
. . . . 5
โข (๐ง = ๐ถ โ ((๐ฅ ยทe ๐ฆ) ยทe ๐ง) = ((๐ฅ ยทe ๐ฆ) ยทe ๐ถ)) |
38 | | oveq2 7369 |
. . . . . 6
โข (๐ง = ๐ถ โ (๐ฆ ยทe ๐ง) = (๐ฆ ยทe ๐ถ)) |
39 | 38 | oveq2d 7377 |
. . . . 5
โข (๐ง = ๐ถ โ (๐ฅ ยทe (๐ฆ ยทe ๐ง)) = (๐ฅ ยทe (๐ฆ ยทe ๐ถ))) |
40 | 37, 39 | eqeq12d 2749 |
. . . 4
โข (๐ง = ๐ถ โ (((๐ฅ ยทe ๐ฆ) ยทe ๐ง) = (๐ฅ ยทe (๐ฆ ยทe ๐ง)) โ ((๐ฅ ยทe ๐ฆ) ยทe ๐ถ) = (๐ฅ ยทe (๐ฆ ยทe ๐ถ)))) |
41 | | oveq2 7369 |
. . . . 5
โข (๐ง = -๐๐ถ โ ((๐ฅ ยทe ๐ฆ) ยทe ๐ง) = ((๐ฅ ยทe ๐ฆ) ยทe
-๐๐ถ)) |
42 | | oveq2 7369 |
. . . . . 6
โข (๐ง = -๐๐ถ โ (๐ฆ ยทe ๐ง) = (๐ฆ ยทe
-๐๐ถ)) |
43 | 42 | oveq2d 7377 |
. . . . 5
โข (๐ง = -๐๐ถ โ (๐ฅ ยทe (๐ฆ ยทe ๐ง)) = (๐ฅ ยทe (๐ฆ ยทe
-๐๐ถ))) |
44 | 41, 43 | eqeq12d 2749 |
. . . 4
โข (๐ง = -๐๐ถ โ (((๐ฅ ยทe ๐ฆ) ยทe ๐ง) = (๐ฅ ยทe (๐ฆ ยทe ๐ง)) โ ((๐ฅ ยทe ๐ฆ) ยทe
-๐๐ถ) =
(๐ฅ ยทe
(๐ฆ ยทe
-๐๐ถ)))) |
45 | 27 | adantr 482 |
. . . . . 6
โข ((((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โง (๐ฆ โ โ*
โง 0 < ๐ฆ)) โ
๐ฅ โ
โ*) |
46 | | simprl 770 |
. . . . . 6
โข ((((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โง (๐ฆ โ โ*
โง 0 < ๐ฆ)) โ
๐ฆ โ
โ*) |
47 | | xmulcl 13201 |
. . . . . 6
โข ((๐ฅ โ โ*
โง ๐ฆ โ
โ*) โ (๐ฅ ยทe ๐ฆ) โ
โ*) |
48 | 45, 46, 47 | syl2anc 585 |
. . . . 5
โข ((((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โง (๐ฆ โ โ*
โง 0 < ๐ฆ)) โ
(๐ฅ ยทe
๐ฆ) โ
โ*) |
49 | 31 | adantr 482 |
. . . . 5
โข ((((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โง (๐ฆ โ โ*
โง 0 < ๐ฆ)) โ
๐ถ โ
โ*) |
50 | | xmulcl 13201 |
. . . . 5
โข (((๐ฅ ยทe ๐ฆ) โ โ*
โง ๐ถ โ
โ*) โ ((๐ฅ ยทe ๐ฆ) ยทe ๐ถ) โ
โ*) |
51 | 48, 49, 50 | syl2anc 585 |
. . . 4
โข ((((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โง (๐ฆ โ โ*
โง 0 < ๐ฆ)) โ
((๐ฅ ยทe
๐ฆ) ยทe
๐ถ) โ
โ*) |
52 | | xmulcl 13201 |
. . . . . 6
โข ((๐ฆ โ โ*
โง ๐ถ โ
โ*) โ (๐ฆ ยทe ๐ถ) โ
โ*) |
53 | 46, 49, 52 | syl2anc 585 |
. . . . 5
โข ((((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โง (๐ฆ โ โ*
โง 0 < ๐ฆ)) โ
(๐ฆ ยทe
๐ถ) โ
โ*) |
54 | | xmulcl 13201 |
. . . . 5
โข ((๐ฅ โ โ*
โง (๐ฆ
ยทe ๐ถ)
โ โ*) โ (๐ฅ ยทe (๐ฆ ยทe ๐ถ)) โ
โ*) |
55 | 45, 53, 54 | syl2anc 585 |
. . . 4
โข ((((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โง (๐ฆ โ โ*
โง 0 < ๐ฆ)) โ
(๐ฅ ยทe
(๐ฆ ยทe
๐ถ)) โ
โ*) |
56 | | xmulasslem3 13214 |
. . . . 5
โข (((๐ฅ โ โ*
โง 0 < ๐ฅ) โง
(๐ฆ โ
โ* โง 0 < ๐ฆ) โง (๐ง โ โ* โง 0 <
๐ง)) โ ((๐ฅ ยทe ๐ฆ) ยทe ๐ง) = (๐ฅ ยทe (๐ฆ ยทe ๐ง))) |
57 | 56 | ad4ant234 1176 |
. . . 4
โข
(((((๐ด โ
โ* โง ๐ต
โ โ* โง ๐ถ โ โ*) โง (๐ฅ โ โ*
โง 0 < ๐ฅ)) โง
(๐ฆ โ
โ* โง 0 < ๐ฆ)) โง (๐ง โ โ* โง 0 <
๐ง)) โ ((๐ฅ ยทe ๐ฆ) ยทe ๐ง) = (๐ฅ ยทe (๐ฆ ยทe ๐ง))) |
58 | | xmul01 13195 |
. . . . . . . 8
โข ((๐ฅ ยทe ๐ฆ) โ โ*
โ ((๐ฅ
ยทe ๐ฆ)
ยทe 0) = 0) |
59 | 48, 58 | syl 17 |
. . . . . . 7
โข ((((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โง (๐ฆ โ โ*
โง 0 < ๐ฆ)) โ
((๐ฅ ยทe
๐ฆ) ยทe 0)
= 0) |
60 | | xmul01 13195 |
. . . . . . . 8
โข (๐ฅ โ โ*
โ (๐ฅ
ยทe 0) = 0) |
61 | 45, 60 | syl 17 |
. . . . . . 7
โข ((((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โง (๐ฆ โ โ*
โง 0 < ๐ฆ)) โ
(๐ฅ ยทe 0)
= 0) |
62 | 59, 61 | eqtr4d 2776 |
. . . . . 6
โข ((((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โง (๐ฆ โ โ*
โง 0 < ๐ฆ)) โ
((๐ฅ ยทe
๐ฆ) ยทe 0)
= (๐ฅ ยทe
0)) |
63 | | xmul01 13195 |
. . . . . . . 8
โข (๐ฆ โ โ*
โ (๐ฆ
ยทe 0) = 0) |
64 | 63 | ad2antrl 727 |
. . . . . . 7
โข ((((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โง (๐ฆ โ โ*
โง 0 < ๐ฆ)) โ
(๐ฆ ยทe 0)
= 0) |
65 | 64 | oveq2d 7377 |
. . . . . 6
โข ((((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โง (๐ฆ โ โ*
โง 0 < ๐ฆ)) โ
(๐ฅ ยทe
(๐ฆ ยทe 0))
= (๐ฅ ยทe
0)) |
66 | 62, 65 | eqtr4d 2776 |
. . . . 5
โข ((((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โง (๐ฆ โ โ*
โง 0 < ๐ฆ)) โ
((๐ฅ ยทe
๐ฆ) ยทe 0)
= (๐ฅ ยทe
(๐ฆ ยทe
0))) |
67 | | oveq2 7369 |
. . . . . 6
โข (๐ง = 0 โ ((๐ฅ ยทe ๐ฆ) ยทe ๐ง) = ((๐ฅ ยทe ๐ฆ) ยทe 0)) |
68 | | oveq2 7369 |
. . . . . . 7
โข (๐ง = 0 โ (๐ฆ ยทe ๐ง) = (๐ฆ ยทe 0)) |
69 | 68 | oveq2d 7377 |
. . . . . 6
โข (๐ง = 0 โ (๐ฅ ยทe (๐ฆ ยทe ๐ง)) = (๐ฅ ยทe (๐ฆ ยทe 0))) |
70 | 67, 69 | eqeq12d 2749 |
. . . . 5
โข (๐ง = 0 โ (((๐ฅ ยทe ๐ฆ) ยทe ๐ง) = (๐ฅ ยทe (๐ฆ ยทe ๐ง)) โ ((๐ฅ ยทe ๐ฆ) ยทe 0) = (๐ฅ ยทe (๐ฆ ยทe
0)))) |
71 | 66, 70 | syl5ibrcom 247 |
. . . 4
โข ((((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โง (๐ฆ โ โ*
โง 0 < ๐ฆ)) โ
(๐ง = 0 โ ((๐ฅ ยทe ๐ฆ) ยทe ๐ง) = (๐ฅ ยทe (๐ฆ ยทe ๐ง)))) |
72 | | xmulneg2 13198 |
. . . . 5
โข (((๐ฅ ยทe ๐ฆ) โ โ*
โง ๐ถ โ
โ*) โ ((๐ฅ ยทe ๐ฆ) ยทe
-๐๐ถ) =
-๐((๐ฅ
ยทe ๐ฆ)
ยทe ๐ถ)) |
73 | 48, 49, 72 | syl2anc 585 |
. . . 4
โข ((((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โง (๐ฆ โ โ*
โง 0 < ๐ฆ)) โ
((๐ฅ ยทe
๐ฆ) ยทe
-๐๐ถ) =
-๐((๐ฅ
ยทe ๐ฆ)
ยทe ๐ถ)) |
74 | | xmulneg2 13198 |
. . . . . . 7
โข ((๐ฆ โ โ*
โง ๐ถ โ
โ*) โ (๐ฆ ยทe
-๐๐ถ) =
-๐(๐ฆ
ยทe ๐ถ)) |
75 | 46, 49, 74 | syl2anc 585 |
. . . . . 6
โข ((((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โง (๐ฆ โ โ*
โง 0 < ๐ฆ)) โ
(๐ฆ ยทe
-๐๐ถ) =
-๐(๐ฆ
ยทe ๐ถ)) |
76 | 75 | oveq2d 7377 |
. . . . 5
โข ((((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โง (๐ฆ โ โ*
โง 0 < ๐ฆ)) โ
(๐ฅ ยทe
(๐ฆ ยทe
-๐๐ถ)) =
(๐ฅ ยทe
-๐(๐ฆ
ยทe ๐ถ))) |
77 | | xmulneg2 13198 |
. . . . . 6
โข ((๐ฅ โ โ*
โง (๐ฆ
ยทe ๐ถ)
โ โ*) โ (๐ฅ ยทe
-๐(๐ฆ
ยทe ๐ถ)) =
-๐(๐ฅ
ยทe (๐ฆ
ยทe ๐ถ))) |
78 | 45, 53, 77 | syl2anc 585 |
. . . . 5
โข ((((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โง (๐ฆ โ โ*
โง 0 < ๐ฆ)) โ
(๐ฅ ยทe
-๐(๐ฆ
ยทe ๐ถ)) =
-๐(๐ฅ
ยทe (๐ฆ
ยทe ๐ถ))) |
79 | 76, 78 | eqtrd 2773 |
. . . 4
โข ((((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โง (๐ฆ โ โ*
โง 0 < ๐ฆ)) โ
(๐ฅ ยทe
(๐ฆ ยทe
-๐๐ถ)) =
-๐(๐ฅ
ยทe (๐ฆ
ยทe ๐ถ))) |
80 | 40, 44, 51, 55, 49, 57, 71, 73, 79 | xmulasslem 13213 |
. . 3
โข ((((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โง (๐ฆ โ โ*
โง 0 < ๐ฆ)) โ
((๐ฅ ยทe
๐ฆ) ยทe
๐ถ) = (๐ฅ ยทe (๐ฆ ยทe ๐ถ))) |
81 | | xmul02 13196 |
. . . . . . . 8
โข (๐ถ โ โ*
โ (0 ยทe ๐ถ) = 0) |
82 | 81 | 3ad2ant3 1136 |
. . . . . . 7
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โ (0 ยทe ๐ถ) = 0) |
83 | 82 | adantr 482 |
. . . . . 6
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ (0
ยทe ๐ถ) =
0) |
84 | 60 | ad2antrl 727 |
. . . . . 6
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ (๐ฅ ยทe 0) =
0) |
85 | 83, 84 | eqtr4d 2776 |
. . . . 5
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ (0
ยทe ๐ถ) =
(๐ฅ ยทe
0)) |
86 | 84 | oveq1d 7376 |
. . . . 5
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ ((๐ฅ ยทe 0)
ยทe ๐ถ) =
(0 ยทe ๐ถ)) |
87 | 83 | oveq2d 7377 |
. . . . 5
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ (๐ฅ ยทe (0
ยทe ๐ถ)) =
(๐ฅ ยทe
0)) |
88 | 85, 86, 87 | 3eqtr4d 2783 |
. . . 4
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ ((๐ฅ ยทe 0)
ยทe ๐ถ) =
(๐ฅ ยทe (0
ยทe ๐ถ))) |
89 | | oveq2 7369 |
. . . . . 6
โข (๐ฆ = 0 โ (๐ฅ ยทe ๐ฆ) = (๐ฅ ยทe 0)) |
90 | 89 | oveq1d 7376 |
. . . . 5
โข (๐ฆ = 0 โ ((๐ฅ ยทe ๐ฆ) ยทe ๐ถ) = ((๐ฅ ยทe 0) ยทe
๐ถ)) |
91 | | oveq1 7368 |
. . . . . 6
โข (๐ฆ = 0 โ (๐ฆ ยทe ๐ถ) = (0 ยทe ๐ถ)) |
92 | 91 | oveq2d 7377 |
. . . . 5
โข (๐ฆ = 0 โ (๐ฅ ยทe (๐ฆ ยทe ๐ถ)) = (๐ฅ ยทe (0 ยทe
๐ถ))) |
93 | 90, 92 | eqeq12d 2749 |
. . . 4
โข (๐ฆ = 0 โ (((๐ฅ ยทe ๐ฆ) ยทe ๐ถ) = (๐ฅ ยทe (๐ฆ ยทe ๐ถ)) โ ((๐ฅ ยทe 0) ยทe
๐ถ) = (๐ฅ ยทe (0 ยทe
๐ถ)))) |
94 | 88, 93 | syl5ibrcom 247 |
. . 3
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ (๐ฆ = 0 โ ((๐ฅ ยทe ๐ฆ) ยทe ๐ถ) = (๐ฅ ยทe (๐ฆ ยทe ๐ถ)))) |
95 | | xmulneg2 13198 |
. . . . . 6
โข ((๐ฅ โ โ*
โง ๐ต โ
โ*) โ (๐ฅ ยทe
-๐๐ต) =
-๐(๐ฅ
ยทe ๐ต)) |
96 | 27, 28, 95 | syl2anc 585 |
. . . . 5
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ (๐ฅ ยทe
-๐๐ต) =
-๐(๐ฅ
ยทe ๐ต)) |
97 | 96 | oveq1d 7376 |
. . . 4
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ ((๐ฅ ยทe
-๐๐ต)
ยทe ๐ถ) =
(-๐(๐ฅ
ยทe ๐ต)
ยทe ๐ถ)) |
98 | | xmulneg1 13197 |
. . . . 5
โข (((๐ฅ ยทe ๐ต) โ โ*
โง ๐ถ โ
โ*) โ (-๐(๐ฅ ยทe ๐ต) ยทe ๐ถ) = -๐((๐ฅ ยทe ๐ต) ยทe ๐ถ)) |
99 | 30, 31, 98 | syl2anc 585 |
. . . 4
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ
(-๐(๐ฅ
ยทe ๐ต)
ยทe ๐ถ) =
-๐((๐ฅ
ยทe ๐ต)
ยทe ๐ถ)) |
100 | 97, 99 | eqtrd 2773 |
. . 3
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ ((๐ฅ ยทe
-๐๐ต)
ยทe ๐ถ) =
-๐((๐ฅ
ยทe ๐ต)
ยทe ๐ถ)) |
101 | | xmulneg1 13197 |
. . . . . 6
โข ((๐ต โ โ*
โง ๐ถ โ
โ*) โ (-๐๐ต ยทe ๐ถ) = -๐(๐ต ยทe ๐ถ)) |
102 | 28, 31, 101 | syl2anc 585 |
. . . . 5
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ
(-๐๐ต
ยทe ๐ถ) =
-๐(๐ต
ยทe ๐ถ)) |
103 | 102 | oveq2d 7377 |
. . . 4
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ (๐ฅ ยทe
(-๐๐ต
ยทe ๐ถ)) =
(๐ฅ ยทe
-๐(๐ต
ยทe ๐ถ))) |
104 | | xmulneg2 13198 |
. . . . 5
โข ((๐ฅ โ โ*
โง (๐ต
ยทe ๐ถ)
โ โ*) โ (๐ฅ ยทe
-๐(๐ต
ยทe ๐ถ)) =
-๐(๐ฅ
ยทe (๐ต
ยทe ๐ถ))) |
105 | 27, 34, 104 | syl2anc 585 |
. . . 4
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ (๐ฅ ยทe
-๐(๐ต
ยทe ๐ถ)) =
-๐(๐ฅ
ยทe (๐ต
ยทe ๐ถ))) |
106 | 103, 105 | eqtrd 2773 |
. . 3
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ (๐ฅ ยทe
(-๐๐ต
ยทe ๐ถ)) =
-๐(๐ฅ
ยทe (๐ต
ยทe ๐ถ))) |
107 | 21, 26, 33, 36, 28, 80, 94, 100, 106 | xmulasslem 13213 |
. 2
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง (๐ฅ โ โ* โง 0 <
๐ฅ)) โ ((๐ฅ ยทe ๐ต) ยทe ๐ถ) = (๐ฅ ยทe (๐ต ยทe ๐ถ))) |
108 | | xmul02 13196 |
. . . . . 6
โข (๐ต โ โ*
โ (0 ยทe ๐ต) = 0) |
109 | 108 | 3ad2ant2 1135 |
. . . . 5
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โ (0 ยทe ๐ต) = 0) |
110 | 109 | oveq1d 7376 |
. . . 4
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โ ((0 ยทe ๐ต) ยทe ๐ถ) = (0 ยทe ๐ถ)) |
111 | | xmul02 13196 |
. . . . 5
โข ((๐ต ยทe ๐ถ) โ โ*
โ (0 ยทe (๐ต ยทe ๐ถ)) = 0) |
112 | 14, 111 | syl 17 |
. . . 4
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โ (0 ยทe (๐ต ยทe ๐ถ)) = 0) |
113 | 82, 110, 112 | 3eqtr4d 2783 |
. . 3
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โ ((0 ยทe ๐ต) ยทe ๐ถ) = (0 ยทe (๐ต ยทe ๐ถ))) |
114 | | oveq1 7368 |
. . . . 5
โข (๐ฅ = 0 โ (๐ฅ ยทe ๐ต) = (0 ยทe ๐ต)) |
115 | 114 | oveq1d 7376 |
. . . 4
โข (๐ฅ = 0 โ ((๐ฅ ยทe ๐ต) ยทe ๐ถ) = ((0 ยทe ๐ต) ยทe ๐ถ)) |
116 | | oveq1 7368 |
. . . 4
โข (๐ฅ = 0 โ (๐ฅ ยทe (๐ต ยทe ๐ถ)) = (0 ยทe (๐ต ยทe ๐ถ))) |
117 | 115, 116 | eqeq12d 2749 |
. . 3
โข (๐ฅ = 0 โ (((๐ฅ ยทe ๐ต) ยทe ๐ถ) = (๐ฅ ยทe (๐ต ยทe ๐ถ)) โ ((0 ยทe ๐ต) ยทe ๐ถ) = (0 ยทe
(๐ต ยทe
๐ถ)))) |
118 | 113, 117 | syl5ibrcom 247 |
. 2
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โ (๐ฅ = 0 โ ((๐ฅ ยทe ๐ต) ยทe ๐ถ) = (๐ฅ ยทe (๐ต ยทe ๐ถ)))) |
119 | | xmulneg1 13197 |
. . . . 5
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ (-๐๐ด ยทe ๐ต) = -๐(๐ด ยทe ๐ต)) |
120 | 119 | 3adant3 1133 |
. . . 4
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โ (-๐๐ด ยทe ๐ต) = -๐(๐ด ยทe ๐ต)) |
121 | 120 | oveq1d 7376 |
. . 3
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โ ((-๐๐ด ยทe ๐ต) ยทe ๐ถ) = (-๐(๐ด ยทe ๐ต) ยทe ๐ถ)) |
122 | | xmulneg1 13197 |
. . . 4
โข (((๐ด ยทe ๐ต) โ โ*
โง ๐ถ โ
โ*) โ (-๐(๐ด ยทe ๐ต) ยทe ๐ถ) = -๐((๐ด ยทe ๐ต) ยทe ๐ถ)) |
123 | 9, 122 | stoic3 1779 |
. . 3
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โ (-๐(๐ด ยทe ๐ต) ยทe ๐ถ) = -๐((๐ด ยทe ๐ต) ยทe ๐ถ)) |
124 | 121, 123 | eqtrd 2773 |
. 2
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โ ((-๐๐ด ยทe ๐ต) ยทe ๐ถ) = -๐((๐ด ยทe ๐ต) ยทe ๐ถ)) |
125 | | xmulneg1 13197 |
. . 3
โข ((๐ด โ โ*
โง (๐ต
ยทe ๐ถ)
โ โ*) โ (-๐๐ด ยทe (๐ต ยทe ๐ถ)) = -๐(๐ด ยทe (๐ต ยทe ๐ถ))) |
126 | 12, 14, 125 | syl2anc 585 |
. 2
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โ (-๐๐ด ยทe (๐ต ยทe ๐ถ)) = -๐(๐ด ยทe (๐ต ยทe ๐ถ))) |
127 | 4, 8, 11, 16, 12, 107, 118, 124, 126 | xmulasslem 13213 |
1
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ*) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (๐ด ยทe (๐ต ยทe ๐ถ))) |