Step | Hyp | Ref
| Expression |
1 | | mulgpropd.b1 |
. . . . . . 7
โข (๐ โ ๐ต = (Baseโ๐บ)) |
2 | | mulgpropd.b2 |
. . . . . . 7
โข (๐ โ ๐ต = (Baseโ๐ป)) |
3 | | mulgpropd.i |
. . . . . . . . . 10
โข (๐ โ ๐ต โ ๐พ) |
4 | | ssel 3935 |
. . . . . . . . . . 11
โข (๐ต โ ๐พ โ (๐ฅ โ ๐ต โ ๐ฅ โ ๐พ)) |
5 | | ssel 3935 |
. . . . . . . . . . 11
โข (๐ต โ ๐พ โ (๐ฆ โ ๐ต โ ๐ฆ โ ๐พ)) |
6 | 4, 5 | anim12d 609 |
. . . . . . . . . 10
โข (๐ต โ ๐พ โ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ฅ โ ๐พ โง ๐ฆ โ ๐พ))) |
7 | 3, 6 | syl 17 |
. . . . . . . . 9
โข (๐ โ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ฅ โ ๐พ โง ๐ฆ โ ๐พ))) |
8 | 7 | imp 407 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ฅ โ ๐พ โง ๐ฆ โ ๐พ)) |
9 | | mulgpropd.e |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ ๐พ โง ๐ฆ โ ๐พ)) โ (๐ฅ(+gโ๐บ)๐ฆ) = (๐ฅ(+gโ๐ป)๐ฆ)) |
10 | 8, 9 | syldan 591 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ฅ(+gโ๐บ)๐ฆ) = (๐ฅ(+gโ๐ป)๐ฆ)) |
11 | 1, 2, 10 | grpidpropd 18477 |
. . . . . 6
โข (๐ โ (0gโ๐บ) = (0gโ๐ป)) |
12 | 11 | 3ad2ant1 1133 |
. . . . 5
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ (0gโ๐บ) = (0gโ๐ป)) |
13 | | 1zzd 12492 |
. . . . . . . 8
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ 1 โ โค) |
14 | | vex 3447 |
. . . . . . . . . . . 12
โข ๐ โ V |
15 | 14 | fvconst2 7149 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ ((โ
ร {๐})โ๐ฅ) = ๐) |
16 | | nnuz 12760 |
. . . . . . . . . . . 12
โข โ =
(โคโฅโ1) |
17 | 16 | eqcomi 2746 |
. . . . . . . . . . 11
โข
(โคโฅโ1) = โ |
18 | 15, 17 | eleq2s 2856 |
. . . . . . . . . 10
โข (๐ฅ โ
(โคโฅโ1) โ ((โ ร {๐})โ๐ฅ) = ๐) |
19 | 18 | adantl 482 |
. . . . . . . . 9
โข (((๐ โง ๐ โ โค โง ๐ โ ๐ต) โง ๐ฅ โ (โคโฅโ1))
โ ((โ ร {๐})โ๐ฅ) = ๐) |
20 | 3 | 3ad2ant1 1133 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ ๐ต โ ๐พ) |
21 | | simp3 1138 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
22 | 20, 21 | sseldd 3943 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ ๐ โ ๐พ) |
23 | 22 | adantr 481 |
. . . . . . . . 9
โข (((๐ โง ๐ โ โค โง ๐ โ ๐ต) โง ๐ฅ โ (โคโฅโ1))
โ ๐ โ ๐พ) |
24 | 19, 23 | eqeltrd 2838 |
. . . . . . . 8
โข (((๐ โง ๐ โ โค โง ๐ โ ๐ต) โง ๐ฅ โ (โคโฅโ1))
โ ((โ ร {๐})โ๐ฅ) โ ๐พ) |
25 | | mulgpropd.k |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ ๐พ โง ๐ฆ โ ๐พ)) โ (๐ฅ(+gโ๐บ)๐ฆ) โ ๐พ) |
26 | 25 | 3ad2antl1 1185 |
. . . . . . . 8
โข (((๐ โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ฅ โ ๐พ โง ๐ฆ โ ๐พ)) โ (๐ฅ(+gโ๐บ)๐ฆ) โ ๐พ) |
27 | 9 | 3ad2antl1 1185 |
. . . . . . . 8
โข (((๐ โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ฅ โ ๐พ โง ๐ฆ โ ๐พ)) โ (๐ฅ(+gโ๐บ)๐ฆ) = (๐ฅ(+gโ๐ป)๐ฆ)) |
28 | 13, 24, 26, 27 | seqfeq3 13912 |
. . . . . . 7
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ seq1((+gโ๐บ), (โ ร {๐})) =
seq1((+gโ๐ป), (โ ร {๐}))) |
29 | 28 | fveq1d 6841 |
. . . . . 6
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ (seq1((+gโ๐บ), (โ ร {๐}))โ๐) = (seq1((+gโ๐ป), (โ ร {๐}))โ๐)) |
30 | 1, 2, 10 | grpinvpropd 18781 |
. . . . . . . 8
โข (๐ โ
(invgโ๐บ) =
(invgโ๐ป)) |
31 | 30 | 3ad2ant1 1133 |
. . . . . . 7
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ (invgโ๐บ) = (invgโ๐ป)) |
32 | 28 | fveq1d 6841 |
. . . . . . 7
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ (seq1((+gโ๐บ), (โ ร {๐}))โ-๐) = (seq1((+gโ๐ป), (โ ร {๐}))โ-๐)) |
33 | 31, 32 | fveq12d 6846 |
. . . . . 6
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐)) = ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐))) |
34 | 29, 33 | ifeq12d 4505 |
. . . . 5
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ if(0 < ๐, (seq1((+gโ๐บ), (โ ร {๐}))โ๐), ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐))) = if(0 < ๐, (seq1((+gโ๐ป), (โ ร {๐}))โ๐), ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐)))) |
35 | 12, 34 | ifeq12d 4505 |
. . . 4
โข ((๐ โง ๐ โ โค โง ๐ โ ๐ต) โ if(๐ = 0, (0gโ๐บ), if(0 < ๐, (seq1((+gโ๐บ), (โ ร {๐}))โ๐), ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐)))) = if(๐ = 0, (0gโ๐ป), if(0 < ๐, (seq1((+gโ๐ป), (โ ร {๐}))โ๐), ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐))))) |
36 | 35 | mpoeq3dva 7428 |
. . 3
โข (๐ โ (๐ โ โค, ๐ โ ๐ต โฆ if(๐ = 0, (0gโ๐บ), if(0 < ๐, (seq1((+gโ๐บ), (โ ร {๐}))โ๐), ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐))))) = (๐ โ โค, ๐ โ ๐ต โฆ if(๐ = 0, (0gโ๐ป), if(0 < ๐, (seq1((+gโ๐ป), (โ ร {๐}))โ๐), ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐)))))) |
37 | | eqidd 2738 |
. . . 4
โข (๐ โ โค =
โค) |
38 | | eqidd 2738 |
. . . 4
โข (๐ โ if(๐ = 0, (0gโ๐บ), if(0 < ๐, (seq1((+gโ๐บ), (โ ร {๐}))โ๐), ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐)))) = if(๐ = 0, (0gโ๐บ), if(0 < ๐, (seq1((+gโ๐บ), (โ ร {๐}))โ๐), ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐))))) |
39 | 37, 1, 38 | mpoeq123dv 7426 |
. . 3
โข (๐ โ (๐ โ โค, ๐ โ ๐ต โฆ if(๐ = 0, (0gโ๐บ), if(0 < ๐, (seq1((+gโ๐บ), (โ ร {๐}))โ๐), ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐))))) = (๐ โ โค, ๐ โ (Baseโ๐บ) โฆ if(๐ = 0, (0gโ๐บ), if(0 < ๐, (seq1((+gโ๐บ), (โ ร {๐}))โ๐), ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐)))))) |
40 | | eqidd 2738 |
. . . 4
โข (๐ โ if(๐ = 0, (0gโ๐ป), if(0 < ๐, (seq1((+gโ๐ป), (โ ร {๐}))โ๐), ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐)))) = if(๐ = 0, (0gโ๐ป), if(0 < ๐, (seq1((+gโ๐ป), (โ ร {๐}))โ๐), ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐))))) |
41 | 37, 2, 40 | mpoeq123dv 7426 |
. . 3
โข (๐ โ (๐ โ โค, ๐ โ ๐ต โฆ if(๐ = 0, (0gโ๐ป), if(0 < ๐, (seq1((+gโ๐ป), (โ ร {๐}))โ๐), ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐))))) = (๐ โ โค, ๐ โ (Baseโ๐ป) โฆ if(๐ = 0, (0gโ๐ป), if(0 < ๐, (seq1((+gโ๐ป), (โ ร {๐}))โ๐), ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐)))))) |
42 | 36, 39, 41 | 3eqtr3d 2785 |
. 2
โข (๐ โ (๐ โ โค, ๐ โ (Baseโ๐บ) โฆ if(๐ = 0, (0gโ๐บ), if(0 < ๐, (seq1((+gโ๐บ), (โ ร {๐}))โ๐), ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐))))) = (๐ โ โค, ๐ โ (Baseโ๐ป) โฆ if(๐ = 0, (0gโ๐ป), if(0 < ๐, (seq1((+gโ๐ป), (โ ร {๐}))โ๐), ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐)))))) |
43 | | eqid 2737 |
. . 3
โข
(Baseโ๐บ) =
(Baseโ๐บ) |
44 | | eqid 2737 |
. . 3
โข
(+gโ๐บ) = (+gโ๐บ) |
45 | | eqid 2737 |
. . 3
โข
(0gโ๐บ) = (0gโ๐บ) |
46 | | eqid 2737 |
. . 3
โข
(invgโ๐บ) = (invgโ๐บ) |
47 | | mulgpropd.m |
. . 3
โข ยท =
(.gโ๐บ) |
48 | 43, 44, 45, 46, 47 | mulgfval 18833 |
. 2
โข ยท =
(๐ โ โค, ๐ โ (Baseโ๐บ) โฆ if(๐ = 0, (0gโ๐บ), if(0 < ๐, (seq1((+gโ๐บ), (โ ร {๐}))โ๐), ((invgโ๐บ)โ(seq1((+gโ๐บ), (โ ร {๐}))โ-๐))))) |
49 | | eqid 2737 |
. . 3
โข
(Baseโ๐ป) =
(Baseโ๐ป) |
50 | | eqid 2737 |
. . 3
โข
(+gโ๐ป) = (+gโ๐ป) |
51 | | eqid 2737 |
. . 3
โข
(0gโ๐ป) = (0gโ๐ป) |
52 | | eqid 2737 |
. . 3
โข
(invgโ๐ป) = (invgโ๐ป) |
53 | | mulgpropd.n |
. . 3
โข ร =
(.gโ๐ป) |
54 | 49, 50, 51, 52, 53 | mulgfval 18833 |
. 2
โข ร =
(๐ โ โค, ๐ โ (Baseโ๐ป) โฆ if(๐ = 0, (0gโ๐ป), if(0 < ๐, (seq1((+gโ๐ป), (โ ร {๐}))โ๐), ((invgโ๐ป)โ(seq1((+gโ๐ป), (โ ร {๐}))โ-๐))))) |
55 | 42, 48, 54 | 3eqtr4g 2802 |
1
โข (๐ โ ยท = ร
) |