Step | Hyp | Ref
| Expression |
1 | | mulgpropd.b1 |
. . . . . . 7
โข (๐ โ ๐ต = (Baseโ๐บ)) |
2 | | mulgpropd.b2 |
. . . . . . 7
โข (๐ โ ๐ต = (Baseโ๐ป)) |
3 | | mulgpropdg.g |
. . . . . . 7
โข (๐ โ ๐บ โ ๐) |
4 | | mulgpropdg.h |
. . . . . . 7
โข (๐ โ ๐ป โ ๐) |
5 | | mulgpropd.i |
. . . . . . . . . 10
โข (๐ โ ๐ต โ ๐พ) |
6 | | ssel 3151 |
. . . . . . . . . . 11
โข (๐ต โ ๐พ โ (๐ฅ โ ๐ต โ ๐ฅ โ ๐พ)) |
7 | | ssel 3151 |
. . . . . . . . . . 11
โข (๐ต โ ๐พ โ (๐ฆ โ ๐ต โ ๐ฆ โ ๐พ)) |
8 | 6, 7 | anim12d 335 |
. . . . . . . . . 10
โข (๐ต โ ๐พ โ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ฅ โ ๐พ โง ๐ฆ โ ๐พ))) |
9 | 5, 8 | syl 14 |
. . . . . . . . 9
โข (๐ โ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ฅ โ ๐พ โง ๐ฆ โ ๐พ))) |
10 | 9 | imp 124 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ฅ โ ๐พ โง ๐ฆ โ ๐พ)) |
11 | | mulgpropd.e |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ ๐พ โง ๐ฆ โ ๐พ)) โ (๐ฅ(+gโ๐บ)๐ฆ) = (๐ฅ(+gโ๐ป)๐ฆ)) |
12 | 10, 11 | syldan 282 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ฅ(+gโ๐บ)๐ฆ) = (๐ฅ(+gโ๐ป)๐ฆ)) |
13 | 1, 2, 3, 4, 12 | grpidpropdg 12798 |
. . . . . 6
โข (๐ โ (0gโ๐บ) = (0gโ๐ป)) |
14 | 13 | 3ad2ant1 1018 |
. . . . 5
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ (0gโ๐บ) = (0gโ๐ป)) |
15 | | 1zzd 9282 |
. . . . . . . 8
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ 1 โ โค) |
16 | | nnuz 9565 |
. . . . . . . . 9
โข โ =
(โคโฅโ1) |
17 | 5 | 3ad2ant1 1018 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ ๐ต โ ๐พ) |
18 | | simp3 999 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
19 | 17, 18 | sseldd 3158 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ ๐ โ ๐พ) |
20 | 16, 19 | ialgrlemconst 12045 |
. . . . . . . 8
โข (((๐ โง ๐ โ โค โง ๐ โ ๐ต) โง ๐ฅ โ (โคโฅโ1))
โ ((โ ร {๐})โ๐ฅ) โ ๐พ) |
21 | | mulgpropd.k |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ ๐พ โง ๐ฆ โ ๐พ)) โ (๐ฅ(+gโ๐บ)๐ฆ) โ ๐พ) |
22 | 21 | 3ad2antl1 1159 |
. . . . . . . 8
โข (((๐ โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ฅ โ ๐พ โง ๐ฆ โ ๐พ)) โ (๐ฅ(+gโ๐บ)๐ฆ) โ ๐พ) |
23 | 11 | 3ad2antl1 1159 |
. . . . . . . 8
โข (((๐ โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ฅ โ ๐พ โง ๐ฆ โ ๐พ)) โ (๐ฅ(+gโ๐บ)๐ฆ) = (๐ฅ(+gโ๐ป)๐ฆ)) |
24 | 15, 20, 22, 23 | seqfeq3 10514 |
. . . . . . 7
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ seq1((+gโ๐บ), (โ ร {๐})) =
seq1((+gโ๐ป), (โ ร {๐}))) |
25 | 24 | fveq1d 5519 |
. . . . . 6
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ (seq1((+gโ๐บ), (โ ร {๐}))โ๐) = (seq1((+gโ๐ป), (โ ร {๐}))โ๐)) |
26 | 1, 2, 3, 4, 12 | grpinvpropdg 12950 |
. . . . . . . 8
โข (๐ โ
(invgโ๐บ) =
(invgโ๐ป)) |
27 | 26 | 3ad2ant1 1018 |
. . . . . . 7
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ (invgโ๐บ) = (invgโ๐ป)) |
28 | 24 | fveq1d 5519 |
. . . . . . 7
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ (seq1((+gโ๐บ), (โ ร {๐}))โ-๐) = (seq1((+gโ๐ป), (โ ร {๐}))โ-๐)) |
29 | 27, 28 | fveq12d 5524 |
. . . . . 6
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐)) = ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐))) |
30 | 25, 29 | ifeq12d 3555 |
. . . . 5
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ if(0 < ๐, (seq1((+gโ๐บ), (โ ร {๐}))โ๐), ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐))) = if(0 < ๐, (seq1((+gโ๐ป), (โ ร {๐}))โ๐), ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐)))) |
31 | 14, 30 | ifeq12d 3555 |
. . . 4
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ if(๐ = 0, (0gโ๐บ), if(0 < ๐, (seq1((+gโ๐บ), (โ ร {๐}))โ๐), ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐)))) = if(๐ = 0, (0gโ๐ป), if(0 < ๐, (seq1((+gโ๐ป), (โ ร {๐}))โ๐), ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐))))) |
32 | 31 | mpoeq3dva 5941 |
. . 3
โข (๐ โ (๐ โ โค, ๐ โ ๐ต โฆ if(๐ = 0, (0gโ๐บ), if(0 < ๐, (seq1((+gโ๐บ), (โ ร {๐}))โ๐), ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐))))) = (๐ โ โค, ๐ โ ๐ต โฆ if(๐ = 0, (0gโ๐ป), if(0 < ๐, (seq1((+gโ๐ป), (โ ร {๐}))โ๐), ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐)))))) |
33 | | eqidd 2178 |
. . . 4
โข (๐ โ โค =
โค) |
34 | | eqidd 2178 |
. . . 4
โข (๐ โ if(๐ = 0, (0gโ๐บ), if(0 < ๐, (seq1((+gโ๐บ), (โ ร {๐}))โ๐), ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐)))) = if(๐ = 0, (0gโ๐บ), if(0 < ๐, (seq1((+gโ๐บ), (โ ร {๐}))โ๐), ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐))))) |
35 | 33, 1, 34 | mpoeq123dv 5939 |
. . 3
โข (๐ โ (๐ โ โค, ๐ โ ๐ต โฆ if(๐ = 0, (0gโ๐บ), if(0 < ๐, (seq1((+gโ๐บ), (โ ร {๐}))โ๐), ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐))))) = (๐ โ โค, ๐ โ (Baseโ๐บ) โฆ if(๐ = 0, (0gโ๐บ), if(0 < ๐, (seq1((+gโ๐บ), (โ ร {๐}))โ๐), ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐)))))) |
36 | | eqidd 2178 |
. . . 4
โข (๐ โ if(๐ = 0, (0gโ๐ป), if(0 < ๐, (seq1((+gโ๐ป), (โ ร {๐}))โ๐), ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐)))) = if(๐ = 0, (0gโ๐ป), if(0 < ๐, (seq1((+gโ๐ป), (โ ร {๐}))โ๐), ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐))))) |
37 | 33, 2, 36 | mpoeq123dv 5939 |
. . 3
โข (๐ โ (๐ โ โค, ๐ โ ๐ต โฆ if(๐ = 0, (0gโ๐ป), if(0 < ๐, (seq1((+gโ๐ป), (โ ร {๐}))โ๐), ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐))))) = (๐ โ โค, ๐ โ (Baseโ๐ป) โฆ if(๐ = 0, (0gโ๐ป), if(0 < ๐, (seq1((+gโ๐ป), (โ ร {๐}))โ๐), ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐)))))) |
38 | 32, 35, 37 | 3eqtr3d 2218 |
. 2
โข (๐ โ (๐ โ โค, ๐ โ (Baseโ๐บ) โฆ if(๐ = 0, (0gโ๐บ), if(0 < ๐, (seq1((+gโ๐บ), (โ ร {๐}))โ๐), ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐))))) = (๐ โ โค, ๐ โ (Baseโ๐ป) โฆ if(๐ = 0, (0gโ๐ป), if(0 < ๐, (seq1((+gโ๐ป), (โ ร {๐}))โ๐), ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐)))))) |
39 | | mulgpropdg.m |
. . 3
โข (๐ โ ยท =
(.gโ๐บ)) |
40 | | eqid 2177 |
. . . . 5
โข
(Baseโ๐บ) =
(Baseโ๐บ) |
41 | | eqid 2177 |
. . . . 5
โข
(+gโ๐บ) = (+gโ๐บ) |
42 | | eqid 2177 |
. . . . 5
โข
(0gโ๐บ) = (0gโ๐บ) |
43 | | eqid 2177 |
. . . . 5
โข
(invgโ๐บ) = (invgโ๐บ) |
44 | | eqid 2177 |
. . . . 5
โข
(.gโ๐บ) = (.gโ๐บ) |
45 | 40, 41, 42, 43, 44 | mulgfvalg 12990 |
. . . 4
โข (๐บ โ ๐ โ (.gโ๐บ) = (๐ โ โค, ๐ โ (Baseโ๐บ) โฆ if(๐ = 0, (0gโ๐บ), if(0 < ๐, (seq1((+gโ๐บ), (โ ร {๐}))โ๐), ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐)))))) |
46 | 3, 45 | syl 14 |
. . 3
โข (๐ โ (.gโ๐บ) = (๐ โ โค, ๐ โ (Baseโ๐บ) โฆ if(๐ = 0, (0gโ๐บ), if(0 < ๐, (seq1((+gโ๐บ), (โ ร {๐}))โ๐), ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐)))))) |
47 | 39, 46 | eqtrd 2210 |
. 2
โข (๐ โ ยท = (๐ โ โค, ๐ โ (Baseโ๐บ) โฆ if(๐ = 0, (0gโ๐บ), if(0 < ๐, (seq1((+gโ๐บ), (โ ร {๐}))โ๐), ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐)))))) |
48 | | mulgpropdg.n |
. . 3
โข (๐ โ ร =
(.gโ๐ป)) |
49 | | eqid 2177 |
. . . . 5
โข
(Baseโ๐ป) =
(Baseโ๐ป) |
50 | | eqid 2177 |
. . . . 5
โข
(+gโ๐ป) = (+gโ๐ป) |
51 | | eqid 2177 |
. . . . 5
โข
(0gโ๐ป) = (0gโ๐ป) |
52 | | eqid 2177 |
. . . . 5
โข
(invgโ๐ป) = (invgโ๐ป) |
53 | | eqid 2177 |
. . . . 5
โข
(.gโ๐ป) = (.gโ๐ป) |
54 | 49, 50, 51, 52, 53 | mulgfvalg 12990 |
. . . 4
โข (๐ป โ ๐ โ (.gโ๐ป) = (๐ โ โค, ๐ โ (Baseโ๐ป) โฆ if(๐ = 0, (0gโ๐ป), if(0 < ๐, (seq1((+gโ๐ป), (โ ร {๐}))โ๐), ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐)))))) |
55 | 4, 54 | syl 14 |
. . 3
โข (๐ โ (.gโ๐ป) = (๐ โ โค, ๐ โ (Baseโ๐ป) โฆ if(๐ = 0, (0gโ๐ป), if(0 < ๐, (seq1((+gโ๐ป), (โ ร {๐}))โ๐), ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐)))))) |
56 | 48, 55 | eqtrd 2210 |
. 2
โข (๐ โ ร = (๐ โ โค, ๐ โ (Baseโ๐ป) โฆ if(๐ = 0, (0gโ๐ป), if(0 < ๐, (seq1((+gโ๐ป), (โ ร {๐}))โ๐), ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐)))))) |
57 | 38, 47, 56 | 3eqtr4d 2220 |
1
โข (๐ โ ยท = ร
) |