Step | Hyp | Ref
| Expression |
1 | | cevath.sigar |
. . . . . . 7
โข ๐บ = (๐ฅ โ โ, ๐ฆ โ โ โฆ
(โโ((โโ๐ฅ) ยท ๐ฆ))) |
2 | | cevath.b |
. . . . . . . . 9
โข (๐ โ (๐น โ โ โง ๐ท โ โ โง ๐ธ โ โ)) |
3 | 2 | simp2d 1143 |
. . . . . . . 8
โข (๐ โ ๐ท โ โ) |
4 | | cevath.a |
. . . . . . . . 9
โข (๐ โ (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) |
5 | 4 | simp1d 1142 |
. . . . . . . 8
โข (๐ โ ๐ด โ โ) |
6 | 4 | simp2d 1143 |
. . . . . . . 8
โข (๐ โ ๐ต โ โ) |
7 | 3, 5, 6 | 3jca 1128 |
. . . . . . 7
โข (๐ โ (๐ท โ โ โง ๐ด โ โ โง ๐ต โ โ)) |
8 | | cevath.c |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
9 | 5, 8 | subcld 11470 |
. . . . . . . . . 10
โข (๐ โ (๐ด โ ๐) โ โ) |
10 | 3, 8 | subcld 11470 |
. . . . . . . . . 10
โข (๐ โ (๐ท โ ๐) โ โ) |
11 | 9, 10 | jca 512 |
. . . . . . . . 9
โข (๐ โ ((๐ด โ ๐) โ โ โง (๐ท โ ๐) โ โ)) |
12 | | cevath.d |
. . . . . . . . . 10
โข (๐ โ (((๐ด โ ๐)๐บ(๐ท โ ๐)) = 0 โง ((๐ต โ ๐)๐บ(๐ธ โ ๐)) = 0 โง ((๐ถ โ ๐)๐บ(๐น โ ๐)) = 0)) |
13 | 12 | simp1d 1142 |
. . . . . . . . 9
โข (๐ โ ((๐ด โ ๐)๐บ(๐ท โ ๐)) = 0) |
14 | 1, 11, 13 | sigariz 45005 |
. . . . . . . 8
โข (๐ โ ((๐ท โ ๐)๐บ(๐ด โ ๐)) = 0) |
15 | 8, 14 | jca 512 |
. . . . . . 7
โข (๐ โ (๐ โ โ โง ((๐ท โ ๐)๐บ(๐ด โ ๐)) = 0)) |
16 | 1, 7, 15 | sigaradd 45008 |
. . . . . 6
โข (๐ โ (((๐ด โ ๐ต)๐บ(๐ท โ ๐ต)) โ ((๐ โ ๐ต)๐บ(๐ท โ ๐ต))) = ((๐ด โ ๐ต)๐บ(๐ โ ๐ต))) |
17 | 1 | sigarperm 45002 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ด โ โ โง ๐ โ โ) โ ((๐ต โ ๐)๐บ(๐ด โ ๐)) = ((๐ด โ ๐ต)๐บ(๐ โ ๐ต))) |
18 | 6, 5, 8, 17 | syl3anc 1371 |
. . . . . 6
โข (๐ โ ((๐ต โ ๐)๐บ(๐ด โ ๐)) = ((๐ด โ ๐ต)๐บ(๐ โ ๐ต))) |
19 | 16, 18 | eqtr4d 2780 |
. . . . 5
โข (๐ โ (((๐ด โ ๐ต)๐บ(๐ท โ ๐ต)) โ ((๐ โ ๐ต)๐บ(๐ท โ ๐ต))) = ((๐ต โ ๐)๐บ(๐ด โ ๐))) |
20 | 19 | oveq1d 7366 |
. . . 4
โข (๐ โ ((((๐ด โ ๐ต)๐บ(๐ท โ ๐ต)) โ ((๐ โ ๐ต)๐บ(๐ท โ ๐ต))) ยท (๐ถ โ ๐ท)) = (((๐ต โ ๐)๐บ(๐ด โ ๐)) ยท (๐ถ โ ๐ท))) |
21 | 5, 6 | subcld 11470 |
. . . . . . 7
โข (๐ โ (๐ด โ ๐ต) โ โ) |
22 | 3, 6 | subcld 11470 |
. . . . . . 7
โข (๐ โ (๐ท โ ๐ต) โ โ) |
23 | 21, 22 | jca 512 |
. . . . . 6
โข (๐ โ ((๐ด โ ๐ต) โ โ โง (๐ท โ ๐ต) โ โ)) |
24 | 1, 23 | sigarimcd 45004 |
. . . . 5
โข (๐ โ ((๐ด โ ๐ต)๐บ(๐ท โ ๐ต)) โ โ) |
25 | 8, 6 | subcld 11470 |
. . . . . . 7
โข (๐ โ (๐ โ ๐ต) โ โ) |
26 | 25, 22 | jca 512 |
. . . . . 6
โข (๐ โ ((๐ โ ๐ต) โ โ โง (๐ท โ ๐ต) โ โ)) |
27 | 1, 26 | sigarimcd 45004 |
. . . . 5
โข (๐ โ ((๐ โ ๐ต)๐บ(๐ท โ ๐ต)) โ โ) |
28 | 4 | simp3d 1144 |
. . . . . 6
โข (๐ โ ๐ถ โ โ) |
29 | 28, 3 | subcld 11470 |
. . . . 5
โข (๐ โ (๐ถ โ ๐ท) โ โ) |
30 | 24, 27, 29 | subdird 11570 |
. . . 4
โข (๐ โ ((((๐ด โ ๐ต)๐บ(๐ท โ ๐ต)) โ ((๐ โ ๐ต)๐บ(๐ท โ ๐ต))) ยท (๐ถ โ ๐ท)) = ((((๐ด โ ๐ต)๐บ(๐ท โ ๐ต)) ยท (๐ถ โ ๐ท)) โ (((๐ โ ๐ต)๐บ(๐ท โ ๐ต)) ยท (๐ถ โ ๐ท)))) |
31 | 20, 30 | eqtr3d 2779 |
. . 3
โข (๐ โ (((๐ต โ ๐)๐บ(๐ด โ ๐)) ยท (๐ถ โ ๐ท)) = ((((๐ด โ ๐ต)๐บ(๐ท โ ๐ต)) ยท (๐ถ โ ๐ท)) โ (((๐ โ ๐ต)๐บ(๐ท โ ๐ต)) ยท (๐ถ โ ๐ท)))) |
32 | 6, 28, 5 | 3jca 1128 |
. . . . 5
โข (๐ โ (๐ต โ โ โง ๐ถ โ โ โง ๐ด โ โ)) |
33 | | cevath.e |
. . . . . . 7
โข (๐ โ (((๐ด โ ๐น)๐บ(๐ต โ ๐น)) = 0 โง ((๐ต โ ๐ท)๐บ(๐ถ โ ๐ท)) = 0 โง ((๐ถ โ ๐ธ)๐บ(๐ด โ ๐ธ)) = 0)) |
34 | 33 | simp2d 1143 |
. . . . . 6
โข (๐ โ ((๐ต โ ๐ท)๐บ(๐ถ โ ๐ท)) = 0) |
35 | 3, 34 | jca 512 |
. . . . 5
โข (๐ โ (๐ท โ โ โง ((๐ต โ ๐ท)๐บ(๐ถ โ ๐ท)) = 0)) |
36 | 1, 32, 35 | sharhght 45007 |
. . . 4
โข (๐ โ (((๐ด โ ๐ต)๐บ(๐ท โ ๐ต)) ยท (๐ถ โ ๐ท)) = (((๐ด โ ๐ถ)๐บ(๐ท โ ๐ถ)) ยท (๐ต โ ๐ท))) |
37 | 6, 28, 8 | 3jca 1128 |
. . . . 5
โข (๐ โ (๐ต โ โ โง ๐ถ โ โ โง ๐ โ โ)) |
38 | 1, 37, 35 | sharhght 45007 |
. . . 4
โข (๐ โ (((๐ โ ๐ต)๐บ(๐ท โ ๐ต)) ยท (๐ถ โ ๐ท)) = (((๐ โ ๐ถ)๐บ(๐ท โ ๐ถ)) ยท (๐ต โ ๐ท))) |
39 | 36, 38 | oveq12d 7369 |
. . 3
โข (๐ โ ((((๐ด โ ๐ต)๐บ(๐ท โ ๐ต)) ยท (๐ถ โ ๐ท)) โ (((๐ โ ๐ต)๐บ(๐ท โ ๐ต)) ยท (๐ถ โ ๐ท))) = ((((๐ด โ ๐ถ)๐บ(๐ท โ ๐ถ)) ยท (๐ต โ ๐ท)) โ (((๐ โ ๐ถ)๐บ(๐ท โ ๐ถ)) ยท (๐ต โ ๐ท)))) |
40 | 5, 28 | subcld 11470 |
. . . . . . 7
โข (๐ โ (๐ด โ ๐ถ) โ โ) |
41 | 3, 28 | subcld 11470 |
. . . . . . 7
โข (๐ โ (๐ท โ ๐ถ) โ โ) |
42 | 1 | sigarim 44993 |
. . . . . . 7
โข (((๐ด โ ๐ถ) โ โ โง (๐ท โ ๐ถ) โ โ) โ ((๐ด โ ๐ถ)๐บ(๐ท โ ๐ถ)) โ โ) |
43 | 40, 41, 42 | syl2anc 584 |
. . . . . 6
โข (๐ โ ((๐ด โ ๐ถ)๐บ(๐ท โ ๐ถ)) โ โ) |
44 | 43 | recnd 11141 |
. . . . 5
โข (๐ โ ((๐ด โ ๐ถ)๐บ(๐ท โ ๐ถ)) โ โ) |
45 | 8, 28 | subcld 11470 |
. . . . . . 7
โข (๐ โ (๐ โ ๐ถ) โ โ) |
46 | 45, 41 | jca 512 |
. . . . . 6
โข (๐ โ ((๐ โ ๐ถ) โ โ โง (๐ท โ ๐ถ) โ โ)) |
47 | 1, 46 | sigarimcd 45004 |
. . . . 5
โข (๐ โ ((๐ โ ๐ถ)๐บ(๐ท โ ๐ถ)) โ โ) |
48 | 6, 3 | subcld 11470 |
. . . . 5
โข (๐ โ (๐ต โ ๐ท) โ โ) |
49 | 44, 47, 48 | subdird 11570 |
. . . 4
โข (๐ โ ((((๐ด โ ๐ถ)๐บ(๐ท โ ๐ถ)) โ ((๐ โ ๐ถ)๐บ(๐ท โ ๐ถ))) ยท (๐ต โ ๐ท)) = ((((๐ด โ ๐ถ)๐บ(๐ท โ ๐ถ)) ยท (๐ต โ ๐ท)) โ (((๐ โ ๐ถ)๐บ(๐ท โ ๐ถ)) ยท (๐ต โ ๐ท)))) |
50 | 3, 5, 28 | 3jca 1128 |
. . . . . . 7
โข (๐ โ (๐ท โ โ โง ๐ด โ โ โง ๐ถ โ โ)) |
51 | 1, 50, 15 | sigaradd 45008 |
. . . . . 6
โข (๐ โ (((๐ด โ ๐ถ)๐บ(๐ท โ ๐ถ)) โ ((๐ โ ๐ถ)๐บ(๐ท โ ๐ถ))) = ((๐ด โ ๐ถ)๐บ(๐ โ ๐ถ))) |
52 | 1 | sigarperm 45002 |
. . . . . . 7
โข ((๐ถ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ((๐ถ โ ๐)๐บ(๐ด โ ๐)) = ((๐ด โ ๐ถ)๐บ(๐ โ ๐ถ))) |
53 | 28, 5, 8, 52 | syl3anc 1371 |
. . . . . 6
โข (๐ โ ((๐ถ โ ๐)๐บ(๐ด โ ๐)) = ((๐ด โ ๐ถ)๐บ(๐ โ ๐ถ))) |
54 | 51, 53 | eqtr4d 2780 |
. . . . 5
โข (๐ โ (((๐ด โ ๐ถ)๐บ(๐ท โ ๐ถ)) โ ((๐ โ ๐ถ)๐บ(๐ท โ ๐ถ))) = ((๐ถ โ ๐)๐บ(๐ด โ ๐))) |
55 | 54 | oveq1d 7366 |
. . . 4
โข (๐ โ ((((๐ด โ ๐ถ)๐บ(๐ท โ ๐ถ)) โ ((๐ โ ๐ถ)๐บ(๐ท โ ๐ถ))) ยท (๐ต โ ๐ท)) = (((๐ถ โ ๐)๐บ(๐ด โ ๐)) ยท (๐ต โ ๐ท))) |
56 | 49, 55 | eqtr3d 2779 |
. . 3
โข (๐ โ ((((๐ด โ ๐ถ)๐บ(๐ท โ ๐ถ)) ยท (๐ต โ ๐ท)) โ (((๐ โ ๐ถ)๐บ(๐ท โ ๐ถ)) ยท (๐ต โ ๐ท))) = (((๐ถ โ ๐)๐บ(๐ด โ ๐)) ยท (๐ต โ ๐ท))) |
57 | 31, 39, 56 | 3eqtrrd 2782 |
. 2
โข (๐ โ (((๐ถ โ ๐)๐บ(๐ด โ ๐)) ยท (๐ต โ ๐ท)) = (((๐ต โ ๐)๐บ(๐ด โ ๐)) ยท (๐ถ โ ๐ท))) |
58 | 6, 8 | subcld 11470 |
. . . 4
โข (๐ โ (๐ต โ ๐) โ โ) |
59 | 1 | sigarac 44994 |
. . . 4
โข (((๐ต โ ๐) โ โ โง (๐ด โ ๐) โ โ) โ ((๐ต โ ๐)๐บ(๐ด โ ๐)) = -((๐ด โ ๐)๐บ(๐ต โ ๐))) |
60 | 58, 9, 59 | syl2anc 584 |
. . 3
โข (๐ โ ((๐ต โ ๐)๐บ(๐ด โ ๐)) = -((๐ด โ ๐)๐บ(๐ต โ ๐))) |
61 | 60 | oveq1d 7366 |
. 2
โข (๐ โ (((๐ต โ ๐)๐บ(๐ด โ ๐)) ยท (๐ถ โ ๐ท)) = (-((๐ด โ ๐)๐บ(๐ต โ ๐)) ยท (๐ถ โ ๐ท))) |
62 | 9, 58 | jca 512 |
. . . . 5
โข (๐ โ ((๐ด โ ๐) โ โ โง (๐ต โ ๐) โ โ)) |
63 | 1, 62 | sigarimcd 45004 |
. . . 4
โข (๐ โ ((๐ด โ ๐)๐บ(๐ต โ ๐)) โ โ) |
64 | | mulneg12 11551 |
. . . 4
โข ((((๐ด โ ๐)๐บ(๐ต โ ๐)) โ โ โง (๐ถ โ ๐ท) โ โ) โ (-((๐ด โ ๐)๐บ(๐ต โ ๐)) ยท (๐ถ โ ๐ท)) = (((๐ด โ ๐)๐บ(๐ต โ ๐)) ยท -(๐ถ โ ๐ท))) |
65 | 63, 29, 64 | syl2anc 584 |
. . 3
โข (๐ โ (-((๐ด โ ๐)๐บ(๐ต โ ๐)) ยท (๐ถ โ ๐ท)) = (((๐ด โ ๐)๐บ(๐ต โ ๐)) ยท -(๐ถ โ ๐ท))) |
66 | 28, 3 | negsubdi2d 11486 |
. . . 4
โข (๐ โ -(๐ถ โ ๐ท) = (๐ท โ ๐ถ)) |
67 | 66 | oveq2d 7367 |
. . 3
โข (๐ โ (((๐ด โ ๐)๐บ(๐ต โ ๐)) ยท -(๐ถ โ ๐ท)) = (((๐ด โ ๐)๐บ(๐ต โ ๐)) ยท (๐ท โ ๐ถ))) |
68 | 65, 67 | eqtrd 2777 |
. 2
โข (๐ โ (-((๐ด โ ๐)๐บ(๐ต โ ๐)) ยท (๐ถ โ ๐ท)) = (((๐ด โ ๐)๐บ(๐ต โ ๐)) ยท (๐ท โ ๐ถ))) |
69 | 57, 61, 68 | 3eqtrd 2781 |
1
โข (๐ โ (((๐ถ โ ๐)๐บ(๐ด โ ๐)) ยท (๐ต โ ๐ท)) = (((๐ด โ ๐)๐บ(๐ต โ ๐)) ยท (๐ท โ ๐ถ))) |