Step | Hyp | Ref
| Expression |
1 | | madjusmdet.b |
. . 3
โข ๐ต = (Baseโ๐ด) |
2 | | madjusmdet.a |
. . 3
โข ๐ด = ((1...๐) Mat ๐
) |
3 | | madjusmdet.d |
. . 3
โข ๐ท = ((1...๐) maDet ๐
) |
4 | | madjusmdet.k |
. . 3
โข ๐พ = ((1...๐) maAdju ๐
) |
5 | | madjusmdet.t |
. . 3
โข ยท =
(.rโ๐
) |
6 | | madjusmdet.z |
. . 3
โข ๐ = (โคRHomโ๐
) |
7 | | madjusmdet.e |
. . 3
โข ๐ธ = ((1...(๐ โ 1)) maDet ๐
) |
8 | | madjusmdet.n |
. . 3
โข (๐ โ ๐ โ โ) |
9 | | madjusmdet.r |
. . 3
โข (๐ โ ๐
โ CRing) |
10 | | madjusmdet.i |
. . 3
โข (๐ โ ๐ผ โ (1...๐)) |
11 | | madjusmdet.j |
. . 3
โข (๐ โ ๐ฝ โ (1...๐)) |
12 | | madjusmdet.m |
. . 3
โข (๐ โ ๐ โ ๐ต) |
13 | | eqid 2737 |
. . 3
โข
(Baseโ(SymGrpโ(1...๐))) = (Baseโ(SymGrpโ(1...๐))) |
14 | | eqid 2737 |
. . 3
โข
(pmSgnโ(1...๐)) = (pmSgnโ(1...๐)) |
15 | | eqid 2737 |
. . 3
โข (๐ผ(((1...๐) minMatR1 ๐
)โ๐)๐ฝ) = (๐ผ(((1...๐) minMatR1 ๐
)โ๐)๐ฝ) |
16 | | fveq2 6847 |
. . . . 5
โข (๐ = ๐ โ ((๐ โ โก๐)โ๐) = ((๐ โ โก๐)โ๐)) |
17 | 16 | oveq1d 7377 |
. . . 4
โข (๐ = ๐ โ (((๐ โ โก๐)โ๐)(๐ผ(((1...๐) minMatR1 ๐
)โ๐)๐ฝ)((๐ โ โก๐)โ๐)) = (((๐ โ โก๐)โ๐)(๐ผ(((1...๐) minMatR1 ๐
)โ๐)๐ฝ)((๐ โ โก๐)โ๐))) |
18 | | fveq2 6847 |
. . . . 5
โข (๐ = ๐ โ ((๐ โ โก๐)โ๐) = ((๐ โ โก๐)โ๐)) |
19 | 18 | oveq2d 7378 |
. . . 4
โข (๐ = ๐ โ (((๐ โ โก๐)โ๐)(๐ผ(((1...๐) minMatR1 ๐
)โ๐)๐ฝ)((๐ โ โก๐)โ๐)) = (((๐ โ โก๐)โ๐)(๐ผ(((1...๐) minMatR1 ๐
)โ๐)๐ฝ)((๐ โ โก๐)โ๐))) |
20 | 17, 19 | cbvmpov 7457 |
. . 3
โข (๐ โ (1...๐), ๐ โ (1...๐) โฆ (((๐ โ โก๐)โ๐)(๐ผ(((1...๐) minMatR1 ๐
)โ๐)๐ฝ)((๐ โ โก๐)โ๐))) = (๐ โ (1...๐), ๐ โ (1...๐) โฆ (((๐ โ โก๐)โ๐)(๐ผ(((1...๐) minMatR1 ๐
)โ๐)๐ฝ)((๐ โ โก๐)โ๐))) |
21 | | eqid 2737 |
. . . . . 6
โข
(1...๐) = (1...๐) |
22 | | madjusmdetlem2.p |
. . . . . 6
โข ๐ = (๐ โ (1...๐) โฆ if(๐ = 1, ๐ผ, if(๐ โค ๐ผ, (๐ โ 1), ๐))) |
23 | | eqid 2737 |
. . . . . 6
โข
(SymGrpโ(1...๐)) = (SymGrpโ(1...๐)) |
24 | 21, 22, 23, 13 | fzto1st 31994 |
. . . . 5
โข (๐ผ โ (1...๐) โ ๐ โ (Baseโ(SymGrpโ(1...๐)))) |
25 | 10, 24 | syl 17 |
. . . 4
โข (๐ โ ๐ โ (Baseโ(SymGrpโ(1...๐)))) |
26 | | nnuz 12813 |
. . . . . . . . 9
โข โ =
(โคโฅโ1) |
27 | 8, 26 | eleqtrdi 2848 |
. . . . . . . 8
โข (๐ โ ๐ โ
(โคโฅโ1)) |
28 | | eluzfz2 13456 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ1) โ ๐ โ (1...๐)) |
29 | 27, 28 | syl 17 |
. . . . . . 7
โข (๐ โ ๐ โ (1...๐)) |
30 | | madjusmdetlem2.s |
. . . . . . . 8
โข ๐ = (๐ โ (1...๐) โฆ if(๐ = 1, ๐, if(๐ โค ๐, (๐ โ 1), ๐))) |
31 | 21, 30, 23, 13 | fzto1st 31994 |
. . . . . . 7
โข (๐ โ (1...๐) โ ๐ โ (Baseโ(SymGrpโ(1...๐)))) |
32 | 29, 31 | syl 17 |
. . . . . 6
โข (๐ โ ๐ โ (Baseโ(SymGrpโ(1...๐)))) |
33 | | eqid 2737 |
. . . . . . 7
โข
(invgโ(SymGrpโ(1...๐))) =
(invgโ(SymGrpโ(1...๐))) |
34 | 23, 13, 33 | symginv 19191 |
. . . . . 6
โข (๐ โ
(Baseโ(SymGrpโ(1...๐))) โ
((invgโ(SymGrpโ(1...๐)))โ๐) = โก๐) |
35 | 32, 34 | syl 17 |
. . . . 5
โข (๐ โ
((invgโ(SymGrpโ(1...๐)))โ๐) = โก๐) |
36 | | fzfid 13885 |
. . . . . . 7
โข (๐ โ (1...๐) โ Fin) |
37 | 23 | symggrp 19189 |
. . . . . . 7
โข
((1...๐) โ Fin
โ (SymGrpโ(1...๐)) โ Grp) |
38 | 36, 37 | syl 17 |
. . . . . 6
โข (๐ โ (SymGrpโ(1...๐)) โ Grp) |
39 | 13, 33 | grpinvcl 18805 |
. . . . . 6
โข
(((SymGrpโ(1...๐)) โ Grp โง ๐ โ (Baseโ(SymGrpโ(1...๐)))) โ
((invgโ(SymGrpโ(1...๐)))โ๐) โ
(Baseโ(SymGrpโ(1...๐)))) |
40 | 38, 32, 39 | syl2anc 585 |
. . . . 5
โข (๐ โ
((invgโ(SymGrpโ(1...๐)))โ๐) โ
(Baseโ(SymGrpโ(1...๐)))) |
41 | 35, 40 | eqeltrrd 2839 |
. . . 4
โข (๐ โ โก๐ โ (Baseโ(SymGrpโ(1...๐)))) |
42 | | eqid 2737 |
. . . . . 6
โข
(+gโ(SymGrpโ(1...๐))) =
(+gโ(SymGrpโ(1...๐))) |
43 | 23, 13, 42 | symgov 19172 |
. . . . 5
โข ((๐ โ
(Baseโ(SymGrpโ(1...๐))) โง โก๐ โ (Baseโ(SymGrpโ(1...๐)))) โ (๐(+gโ(SymGrpโ(1...๐)))โก๐) = (๐ โ โก๐)) |
44 | 23, 13, 42 | symgcl 19173 |
. . . . 5
โข ((๐ โ
(Baseโ(SymGrpโ(1...๐))) โง โก๐ โ (Baseโ(SymGrpโ(1...๐)))) โ (๐(+gโ(SymGrpโ(1...๐)))โก๐) โ (Baseโ(SymGrpโ(1...๐)))) |
45 | 43, 44 | eqeltrrd 2839 |
. . . 4
โข ((๐ โ
(Baseโ(SymGrpโ(1...๐))) โง โก๐ โ (Baseโ(SymGrpโ(1...๐)))) โ (๐ โ โก๐) โ
(Baseโ(SymGrpโ(1...๐)))) |
46 | 25, 41, 45 | syl2anc 585 |
. . 3
โข (๐ โ (๐ โ โก๐) โ
(Baseโ(SymGrpโ(1...๐)))) |
47 | | madjusmdetlem4.q |
. . . . . 6
โข ๐ = (๐ โ (1...๐) โฆ if(๐ = 1, ๐ฝ, if(๐ โค ๐ฝ, (๐ โ 1), ๐))) |
48 | 21, 47, 23, 13 | fzto1st 31994 |
. . . . 5
โข (๐ฝ โ (1...๐) โ ๐ โ (Baseโ(SymGrpโ(1...๐)))) |
49 | 11, 48 | syl 17 |
. . . 4
โข (๐ โ ๐ โ (Baseโ(SymGrpโ(1...๐)))) |
50 | | madjusmdetlem4.t |
. . . . . . . 8
โข ๐ = (๐ โ (1...๐) โฆ if(๐ = 1, ๐, if(๐ โค ๐, (๐ โ 1), ๐))) |
51 | 21, 50, 23, 13 | fzto1st 31994 |
. . . . . . 7
โข (๐ โ (1...๐) โ ๐ โ (Baseโ(SymGrpโ(1...๐)))) |
52 | 29, 51 | syl 17 |
. . . . . 6
โข (๐ โ ๐ โ (Baseโ(SymGrpโ(1...๐)))) |
53 | 23, 13, 33 | symginv 19191 |
. . . . . 6
โข (๐ โ
(Baseโ(SymGrpโ(1...๐))) โ
((invgโ(SymGrpโ(1...๐)))โ๐) = โก๐) |
54 | 52, 53 | syl 17 |
. . . . 5
โข (๐ โ
((invgโ(SymGrpโ(1...๐)))โ๐) = โก๐) |
55 | 13, 33 | grpinvcl 18805 |
. . . . . 6
โข
(((SymGrpโ(1...๐)) โ Grp โง ๐ โ (Baseโ(SymGrpโ(1...๐)))) โ
((invgโ(SymGrpโ(1...๐)))โ๐) โ
(Baseโ(SymGrpโ(1...๐)))) |
56 | 38, 52, 55 | syl2anc 585 |
. . . . 5
โข (๐ โ
((invgโ(SymGrpโ(1...๐)))โ๐) โ
(Baseโ(SymGrpโ(1...๐)))) |
57 | 54, 56 | eqeltrrd 2839 |
. . . 4
โข (๐ โ โก๐ โ (Baseโ(SymGrpโ(1...๐)))) |
58 | 23, 13, 42 | symgov 19172 |
. . . . 5
โข ((๐ โ
(Baseโ(SymGrpโ(1...๐))) โง โก๐ โ (Baseโ(SymGrpโ(1...๐)))) โ (๐(+gโ(SymGrpโ(1...๐)))โก๐) = (๐ โ โก๐)) |
59 | 23, 13, 42 | symgcl 19173 |
. . . . 5
โข ((๐ โ
(Baseโ(SymGrpโ(1...๐))) โง โก๐ โ (Baseโ(SymGrpโ(1...๐)))) โ (๐(+gโ(SymGrpโ(1...๐)))โก๐) โ (Baseโ(SymGrpโ(1...๐)))) |
60 | 58, 59 | eqeltrrd 2839 |
. . . 4
โข ((๐ โ
(Baseโ(SymGrpโ(1...๐))) โง โก๐ โ (Baseโ(SymGrpโ(1...๐)))) โ (๐ โ โก๐) โ
(Baseโ(SymGrpโ(1...๐)))) |
61 | 49, 57, 60 | syl2anc 585 |
. . 3
โข (๐ โ (๐ โ โก๐) โ
(Baseโ(SymGrpโ(1...๐)))) |
62 | 23, 13 | symgbasf1o 19163 |
. . . . . . 7
โข (๐ โ
(Baseโ(SymGrpโ(1...๐))) โ ๐:(1...๐)โ1-1-ontoโ(1...๐)) |
63 | 32, 62 | syl 17 |
. . . . . 6
โข (๐ โ ๐:(1...๐)โ1-1-ontoโ(1...๐)) |
64 | | f1of1 6788 |
. . . . . 6
โข (๐:(1...๐)โ1-1-ontoโ(1...๐) โ ๐:(1...๐)โ1-1โ(1...๐)) |
65 | | df-f1 6506 |
. . . . . . 7
โข (๐:(1...๐)โ1-1โ(1...๐) โ (๐:(1...๐)โถ(1...๐) โง Fun โก๐)) |
66 | 65 | simprbi 498 |
. . . . . 6
โข (๐:(1...๐)โ1-1โ(1...๐) โ Fun โก๐) |
67 | 63, 64, 66 | 3syl 18 |
. . . . 5
โข (๐ โ Fun โก๐) |
68 | | f1ocnv 6801 |
. . . . . . 7
โข (๐:(1...๐)โ1-1-ontoโ(1...๐) โ โก๐:(1...๐)โ1-1-ontoโ(1...๐)) |
69 | | f1odm 6793 |
. . . . . . 7
โข (โก๐:(1...๐)โ1-1-ontoโ(1...๐) โ dom โก๐ = (1...๐)) |
70 | 63, 68, 69 | 3syl 18 |
. . . . . 6
โข (๐ โ dom โก๐ = (1...๐)) |
71 | 29, 70 | eleqtrrd 2841 |
. . . . 5
โข (๐ โ ๐ โ dom โก๐) |
72 | | fvco 6944 |
. . . . 5
โข ((Fun
โก๐ โง ๐ โ dom โก๐) โ ((๐ โ โก๐)โ๐) = (๐โ(โก๐โ๐))) |
73 | 67, 71, 72 | syl2anc 585 |
. . . 4
โข (๐ โ ((๐ โ โก๐)โ๐) = (๐โ(โก๐โ๐))) |
74 | 21, 30, 23, 13 | fzto1stinvn 31995 |
. . . . . 6
โข (๐ โ (1...๐) โ (โก๐โ๐) = 1) |
75 | 29, 74 | syl 17 |
. . . . 5
โข (๐ โ (โก๐โ๐) = 1) |
76 | 75 | fveq2d 6851 |
. . . 4
โข (๐ โ (๐โ(โก๐โ๐)) = (๐โ1)) |
77 | 21, 22 | fzto1stfv1 31992 |
. . . . 5
โข (๐ผ โ (1...๐) โ (๐โ1) = ๐ผ) |
78 | 10, 77 | syl 17 |
. . . 4
โข (๐ โ (๐โ1) = ๐ผ) |
79 | 73, 76, 78 | 3eqtrd 2781 |
. . 3
โข (๐ โ ((๐ โ โก๐)โ๐) = ๐ผ) |
80 | 23, 13 | symgbasf1o 19163 |
. . . . . . 7
โข (๐ โ
(Baseโ(SymGrpโ(1...๐))) โ ๐:(1...๐)โ1-1-ontoโ(1...๐)) |
81 | 52, 80 | syl 17 |
. . . . . 6
โข (๐ โ ๐:(1...๐)โ1-1-ontoโ(1...๐)) |
82 | | f1of1 6788 |
. . . . . 6
โข (๐:(1...๐)โ1-1-ontoโ(1...๐) โ ๐:(1...๐)โ1-1โ(1...๐)) |
83 | | df-f1 6506 |
. . . . . . 7
โข (๐:(1...๐)โ1-1โ(1...๐) โ (๐:(1...๐)โถ(1...๐) โง Fun โก๐)) |
84 | 83 | simprbi 498 |
. . . . . 6
โข (๐:(1...๐)โ1-1โ(1...๐) โ Fun โก๐) |
85 | 81, 82, 84 | 3syl 18 |
. . . . 5
โข (๐ โ Fun โก๐) |
86 | | f1ocnv 6801 |
. . . . . . 7
โข (๐:(1...๐)โ1-1-ontoโ(1...๐) โ โก๐:(1...๐)โ1-1-ontoโ(1...๐)) |
87 | | f1odm 6793 |
. . . . . . 7
โข (โก๐:(1...๐)โ1-1-ontoโ(1...๐) โ dom โก๐ = (1...๐)) |
88 | 81, 86, 87 | 3syl 18 |
. . . . . 6
โข (๐ โ dom โก๐ = (1...๐)) |
89 | 29, 88 | eleqtrrd 2841 |
. . . . 5
โข (๐ โ ๐ โ dom โก๐) |
90 | | fvco 6944 |
. . . . 5
โข ((Fun
โก๐ โง ๐ โ dom โก๐) โ ((๐ โ โก๐)โ๐) = (๐โ(โก๐โ๐))) |
91 | 85, 89, 90 | syl2anc 585 |
. . . 4
โข (๐ โ ((๐ โ โก๐)โ๐) = (๐โ(โก๐โ๐))) |
92 | 21, 50, 23, 13 | fzto1stinvn 31995 |
. . . . . 6
โข (๐ โ (1...๐) โ (โก๐โ๐) = 1) |
93 | 29, 92 | syl 17 |
. . . . 5
โข (๐ โ (โก๐โ๐) = 1) |
94 | 93 | fveq2d 6851 |
. . . 4
โข (๐ โ (๐โ(โก๐โ๐)) = (๐โ1)) |
95 | 21, 47 | fzto1stfv1 31992 |
. . . . 5
โข (๐ฝ โ (1...๐) โ (๐โ1) = ๐ฝ) |
96 | 11, 95 | syl 17 |
. . . 4
โข (๐ โ (๐โ1) = ๐ฝ) |
97 | 91, 94, 96 | 3eqtrd 2781 |
. . 3
โข (๐ โ ((๐ โ โก๐)โ๐) = ๐ฝ) |
98 | | crngring 19983 |
. . . . . 6
โข (๐
โ CRing โ ๐
โ Ring) |
99 | 9, 98 | syl 17 |
. . . . 5
โข (๐ โ ๐
โ Ring) |
100 | 2, 1 | minmar1cl 22016 |
. . . . 5
โข (((๐
โ Ring โง ๐ โ ๐ต) โง (๐ผ โ (1...๐) โง ๐ฝ โ (1...๐))) โ (๐ผ(((1...๐) minMatR1 ๐
)โ๐)๐ฝ) โ ๐ต) |
101 | 99, 12, 10, 11, 100 | syl22anc 838 |
. . . 4
โข (๐ โ (๐ผ(((1...๐) minMatR1 ๐
)โ๐)๐ฝ) โ ๐ต) |
102 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 22, 30, 47, 50, 20, 101 | madjusmdetlem3 32450 |
. . 3
โข (๐ โ (๐ผ(subMat1โ(๐ผ(((1...๐) minMatR1 ๐
)โ๐)๐ฝ))๐ฝ) = (๐(subMat1โ(๐ โ (1...๐), ๐ โ (1...๐) โฆ (((๐ โ โก๐)โ๐)(๐ผ(((1...๐) minMatR1 ๐
)โ๐)๐ฝ)((๐ โ โก๐)โ๐))))๐)) |
103 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 20, 46, 61, 79, 97, 102 | madjusmdetlem1 32448 |
. 2
โข (๐ โ (๐ฝ(๐พโ๐)๐ผ) = ((๐โ(((pmSgnโ(1...๐))โ(๐ โ โก๐)) ยท ((pmSgnโ(1...๐))โ(๐ โ โก๐)))) ยท (๐ธโ(๐ผ(subMat1โ๐)๐ฝ)))) |
104 | 23, 14, 13 | psgnco 21003 |
. . . . . . . 8
โข
(((1...๐) โ Fin
โง ๐ โ
(Baseโ(SymGrpโ(1...๐))) โง โก๐ โ (Baseโ(SymGrpโ(1...๐)))) โ
((pmSgnโ(1...๐))โ(๐ โ โก๐)) = (((pmSgnโ(1...๐))โ๐) ยท ((pmSgnโ(1...๐))โโก๐))) |
105 | 36, 25, 41, 104 | syl3anc 1372 |
. . . . . . 7
โข (๐ โ ((pmSgnโ(1...๐))โ(๐ โ โก๐)) = (((pmSgnโ(1...๐))โ๐) ยท ((pmSgnโ(1...๐))โโก๐))) |
106 | 21, 22, 23, 13, 14 | psgnfzto1st 31996 |
. . . . . . . . 9
โข (๐ผ โ (1...๐) โ ((pmSgnโ(1...๐))โ๐) = (-1โ(๐ผ + 1))) |
107 | 10, 106 | syl 17 |
. . . . . . . 8
โข (๐ โ ((pmSgnโ(1...๐))โ๐) = (-1โ(๐ผ + 1))) |
108 | 23, 14, 13 | psgninv 21002 |
. . . . . . . . . 10
โข
(((1...๐) โ Fin
โง ๐ โ
(Baseโ(SymGrpโ(1...๐)))) โ ((pmSgnโ(1...๐))โโก๐) = ((pmSgnโ(1...๐))โ๐)) |
109 | 36, 32, 108 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ ((pmSgnโ(1...๐))โโก๐) = ((pmSgnโ(1...๐))โ๐)) |
110 | 21, 30, 23, 13, 14 | psgnfzto1st 31996 |
. . . . . . . . . 10
โข (๐ โ (1...๐) โ ((pmSgnโ(1...๐))โ๐) = (-1โ(๐ + 1))) |
111 | 29, 110 | syl 17 |
. . . . . . . . 9
โข (๐ โ ((pmSgnโ(1...๐))โ๐) = (-1โ(๐ + 1))) |
112 | 109, 111 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ ((pmSgnโ(1...๐))โโก๐) = (-1โ(๐ + 1))) |
113 | 107, 112 | oveq12d 7380 |
. . . . . . 7
โข (๐ โ (((pmSgnโ(1...๐))โ๐) ยท ((pmSgnโ(1...๐))โโก๐)) = ((-1โ(๐ผ + 1)) ยท (-1โ(๐ + 1)))) |
114 | 105, 113 | eqtrd 2777 |
. . . . . 6
โข (๐ โ ((pmSgnโ(1...๐))โ(๐ โ โก๐)) = ((-1โ(๐ผ + 1)) ยท (-1โ(๐ + 1)))) |
115 | 23, 14, 13 | psgnco 21003 |
. . . . . . . 8
โข
(((1...๐) โ Fin
โง ๐ โ
(Baseโ(SymGrpโ(1...๐))) โง โก๐ โ (Baseโ(SymGrpโ(1...๐)))) โ
((pmSgnโ(1...๐))โ(๐ โ โก๐)) = (((pmSgnโ(1...๐))โ๐) ยท ((pmSgnโ(1...๐))โโก๐))) |
116 | 36, 49, 57, 115 | syl3anc 1372 |
. . . . . . 7
โข (๐ โ ((pmSgnโ(1...๐))โ(๐ โ โก๐)) = (((pmSgnโ(1...๐))โ๐) ยท ((pmSgnโ(1...๐))โโก๐))) |
117 | 21, 47, 23, 13, 14 | psgnfzto1st 31996 |
. . . . . . . . 9
โข (๐ฝ โ (1...๐) โ ((pmSgnโ(1...๐))โ๐) = (-1โ(๐ฝ + 1))) |
118 | 11, 117 | syl 17 |
. . . . . . . 8
โข (๐ โ ((pmSgnโ(1...๐))โ๐) = (-1โ(๐ฝ + 1))) |
119 | 23, 14, 13 | psgninv 21002 |
. . . . . . . . . 10
โข
(((1...๐) โ Fin
โง ๐ โ
(Baseโ(SymGrpโ(1...๐)))) โ ((pmSgnโ(1...๐))โโก๐) = ((pmSgnโ(1...๐))โ๐)) |
120 | 36, 52, 119 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ ((pmSgnโ(1...๐))โโก๐) = ((pmSgnโ(1...๐))โ๐)) |
121 | 21, 50, 23, 13, 14 | psgnfzto1st 31996 |
. . . . . . . . . 10
โข (๐ โ (1...๐) โ ((pmSgnโ(1...๐))โ๐) = (-1โ(๐ + 1))) |
122 | 29, 121 | syl 17 |
. . . . . . . . 9
โข (๐ โ ((pmSgnโ(1...๐))โ๐) = (-1โ(๐ + 1))) |
123 | 120, 122 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ ((pmSgnโ(1...๐))โโก๐) = (-1โ(๐ + 1))) |
124 | 118, 123 | oveq12d 7380 |
. . . . . . 7
โข (๐ โ (((pmSgnโ(1...๐))โ๐) ยท ((pmSgnโ(1...๐))โโก๐)) = ((-1โ(๐ฝ + 1)) ยท (-1โ(๐ + 1)))) |
125 | 116, 124 | eqtrd 2777 |
. . . . . 6
โข (๐ โ ((pmSgnโ(1...๐))โ(๐ โ โก๐)) = ((-1โ(๐ฝ + 1)) ยท (-1โ(๐ + 1)))) |
126 | 114, 125 | oveq12d 7380 |
. . . . 5
โข (๐ โ (((pmSgnโ(1...๐))โ(๐ โ โก๐)) ยท ((pmSgnโ(1...๐))โ(๐ โ โก๐))) = (((-1โ(๐ผ + 1)) ยท (-1โ(๐ + 1))) ยท ((-1โ(๐ฝ + 1)) ยท (-1โ(๐ + 1))))) |
127 | | 1cnd 11157 |
. . . . . . . . 9
โข (๐ โ 1 โ
โ) |
128 | 127 | negcld 11506 |
. . . . . . . 8
โข (๐ โ -1 โ
โ) |
129 | | fz1ssnn 13479 |
. . . . . . . . . . 11
โข
(1...๐) โ
โ |
130 | 129, 10 | sselid 3947 |
. . . . . . . . . 10
โข (๐ โ ๐ผ โ โ) |
131 | 130 | nnnn0d 12480 |
. . . . . . . . 9
โข (๐ โ ๐ผ โ
โ0) |
132 | | 1nn0 12436 |
. . . . . . . . . 10
โข 1 โ
โ0 |
133 | 132 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 1 โ
โ0) |
134 | 131, 133 | nn0addcld 12484 |
. . . . . . . 8
โข (๐ โ (๐ผ + 1) โ
โ0) |
135 | 128, 134 | expcld 14058 |
. . . . . . 7
โข (๐ โ (-1โ(๐ผ + 1)) โ
โ) |
136 | 8 | nnnn0d 12480 |
. . . . . . . . 9
โข (๐ โ ๐ โ
โ0) |
137 | 136, 133 | nn0addcld 12484 |
. . . . . . . 8
โข (๐ โ (๐ + 1) โ
โ0) |
138 | 128, 137 | expcld 14058 |
. . . . . . 7
โข (๐ โ (-1โ(๐ + 1)) โ
โ) |
139 | 129, 11 | sselid 3947 |
. . . . . . . . . 10
โข (๐ โ ๐ฝ โ โ) |
140 | 139 | nnnn0d 12480 |
. . . . . . . . 9
โข (๐ โ ๐ฝ โ
โ0) |
141 | 140, 133 | nn0addcld 12484 |
. . . . . . . 8
โข (๐ โ (๐ฝ + 1) โ
โ0) |
142 | 128, 141 | expcld 14058 |
. . . . . . 7
โข (๐ โ (-1โ(๐ฝ + 1)) โ
โ) |
143 | 135, 138,
142, 138 | mul4d 11374 |
. . . . . 6
โข (๐ โ (((-1โ(๐ผ + 1)) ยท (-1โ(๐ + 1))) ยท
((-1โ(๐ฝ + 1)) ยท
(-1โ(๐ + 1)))) =
(((-1โ(๐ผ + 1))
ยท (-1โ(๐ฝ + 1)))
ยท ((-1โ(๐ + 1))
ยท (-1โ(๐ +
1))))) |
144 | 128, 141,
134 | expaddd 14060 |
. . . . . . . 8
โข (๐ โ (-1โ((๐ผ + 1) + (๐ฝ + 1))) = ((-1โ(๐ผ + 1)) ยท (-1โ(๐ฝ + 1)))) |
145 | 130 | nncnd 12176 |
. . . . . . . . . . . 12
โข (๐ โ ๐ผ โ โ) |
146 | 139 | nncnd 12176 |
. . . . . . . . . . . 12
โข (๐ โ ๐ฝ โ โ) |
147 | 145, 127,
146, 127 | add4d 11390 |
. . . . . . . . . . 11
โข (๐ โ ((๐ผ + 1) + (๐ฝ + 1)) = ((๐ผ + ๐ฝ) + (1 + 1))) |
148 | | 1p1e2 12285 |
. . . . . . . . . . . 12
โข (1 + 1) =
2 |
149 | 148 | oveq2i 7373 |
. . . . . . . . . . 11
โข ((๐ผ + ๐ฝ) + (1 + 1)) = ((๐ผ + ๐ฝ) + 2) |
150 | 147, 149 | eqtrdi 2793 |
. . . . . . . . . 10
โข (๐ โ ((๐ผ + 1) + (๐ฝ + 1)) = ((๐ผ + ๐ฝ) + 2)) |
151 | 150 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ โ (-1โ((๐ผ + 1) + (๐ฝ + 1))) = (-1โ((๐ผ + ๐ฝ) + 2))) |
152 | | 2nn0 12437 |
. . . . . . . . . . . 12
โข 2 โ
โ0 |
153 | 152 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ 2 โ
โ0) |
154 | 131, 140 | nn0addcld 12484 |
. . . . . . . . . . 11
โข (๐ โ (๐ผ + ๐ฝ) โ
โ0) |
155 | 128, 153,
154 | expaddd 14060 |
. . . . . . . . . 10
โข (๐ โ (-1โ((๐ผ + ๐ฝ) + 2)) = ((-1โ(๐ผ + ๐ฝ)) ยท (-1โ2))) |
156 | | neg1sqe1 14107 |
. . . . . . . . . . 11
โข
(-1โ2) = 1 |
157 | 156 | oveq2i 7373 |
. . . . . . . . . 10
โข
((-1โ(๐ผ + ๐ฝ)) ยท (-1โ2)) =
((-1โ(๐ผ + ๐ฝ)) ยท 1) |
158 | 155, 157 | eqtrdi 2793 |
. . . . . . . . 9
โข (๐ โ (-1โ((๐ผ + ๐ฝ) + 2)) = ((-1โ(๐ผ + ๐ฝ)) ยท 1)) |
159 | 128, 154 | expcld 14058 |
. . . . . . . . . 10
โข (๐ โ (-1โ(๐ผ + ๐ฝ)) โ โ) |
160 | 159 | mulid1d 11179 |
. . . . . . . . 9
โข (๐ โ ((-1โ(๐ผ + ๐ฝ)) ยท 1) = (-1โ(๐ผ + ๐ฝ))) |
161 | 151, 158,
160 | 3eqtrd 2781 |
. . . . . . . 8
โข (๐ โ (-1โ((๐ผ + 1) + (๐ฝ + 1))) = (-1โ(๐ผ + ๐ฝ))) |
162 | 144, 161 | eqtr3d 2779 |
. . . . . . 7
โข (๐ โ ((-1โ(๐ผ + 1)) ยท (-1โ(๐ฝ + 1))) = (-1โ(๐ผ + ๐ฝ))) |
163 | 137 | nn0zd 12532 |
. . . . . . . 8
โข (๐ โ (๐ + 1) โ โค) |
164 | | m1expcl2 13998 |
. . . . . . . 8
โข ((๐ + 1) โ โค โ
(-1โ(๐ + 1)) โ
{-1, 1}) |
165 | | 1neg1t1neg1 31696 |
. . . . . . . 8
โข
((-1โ(๐ + 1))
โ {-1, 1} โ ((-1โ(๐ + 1)) ยท (-1โ(๐ + 1))) = 1) |
166 | 163, 164,
165 | 3syl 18 |
. . . . . . 7
โข (๐ โ ((-1โ(๐ + 1)) ยท (-1โ(๐ + 1))) = 1) |
167 | 162, 166 | oveq12d 7380 |
. . . . . 6
โข (๐ โ (((-1โ(๐ผ + 1)) ยท (-1โ(๐ฝ + 1))) ยท
((-1โ(๐ + 1)) ยท
(-1โ(๐ + 1)))) =
((-1โ(๐ผ + ๐ฝ)) ยท 1)) |
168 | 143, 167,
160 | 3eqtrd 2781 |
. . . . 5
โข (๐ โ (((-1โ(๐ผ + 1)) ยท (-1โ(๐ + 1))) ยท
((-1โ(๐ฝ + 1)) ยท
(-1โ(๐ + 1)))) =
(-1โ(๐ผ + ๐ฝ))) |
169 | 126, 168 | eqtrd 2777 |
. . . 4
โข (๐ โ (((pmSgnโ(1...๐))โ(๐ โ โก๐)) ยท ((pmSgnโ(1...๐))โ(๐ โ โก๐))) = (-1โ(๐ผ + ๐ฝ))) |
170 | 169 | fveq2d 6851 |
. . 3
โข (๐ โ (๐โ(((pmSgnโ(1...๐))โ(๐ โ โก๐)) ยท ((pmSgnโ(1...๐))โ(๐ โ โก๐)))) = (๐โ(-1โ(๐ผ + ๐ฝ)))) |
171 | 170 | oveq1d 7377 |
. 2
โข (๐ โ ((๐โ(((pmSgnโ(1...๐))โ(๐ โ โก๐)) ยท ((pmSgnโ(1...๐))โ(๐ โ โก๐)))) ยท (๐ธโ(๐ผ(subMat1โ๐)๐ฝ))) = ((๐โ(-1โ(๐ผ + ๐ฝ))) ยท (๐ธโ(๐ผ(subMat1โ๐)๐ฝ)))) |
172 | 103, 171 | eqtrd 2777 |
1
โข (๐ โ (๐ฝ(๐พโ๐)๐ผ) = ((๐โ(-1โ(๐ผ + ๐ฝ))) ยท (๐ธโ(๐ผ(subMat1โ๐)๐ฝ)))) |