Step | Hyp | Ref
| Expression |
1 | | simp1 1136 |
. . . 4
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ ๐ด โ (๐ผโ๐)) |
2 | | simpl 483 |
. . . 4
โข ((๐ โ (1...๐) โง ๐ โ (1...๐)) โ ๐ โ (1...๐)) |
3 | | fveecn 28149 |
. . . 4
โข ((๐ด โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ดโ๐) โ โ) |
4 | 1, 2, 3 | syl2an 596 |
. . 3
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (1...๐) โง ๐ โ (1...๐))) โ (๐ดโ๐) โ โ) |
5 | | simp2 1137 |
. . . 4
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ ๐ต โ (๐ผโ๐)) |
6 | | fveecn 28149 |
. . . 4
โข ((๐ต โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ตโ๐) โ โ) |
7 | 5, 2, 6 | syl2an 596 |
. . 3
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (1...๐) โง ๐ โ (1...๐))) โ (๐ตโ๐) โ โ) |
8 | | simp3 1138 |
. . . 4
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ ๐ถ โ (๐ผโ๐)) |
9 | | fveecn 28149 |
. . . 4
โข ((๐ถ โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ถโ๐) โ โ) |
10 | 8, 2, 9 | syl2an 596 |
. . 3
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (1...๐) โง ๐ โ (1...๐))) โ (๐ถโ๐) โ โ) |
11 | | simpr 485 |
. . . 4
โข ((๐ โ (1...๐) โง ๐ โ (1...๐)) โ ๐ โ (1...๐)) |
12 | | fveecn 28149 |
. . . 4
โข ((๐ด โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ดโ๐) โ โ) |
13 | 1, 11, 12 | syl2an 596 |
. . 3
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (1...๐) โง ๐ โ (1...๐))) โ (๐ดโ๐) โ โ) |
14 | | fveecn 28149 |
. . . 4
โข ((๐ต โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ตโ๐) โ โ) |
15 | 5, 11, 14 | syl2an 596 |
. . 3
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (1...๐) โง ๐ โ (1...๐))) โ (๐ตโ๐) โ โ) |
16 | | fveecn 28149 |
. . . 4
โข ((๐ถ โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ถโ๐) โ โ) |
17 | 8, 11, 16 | syl2an 596 |
. . 3
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (1...๐) โง ๐ โ (1...๐))) โ (๐ถโ๐) โ โ) |
18 | | simp1 1136 |
. . . . . . . . . . . 12
โข (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โ (๐ดโ๐) โ โ) |
19 | | simp3 1138 |
. . . . . . . . . . . 12
โข (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โ (๐ถโ๐) โ โ) |
20 | | mulcl 11190 |
. . . . . . . . . . . 12
โข (((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โ ((๐ดโ๐) ยท (๐ถโ๐)) โ โ) |
21 | 18, 19, 20 | syl2an 596 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((๐ดโ๐) ยท (๐ถโ๐)) โ โ) |
22 | | simp2 1137 |
. . . . . . . . . . . 12
โข (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โ (๐ตโ๐) โ โ) |
23 | | simp1 1136 |
. . . . . . . . . . . 12
โข (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โ (๐ดโ๐) โ โ) |
24 | | mulcl 11190 |
. . . . . . . . . . . 12
โข (((๐ตโ๐) โ โ โง (๐ดโ๐) โ โ) โ ((๐ตโ๐) ยท (๐ดโ๐)) โ โ) |
25 | 22, 23, 24 | syl2an 596 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((๐ตโ๐) ยท (๐ดโ๐)) โ โ) |
26 | 21, 25 | addcld 11229 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ โ) |
27 | | mulcl 11190 |
. . . . . . . . . . 11
โข (((๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โ ((๐ตโ๐) ยท (๐ถโ๐)) โ โ) |
28 | 22, 19, 27 | syl2an 596 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((๐ตโ๐) ยท (๐ถโ๐)) โ โ) |
29 | 26, 28 | subcld 11567 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ ((๐ตโ๐) ยท (๐ถโ๐))) โ โ) |
30 | | simp2 1137 |
. . . . . . . . . 10
โข (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โ (๐ตโ๐) โ โ) |
31 | | mulcl 11190 |
. . . . . . . . . 10
โข (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ) โ ((๐ดโ๐) ยท (๐ตโ๐)) โ โ) |
32 | 18, 30, 31 | syl2an 596 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((๐ดโ๐) ยท (๐ตโ๐)) โ โ) |
33 | | simp3 1138 |
. . . . . . . . . . 11
โข (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โ (๐ถโ๐) โ โ) |
34 | | mulcl 11190 |
. . . . . . . . . . 11
โข (((๐ถโ๐) โ โ โง (๐ดโ๐) โ โ) โ ((๐ถโ๐) ยท (๐ดโ๐)) โ โ) |
35 | 33, 23, 34 | syl2an 596 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((๐ถโ๐) ยท (๐ดโ๐)) โ โ) |
36 | | mulcl 11190 |
. . . . . . . . . . 11
โข (((๐ถโ๐) โ โ โง (๐ตโ๐) โ โ) โ ((๐ถโ๐) ยท (๐ตโ๐)) โ โ) |
37 | 33, 30, 36 | syl2an 596 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((๐ถโ๐) ยท (๐ตโ๐)) โ โ) |
38 | 35, 37 | subcld 11567 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))) โ โ) |
39 | 29, 32, 38 | subadd2d 11586 |
. . . . . . . 8
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ ((๐ตโ๐) ยท (๐ถโ๐))) โ ((๐ดโ๐) ยท (๐ตโ๐))) = (((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))) โ ((((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))) + ((๐ดโ๐) ยท (๐ตโ๐))) = ((((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ ((๐ตโ๐) ยท (๐ถโ๐))))) |
40 | | eqcom 2739 |
. . . . . . . 8
โข
(((((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))) + ((๐ดโ๐) ยท (๐ตโ๐))) = ((((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ ((๐ตโ๐) ยท (๐ถโ๐))) โ ((((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ ((๐ตโ๐) ยท (๐ถโ๐))) = ((((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))) + ((๐ดโ๐) ยท (๐ตโ๐)))) |
41 | 39, 40 | bitrdi 286 |
. . . . . . 7
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ ((๐ตโ๐) ยท (๐ถโ๐))) โ ((๐ดโ๐) ยท (๐ตโ๐))) = (((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))) โ ((((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ ((๐ตโ๐) ยท (๐ถโ๐))) = ((((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))) + ((๐ดโ๐) ยท (๐ตโ๐))))) |
42 | 35, 32, 37 | addsubd 11588 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((๐ถโ๐) ยท (๐ดโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐))) โ ((๐ถโ๐) ยท (๐ตโ๐))) = ((((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))) + ((๐ดโ๐) ยท (๐ตโ๐)))) |
43 | 35, 32 | addcomd 11412 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((๐ถโ๐) ยท (๐ดโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐))) = (((๐ดโ๐) ยท (๐ตโ๐)) + ((๐ถโ๐) ยท (๐ดโ๐)))) |
44 | 43 | oveq1d 7420 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((๐ถโ๐) ยท (๐ดโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐))) โ ((๐ถโ๐) ยท (๐ตโ๐))) = ((((๐ดโ๐) ยท (๐ตโ๐)) + ((๐ถโ๐) ยท (๐ดโ๐))) โ ((๐ถโ๐) ยท (๐ตโ๐)))) |
45 | 42, 44 | eqtr3d 2774 |
. . . . . . . 8
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))) + ((๐ดโ๐) ยท (๐ตโ๐))) = ((((๐ดโ๐) ยท (๐ตโ๐)) + ((๐ถโ๐) ยท (๐ดโ๐))) โ ((๐ถโ๐) ยท (๐ตโ๐)))) |
46 | 45 | eqeq2d 2743 |
. . . . . . 7
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ ((๐ตโ๐) ยท (๐ถโ๐))) = ((((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))) + ((๐ดโ๐) ยท (๐ตโ๐))) โ ((((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ ((๐ตโ๐) ยท (๐ถโ๐))) = ((((๐ดโ๐) ยท (๐ตโ๐)) + ((๐ถโ๐) ยท (๐ดโ๐))) โ ((๐ถโ๐) ยท (๐ตโ๐))))) |
47 | 41, 46 | bitrd 278 |
. . . . . 6
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ ((๐ตโ๐) ยท (๐ถโ๐))) โ ((๐ดโ๐) ยท (๐ตโ๐))) = (((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))) โ ((((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ ((๐ตโ๐) ยท (๐ถโ๐))) = ((((๐ดโ๐) ยท (๐ตโ๐)) + ((๐ถโ๐) ยท (๐ดโ๐))) โ ((๐ถโ๐) ยท (๐ตโ๐))))) |
48 | 26, 28, 32 | subsub4d 11598 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ ((๐ตโ๐) ยท (๐ถโ๐))) โ ((๐ดโ๐) ยท (๐ตโ๐))) = ((((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐))))) |
49 | 28, 32 | addcld 11229 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐))) โ โ) |
50 | 21, 49, 25 | subsub3d 11597 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((๐ดโ๐) ยท (๐ถโ๐)) โ ((((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐))) โ ((๐ตโ๐) ยท (๐ดโ๐)))) = ((((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐))))) |
51 | 28, 25, 32 | subsub3d 11597 |
. . . . . . . . . . . 12
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((๐ตโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ดโ๐)) โ ((๐ดโ๐) ยท (๐ตโ๐)))) = ((((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐))) โ ((๐ตโ๐) ยท (๐ดโ๐)))) |
52 | 51 | eqcomd 2738 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐))) โ ((๐ตโ๐) ยท (๐ดโ๐))) = (((๐ตโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ดโ๐)) โ ((๐ดโ๐) ยท (๐ตโ๐))))) |
53 | 52 | oveq2d 7421 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((๐ดโ๐) ยท (๐ถโ๐)) โ ((((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐))) โ ((๐ตโ๐) ยท (๐ดโ๐)))) = (((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ดโ๐)) โ ((๐ดโ๐) ยท (๐ตโ๐)))))) |
54 | 25, 32 | subcld 11567 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((๐ตโ๐) ยท (๐ดโ๐)) โ ((๐ดโ๐) ยท (๐ตโ๐))) โ โ) |
55 | 21, 28, 54 | subsubd 11595 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ดโ๐)) โ ((๐ดโ๐) ยท (๐ตโ๐))))) = ((((๐ดโ๐) ยท (๐ถโ๐)) โ ((๐ตโ๐) ยท (๐ถโ๐))) + (((๐ตโ๐) ยท (๐ดโ๐)) โ ((๐ดโ๐) ยท (๐ตโ๐))))) |
56 | 53, 55 | eqtrd 2772 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((๐ดโ๐) ยท (๐ถโ๐)) โ ((((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐))) โ ((๐ตโ๐) ยท (๐ดโ๐)))) = ((((๐ดโ๐) ยท (๐ถโ๐)) โ ((๐ตโ๐) ยท (๐ถโ๐))) + (((๐ตโ๐) ยท (๐ดโ๐)) โ ((๐ดโ๐) ยท (๐ตโ๐))))) |
57 | 48, 50, 56 | 3eqtr2d 2778 |
. . . . . . . 8
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ ((๐ตโ๐) ยท (๐ถโ๐))) โ ((๐ดโ๐) ยท (๐ตโ๐))) = ((((๐ดโ๐) ยท (๐ถโ๐)) โ ((๐ตโ๐) ยท (๐ถโ๐))) + (((๐ตโ๐) ยท (๐ดโ๐)) โ ((๐ดโ๐) ยท (๐ตโ๐))))) |
58 | 21, 28 | subcld 11567 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((๐ดโ๐) ยท (๐ถโ๐)) โ ((๐ตโ๐) ยท (๐ถโ๐))) โ โ) |
59 | 58, 25, 32 | addsub12d 11590 |
. . . . . . . 8
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((๐ดโ๐) ยท (๐ถโ๐)) โ ((๐ตโ๐) ยท (๐ถโ๐))) + (((๐ตโ๐) ยท (๐ดโ๐)) โ ((๐ดโ๐) ยท (๐ตโ๐)))) = (((๐ตโ๐) ยท (๐ดโ๐)) + ((((๐ดโ๐) ยท (๐ถโ๐)) โ ((๐ตโ๐) ยท (๐ถโ๐))) โ ((๐ดโ๐) ยท (๐ตโ๐))))) |
60 | 21, 28, 32 | subsub4d 11598 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((๐ดโ๐) ยท (๐ถโ๐)) โ ((๐ตโ๐) ยท (๐ถโ๐))) โ ((๐ดโ๐) ยท (๐ตโ๐))) = (((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐))))) |
61 | 60 | oveq2d 7421 |
. . . . . . . 8
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((๐ตโ๐) ยท (๐ดโ๐)) + ((((๐ดโ๐) ยท (๐ถโ๐)) โ ((๐ตโ๐) ยท (๐ถโ๐))) โ ((๐ดโ๐) ยท (๐ตโ๐)))) = (((๐ตโ๐) ยท (๐ดโ๐)) + (((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐)))))) |
62 | 57, 59, 61 | 3eqtrd 2776 |
. . . . . . 7
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ ((๐ตโ๐) ยท (๐ถโ๐))) โ ((๐ดโ๐) ยท (๐ตโ๐))) = (((๐ตโ๐) ยท (๐ดโ๐)) + (((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐)))))) |
63 | 62 | eqeq1d 2734 |
. . . . . 6
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ ((๐ตโ๐) ยท (๐ถโ๐))) โ ((๐ดโ๐) ยท (๐ตโ๐))) = (((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))) โ (((๐ตโ๐) ยท (๐ดโ๐)) + (((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐))))) = (((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))))) |
64 | 32, 35 | addcld 11229 |
. . . . . . 7
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((๐ดโ๐) ยท (๐ตโ๐)) + ((๐ถโ๐) ยท (๐ดโ๐))) โ โ) |
65 | | subeqrev 11632 |
. . . . . . 7
โข
((((((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ โ โง ((๐ตโ๐) ยท (๐ถโ๐)) โ โ) โง ((((๐ดโ๐) ยท (๐ตโ๐)) + ((๐ถโ๐) ยท (๐ดโ๐))) โ โ โง ((๐ถโ๐) ยท (๐ตโ๐)) โ โ)) โ (((((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ ((๐ตโ๐) ยท (๐ถโ๐))) = ((((๐ดโ๐) ยท (๐ตโ๐)) + ((๐ถโ๐) ยท (๐ดโ๐))) โ ((๐ถโ๐) ยท (๐ตโ๐))) โ (((๐ตโ๐) ยท (๐ถโ๐)) โ (((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐)))) = (((๐ถโ๐) ยท (๐ตโ๐)) โ (((๐ดโ๐) ยท (๐ตโ๐)) + ((๐ถโ๐) ยท (๐ดโ๐)))))) |
66 | 26, 28, 64, 37, 65 | syl22anc 837 |
. . . . . 6
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐))) โ ((๐ตโ๐) ยท (๐ถโ๐))) = ((((๐ดโ๐) ยท (๐ตโ๐)) + ((๐ถโ๐) ยท (๐ดโ๐))) โ ((๐ถโ๐) ยท (๐ตโ๐))) โ (((๐ตโ๐) ยท (๐ถโ๐)) โ (((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐)))) = (((๐ถโ๐) ยท (๐ตโ๐)) โ (((๐ดโ๐) ยท (๐ตโ๐)) + ((๐ถโ๐) ยท (๐ดโ๐)))))) |
67 | 47, 63, 66 | 3bitr3rd 309 |
. . . . 5
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((๐ตโ๐) ยท (๐ถโ๐)) โ (((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐)))) = (((๐ถโ๐) ยท (๐ตโ๐)) โ (((๐ดโ๐) ยท (๐ตโ๐)) + ((๐ถโ๐) ยท (๐ดโ๐)))) โ (((๐ตโ๐) ยท (๐ดโ๐)) + (((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐))))) = (((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))))) |
68 | 21, 49 | subcld 11567 |
. . . . . . . 8
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐)))) โ โ) |
69 | 25, 68, 38 | addrsub 11627 |
. . . . . . 7
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((๐ตโ๐) ยท (๐ดโ๐)) + (((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐))))) = (((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))) โ (((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐)))) = ((((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))) โ ((๐ตโ๐) ยท (๐ดโ๐))))) |
70 | 35, 37, 25 | sub32d 11599 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))) โ ((๐ตโ๐) ยท (๐ดโ๐))) = ((((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ตโ๐) ยท (๐ดโ๐))) โ ((๐ถโ๐) ยท (๐ตโ๐)))) |
71 | 35, 25, 37 | subsub4d 11598 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ตโ๐) ยท (๐ดโ๐))) โ ((๐ถโ๐) ยท (๐ตโ๐))) = (((๐ถโ๐) ยท (๐ดโ๐)) โ (((๐ตโ๐) ยท (๐ดโ๐)) + ((๐ถโ๐) ยท (๐ตโ๐))))) |
72 | 70, 71 | eqtrd 2772 |
. . . . . . . 8
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))) โ ((๐ตโ๐) ยท (๐ดโ๐))) = (((๐ถโ๐) ยท (๐ดโ๐)) โ (((๐ตโ๐) ยท (๐ดโ๐)) + ((๐ถโ๐) ยท (๐ตโ๐))))) |
73 | 72 | eqeq2d 2743 |
. . . . . . 7
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐)))) = ((((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))) โ ((๐ตโ๐) ยท (๐ดโ๐))) โ (((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐)))) = (((๐ถโ๐) ยท (๐ดโ๐)) โ (((๐ตโ๐) ยท (๐ดโ๐)) + ((๐ถโ๐) ยท (๐ตโ๐)))))) |
74 | 69, 73 | bitrd 278 |
. . . . . 6
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((๐ตโ๐) ยท (๐ดโ๐)) + (((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐))))) = (((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))) โ (((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐)))) = (((๐ถโ๐) ยท (๐ดโ๐)) โ (((๐ตโ๐) ยท (๐ดโ๐)) + ((๐ถโ๐) ยท (๐ตโ๐)))))) |
75 | | eqcom 2739 |
. . . . . 6
โข ((((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐)))) = (((๐ถโ๐) ยท (๐ดโ๐)) โ (((๐ตโ๐) ยท (๐ดโ๐)) + ((๐ถโ๐) ยท (๐ตโ๐)))) โ (((๐ถโ๐) ยท (๐ดโ๐)) โ (((๐ตโ๐) ยท (๐ดโ๐)) + ((๐ถโ๐) ยท (๐ตโ๐)))) = (((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐))))) |
76 | 74, 75 | bitrdi 286 |
. . . . 5
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((๐ตโ๐) ยท (๐ดโ๐)) + (((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐))))) = (((๐ถโ๐) ยท (๐ดโ๐)) โ ((๐ถโ๐) ยท (๐ตโ๐))) โ (((๐ถโ๐) ยท (๐ดโ๐)) โ (((๐ตโ๐) ยท (๐ดโ๐)) + ((๐ถโ๐) ยท (๐ตโ๐)))) = (((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐)))))) |
77 | 67, 76 | bitrd 278 |
. . . 4
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((๐ตโ๐) ยท (๐ถโ๐)) โ (((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐)))) = (((๐ถโ๐) ยท (๐ตโ๐)) โ (((๐ดโ๐) ยท (๐ตโ๐)) + ((๐ถโ๐) ยท (๐ดโ๐)))) โ (((๐ถโ๐) ยท (๐ดโ๐)) โ (((๐ตโ๐) ยท (๐ดโ๐)) + ((๐ถโ๐) ยท (๐ตโ๐)))) = (((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐)))))) |
78 | | colinearalglem1 28153 |
. . . 4
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (((๐ตโ๐) ยท (๐ถโ๐)) โ (((๐ดโ๐) ยท (๐ถโ๐)) + ((๐ตโ๐) ยท (๐ดโ๐)))) = (((๐ถโ๐) ยท (๐ตโ๐)) โ (((๐ดโ๐) ยท (๐ตโ๐)) + ((๐ถโ๐) ยท (๐ดโ๐)))))) |
79 | | 3anrot 1100 |
. . . . 5
โข (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โ ((๐ตโ๐) โ โ โง (๐ถโ๐) โ โ โง (๐ดโ๐) โ โ)) |
80 | | 3anrot 1100 |
. . . . 5
โข (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โ ((๐ตโ๐) โ โ โง (๐ถโ๐) โ โ โง (๐ดโ๐) โ โ)) |
81 | | colinearalglem1 28153 |
. . . . 5
โข ((((๐ตโ๐) โ โ โง (๐ถโ๐) โ โ โง (๐ดโ๐) โ โ) โง ((๐ตโ๐) โ โ โง (๐ถโ๐) โ โ โง (๐ดโ๐) โ โ)) โ ((((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) = (((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โ (((๐ถโ๐) ยท (๐ดโ๐)) โ (((๐ตโ๐) ยท (๐ดโ๐)) + ((๐ถโ๐) ยท (๐ตโ๐)))) = (((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐)))))) |
82 | 79, 80, 81 | syl2anb 598 |
. . . 4
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) = (((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โ (((๐ถโ๐) ยท (๐ดโ๐)) โ (((๐ตโ๐) ยท (๐ดโ๐)) + ((๐ถโ๐) ยท (๐ตโ๐)))) = (((๐ดโ๐) ยท (๐ถโ๐)) โ (((๐ตโ๐) ยท (๐ถโ๐)) + ((๐ดโ๐) ยท (๐ตโ๐)))))) |
83 | 77, 78, 82 | 3bitr4d 310 |
. . 3
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ ((((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) = (((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))))) |
84 | 4, 7, 10, 13, 15, 17, 83 | syl33anc 1385 |
. 2
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (1...๐) โง ๐ โ (1...๐))) โ ((((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) = (((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))))) |
85 | 84 | 2ralbidva 3216 |
1
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) = (((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))))) |