Step | Hyp | Ref
| Expression |
1 | | sharhght.a |
. . . . . . . 8
โข (๐ โ (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) |
2 | 1 | simp1d 1143 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
3 | 1 | simp3d 1145 |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
4 | | sharhght.b |
. . . . . . . 8
โข (๐ โ (๐ท โ โ โง ((๐ด โ ๐ท)๐บ(๐ต โ ๐ท)) = 0)) |
5 | 4 | simpld 496 |
. . . . . . 7
โข (๐ โ ๐ท โ โ) |
6 | 2, 3, 5 | nnncan1d 11553 |
. . . . . 6
โข (๐ โ ((๐ด โ ๐ถ) โ (๐ด โ ๐ท)) = (๐ท โ ๐ถ)) |
7 | 6 | oveq2d 7378 |
. . . . 5
โข (๐ โ ((๐ต โ ๐ท)๐บ((๐ด โ ๐ถ) โ (๐ด โ ๐ท))) = ((๐ต โ ๐ท)๐บ(๐ท โ ๐ถ))) |
8 | 1 | simp2d 1144 |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
9 | 8, 5 | subcld 11519 |
. . . . . 6
โข (๐ โ (๐ต โ ๐ท) โ โ) |
10 | 2, 3 | subcld 11519 |
. . . . . 6
โข (๐ โ (๐ด โ ๐ถ) โ โ) |
11 | 2, 5 | subcld 11519 |
. . . . . 6
โข (๐ โ (๐ด โ ๐ท) โ โ) |
12 | | sharhght.sigar |
. . . . . . 7
โข ๐บ = (๐ฅ โ โ, ๐ฆ โ โ โฆ
(โโ((โโ๐ฅ) ยท ๐ฆ))) |
13 | 12 | sigarms 45171 |
. . . . . 6
โข (((๐ต โ ๐ท) โ โ โง (๐ด โ ๐ถ) โ โ โง (๐ด โ ๐ท) โ โ) โ ((๐ต โ ๐ท)๐บ((๐ด โ ๐ถ) โ (๐ด โ ๐ท))) = (((๐ต โ ๐ท)๐บ(๐ด โ ๐ถ)) โ ((๐ต โ ๐ท)๐บ(๐ด โ ๐ท)))) |
14 | 9, 10, 11, 13 | syl3anc 1372 |
. . . . 5
โข (๐ โ ((๐ต โ ๐ท)๐บ((๐ด โ ๐ถ) โ (๐ด โ ๐ท))) = (((๐ต โ ๐ท)๐บ(๐ด โ ๐ถ)) โ ((๐ต โ ๐ท)๐บ(๐ด โ ๐ท)))) |
15 | 7, 14 | eqtr3d 2779 |
. . . 4
โข (๐ โ ((๐ต โ ๐ท)๐บ(๐ท โ ๐ถ)) = (((๐ต โ ๐ท)๐บ(๐ด โ ๐ถ)) โ ((๐ต โ ๐ท)๐บ(๐ด โ ๐ท)))) |
16 | 12 | sigarac 45167 |
. . . . . . . . 9
โข (((๐ด โ ๐ท) โ โ โง (๐ต โ ๐ท) โ โ) โ ((๐ด โ ๐ท)๐บ(๐ต โ ๐ท)) = -((๐ต โ ๐ท)๐บ(๐ด โ ๐ท))) |
17 | 11, 9, 16 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ ((๐ด โ ๐ท)๐บ(๐ต โ ๐ท)) = -((๐ต โ ๐ท)๐บ(๐ด โ ๐ท))) |
18 | 4 | simprd 497 |
. . . . . . . 8
โข (๐ โ ((๐ด โ ๐ท)๐บ(๐ต โ ๐ท)) = 0) |
19 | 17, 18 | eqtr3d 2779 |
. . . . . . 7
โข (๐ โ -((๐ต โ ๐ท)๐บ(๐ด โ ๐ท)) = 0) |
20 | 19 | negeqd 11402 |
. . . . . 6
โข (๐ โ --((๐ต โ ๐ท)๐บ(๐ด โ ๐ท)) = -0) |
21 | 9, 11 | jca 513 |
. . . . . . . 8
โข (๐ โ ((๐ต โ ๐ท) โ โ โง (๐ด โ ๐ท) โ โ)) |
22 | 12, 21 | sigarimcd 45177 |
. . . . . . 7
โข (๐ โ ((๐ต โ ๐ท)๐บ(๐ด โ ๐ท)) โ โ) |
23 | 22 | negnegd 11510 |
. . . . . 6
โข (๐ โ --((๐ต โ ๐ท)๐บ(๐ด โ ๐ท)) = ((๐ต โ ๐ท)๐บ(๐ด โ ๐ท))) |
24 | | neg0 11454 |
. . . . . . 7
โข -0 =
0 |
25 | 24 | a1i 11 |
. . . . . 6
โข (๐ โ -0 = 0) |
26 | 20, 23, 25 | 3eqtr3d 2785 |
. . . . 5
โข (๐ โ ((๐ต โ ๐ท)๐บ(๐ด โ ๐ท)) = 0) |
27 | 26 | oveq2d 7378 |
. . . 4
โข (๐ โ (((๐ต โ ๐ท)๐บ(๐ด โ ๐ถ)) โ ((๐ต โ ๐ท)๐บ(๐ด โ ๐ท))) = (((๐ต โ ๐ท)๐บ(๐ด โ ๐ถ)) โ 0)) |
28 | 9, 10 | jca 513 |
. . . . . 6
โข (๐ โ ((๐ต โ ๐ท) โ โ โง (๐ด โ ๐ถ) โ โ)) |
29 | 12, 28 | sigarimcd 45177 |
. . . . 5
โข (๐ โ ((๐ต โ ๐ท)๐บ(๐ด โ ๐ถ)) โ โ) |
30 | 29 | subid1d 11508 |
. . . 4
โข (๐ โ (((๐ต โ ๐ท)๐บ(๐ด โ ๐ถ)) โ 0) = ((๐ต โ ๐ท)๐บ(๐ด โ ๐ถ))) |
31 | 15, 27, 30 | 3eqtrd 2781 |
. . 3
โข (๐ โ ((๐ต โ ๐ท)๐บ(๐ท โ ๐ถ)) = ((๐ต โ ๐ท)๐บ(๐ด โ ๐ถ))) |
32 | 8, 5, 3 | nnncan2d 11554 |
. . . 4
โข (๐ โ ((๐ต โ ๐ถ) โ (๐ท โ ๐ถ)) = (๐ต โ ๐ท)) |
33 | 32 | oveq1d 7377 |
. . 3
โข (๐ โ (((๐ต โ ๐ถ) โ (๐ท โ ๐ถ))๐บ(๐ด โ ๐ถ)) = ((๐ต โ ๐ท)๐บ(๐ด โ ๐ถ))) |
34 | 8, 3 | subcld 11519 |
. . . 4
โข (๐ โ (๐ต โ ๐ถ) โ โ) |
35 | 5, 3 | subcld 11519 |
. . . 4
โข (๐ โ (๐ท โ ๐ถ) โ โ) |
36 | 12 | sigarmf 45169 |
. . . 4
โข (((๐ต โ ๐ถ) โ โ โง (๐ด โ ๐ถ) โ โ โง (๐ท โ ๐ถ) โ โ) โ (((๐ต โ ๐ถ) โ (๐ท โ ๐ถ))๐บ(๐ด โ ๐ถ)) = (((๐ต โ ๐ถ)๐บ(๐ด โ ๐ถ)) โ ((๐ท โ ๐ถ)๐บ(๐ด โ ๐ถ)))) |
37 | 34, 10, 35, 36 | syl3anc 1372 |
. . 3
โข (๐ โ (((๐ต โ ๐ถ) โ (๐ท โ ๐ถ))๐บ(๐ด โ ๐ถ)) = (((๐ต โ ๐ถ)๐บ(๐ด โ ๐ถ)) โ ((๐ท โ ๐ถ)๐บ(๐ด โ ๐ถ)))) |
38 | 31, 33, 37 | 3eqtr2rd 2784 |
. 2
โข (๐ โ (((๐ต โ ๐ถ)๐บ(๐ด โ ๐ถ)) โ ((๐ท โ ๐ถ)๐บ(๐ด โ ๐ถ))) = ((๐ต โ ๐ท)๐บ(๐ท โ ๐ถ))) |
39 | 3, 5 | subcld 11519 |
. . . 4
โข (๐ โ (๐ถ โ ๐ท) โ โ) |
40 | | 1red 11163 |
. . . . 5
โข (๐ โ 1 โ
โ) |
41 | 40 | renegcld 11589 |
. . . 4
โข (๐ โ -1 โ
โ) |
42 | 12 | sigarls 45172 |
. . . 4
โข (((๐ต โ ๐ท) โ โ โง (๐ถ โ ๐ท) โ โ โง -1 โ โ)
โ ((๐ต โ ๐ท)๐บ((๐ถ โ ๐ท) ยท -1)) = (((๐ต โ ๐ท)๐บ(๐ถ โ ๐ท)) ยท -1)) |
43 | 9, 39, 41, 42 | syl3anc 1372 |
. . 3
โข (๐ โ ((๐ต โ ๐ท)๐บ((๐ถ โ ๐ท) ยท -1)) = (((๐ต โ ๐ท)๐บ(๐ถ โ ๐ท)) ยท -1)) |
44 | 39 | mulm1d 11614 |
. . . . 5
โข (๐ โ (-1 ยท (๐ถ โ ๐ท)) = -(๐ถ โ ๐ท)) |
45 | | 1cnd 11157 |
. . . . . . 7
โข (๐ โ 1 โ
โ) |
46 | 45 | negcld 11506 |
. . . . . 6
โข (๐ โ -1 โ
โ) |
47 | 46, 39 | mulcomd 11183 |
. . . . 5
โข (๐ โ (-1 ยท (๐ถ โ ๐ท)) = ((๐ถ โ ๐ท) ยท -1)) |
48 | 3, 5 | negsubdi2d 11535 |
. . . . 5
โข (๐ โ -(๐ถ โ ๐ท) = (๐ท โ ๐ถ)) |
49 | 44, 47, 48 | 3eqtr3d 2785 |
. . . 4
โข (๐ โ ((๐ถ โ ๐ท) ยท -1) = (๐ท โ ๐ถ)) |
50 | 49 | oveq2d 7378 |
. . 3
โข (๐ โ ((๐ต โ ๐ท)๐บ((๐ถ โ ๐ท) ยท -1)) = ((๐ต โ ๐ท)๐บ(๐ท โ ๐ถ))) |
51 | 9, 39 | jca 513 |
. . . . . 6
โข (๐ โ ((๐ต โ ๐ท) โ โ โง (๐ถ โ ๐ท) โ โ)) |
52 | 12, 51 | sigarimcd 45177 |
. . . . 5
โข (๐ โ ((๐ต โ ๐ท)๐บ(๐ถ โ ๐ท)) โ โ) |
53 | 52 | mulm1d 11614 |
. . . 4
โข (๐ โ (-1 ยท ((๐ต โ ๐ท)๐บ(๐ถ โ ๐ท))) = -((๐ต โ ๐ท)๐บ(๐ถ โ ๐ท))) |
54 | 52, 46 | mulcomd 11183 |
. . . 4
โข (๐ โ (((๐ต โ ๐ท)๐บ(๐ถ โ ๐ท)) ยท -1) = (-1 ยท ((๐ต โ ๐ท)๐บ(๐ถ โ ๐ท)))) |
55 | 12 | sigarac 45167 |
. . . . 5
โข (((๐ถ โ ๐ท) โ โ โง (๐ต โ ๐ท) โ โ) โ ((๐ถ โ ๐ท)๐บ(๐ต โ ๐ท)) = -((๐ต โ ๐ท)๐บ(๐ถ โ ๐ท))) |
56 | 39, 9, 55 | syl2anc 585 |
. . . 4
โข (๐ โ ((๐ถ โ ๐ท)๐บ(๐ต โ ๐ท)) = -((๐ต โ ๐ท)๐บ(๐ถ โ ๐ท))) |
57 | 53, 54, 56 | 3eqtr4d 2787 |
. . 3
โข (๐ โ (((๐ต โ ๐ท)๐บ(๐ถ โ ๐ท)) ยท -1) = ((๐ถ โ ๐ท)๐บ(๐ต โ ๐ท))) |
58 | 43, 50, 57 | 3eqtr3d 2785 |
. 2
โข (๐ โ ((๐ต โ ๐ท)๐บ(๐ท โ ๐ถ)) = ((๐ถ โ ๐ท)๐บ(๐ต โ ๐ท))) |
59 | 12 | sigarperm 45175 |
. . 3
โข ((๐ถ โ โ โง ๐ต โ โ โง ๐ท โ โ) โ ((๐ถ โ ๐ท)๐บ(๐ต โ ๐ท)) = ((๐ต โ ๐ถ)๐บ(๐ท โ ๐ถ))) |
60 | 3, 8, 5, 59 | syl3anc 1372 |
. 2
โข (๐ โ ((๐ถ โ ๐ท)๐บ(๐ต โ ๐ท)) = ((๐ต โ ๐ถ)๐บ(๐ท โ ๐ถ))) |
61 | 38, 58, 60 | 3eqtrd 2781 |
1
โข (๐ โ (((๐ต โ ๐ถ)๐บ(๐ด โ ๐ถ)) โ ((๐ท โ ๐ถ)๐บ(๐ด โ ๐ถ))) = ((๐ต โ ๐ถ)๐บ(๐ท โ ๐ถ))) |