Step | Hyp | Ref
| Expression |
1 | | mulgval.t |
. 2
โข ยท =
(.gโ๐บ) |
2 | | df-mulg 12984 |
. . 3
โข
.g = (๐ค
โ V โฆ (๐ โ
โค, ๐ฅ โ
(Baseโ๐ค) โฆ
if(๐ = 0,
(0gโ๐ค),
โฆseq1((+gโ๐ค), (โ ร {๐ฅ})) / ๐ โฆif(0 < ๐, (๐ โ๐), ((invgโ๐ค)โ(๐ โ-๐)))))) |
3 | | eqidd 2178 |
. . . 4
โข (๐ค = ๐บ โ โค = โค) |
4 | | fveq2 5516 |
. . . . 5
โข (๐ค = ๐บ โ (Baseโ๐ค) = (Baseโ๐บ)) |
5 | | mulgval.b |
. . . . 5
โข ๐ต = (Baseโ๐บ) |
6 | 4, 5 | eqtr4di 2228 |
. . . 4
โข (๐ค = ๐บ โ (Baseโ๐ค) = ๐ต) |
7 | | fveq2 5516 |
. . . . . 6
โข (๐ค = ๐บ โ (0gโ๐ค) = (0gโ๐บ)) |
8 | | mulgval.o |
. . . . . 6
โข 0 =
(0gโ๐บ) |
9 | 7, 8 | eqtr4di 2228 |
. . . . 5
โข (๐ค = ๐บ โ (0gโ๐ค) = 0 ) |
10 | | seqex 10447 |
. . . . . . 7
โข
seq1((+gโ๐ค), (โ ร {๐ฅ})) โ V |
11 | 10 | a1i 9 |
. . . . . 6
โข (๐ค = ๐บ โ seq1((+gโ๐ค), (โ ร {๐ฅ})) โ V) |
12 | | id 19 |
. . . . . . . . 9
โข (๐ =
seq1((+gโ๐ค), (โ ร {๐ฅ})) โ ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) |
13 | | fveq2 5516 |
. . . . . . . . . . 11
โข (๐ค = ๐บ โ (+gโ๐ค) = (+gโ๐บ)) |
14 | | mulgval.p |
. . . . . . . . . . 11
โข + =
(+gโ๐บ) |
15 | 13, 14 | eqtr4di 2228 |
. . . . . . . . . 10
โข (๐ค = ๐บ โ (+gโ๐ค) = + ) |
16 | 15 | seqeq2d 10452 |
. . . . . . . . 9
โข (๐ค = ๐บ โ seq1((+gโ๐ค), (โ ร {๐ฅ})) = seq1( + , (โ ร {๐ฅ}))) |
17 | 12, 16 | sylan9eqr 2232 |
. . . . . . . 8
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ ๐ = seq1( + , (โ ร {๐ฅ}))) |
18 | 17 | fveq1d 5518 |
. . . . . . 7
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ (๐ โ๐) = (seq1( + , (โ ร {๐ฅ}))โ๐)) |
19 | | simpl 109 |
. . . . . . . . . 10
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ ๐ค = ๐บ) |
20 | 19 | fveq2d 5520 |
. . . . . . . . 9
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ
(invgโ๐ค) =
(invgโ๐บ)) |
21 | | mulgval.i |
. . . . . . . . 9
โข ๐ผ = (invgโ๐บ) |
22 | 20, 21 | eqtr4di 2228 |
. . . . . . . 8
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ
(invgโ๐ค) =
๐ผ) |
23 | 17 | fveq1d 5518 |
. . . . . . . 8
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ (๐ โ-๐) = (seq1( + , (โ ร {๐ฅ}))โ-๐)) |
24 | 22, 23 | fveq12d 5523 |
. . . . . . 7
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ
((invgโ๐ค)โ(๐ โ-๐)) = (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))) |
25 | 18, 24 | ifeq12d 3554 |
. . . . . 6
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ if(0 < ๐, (๐ โ๐), ((invgโ๐ค)โ(๐ โ-๐))) = if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)))) |
26 | 11, 25 | csbied 3104 |
. . . . 5
โข (๐ค = ๐บ โ
โฆseq1((+gโ๐ค), (โ ร {๐ฅ})) / ๐ โฆif(0 < ๐, (๐ โ๐), ((invgโ๐ค)โ(๐ โ-๐))) = if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)))) |
27 | 9, 26 | ifeq12d 3554 |
. . . 4
โข (๐ค = ๐บ โ if(๐ = 0, (0gโ๐ค),
โฆseq1((+gโ๐ค), (โ ร {๐ฅ})) / ๐ โฆif(0 < ๐, (๐ โ๐), ((invgโ๐ค)โ(๐ โ-๐)))) = if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) |
28 | 3, 6, 27 | mpoeq123dv 5937 |
. . 3
โข (๐ค = ๐บ โ (๐ โ โค, ๐ฅ โ (Baseโ๐ค) โฆ if(๐ = 0, (0gโ๐ค),
โฆseq1((+gโ๐ค), (โ ร {๐ฅ})) / ๐ โฆif(0 < ๐, (๐ โ๐), ((invgโ๐ค)โ(๐ โ-๐))))) = (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)))))) |
29 | | elex 2749 |
. . 3
โข (๐บ โ ๐ โ ๐บ โ V) |
30 | | zex 9262 |
. . . 4
โข โค
โ V |
31 | | basfn 12520 |
. . . . . 6
โข Base Fn
V |
32 | | funfvex 5533 |
. . . . . . 7
โข ((Fun
Base โง ๐บ โ dom
Base) โ (Baseโ๐บ)
โ V) |
33 | 32 | funfni 5317 |
. . . . . 6
โข ((Base Fn
V โง ๐บ โ V) โ
(Baseโ๐บ) โ
V) |
34 | 31, 29, 33 | sylancr 414 |
. . . . 5
โข (๐บ โ ๐ โ (Baseโ๐บ) โ V) |
35 | 5, 34 | eqeltrid 2264 |
. . . 4
โข (๐บ โ ๐ โ ๐ต โ V) |
36 | | mpoexga 6213 |
. . . 4
โข ((โค
โ V โง ๐ต โ V)
โ (๐ โ โค,
๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) โ V) |
37 | 30, 35, 36 | sylancr 414 |
. . 3
โข (๐บ โ ๐ โ (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) โ V) |
38 | 2, 28, 29, 37 | fvmptd3 5610 |
. 2
โข (๐บ โ ๐ โ (.gโ๐บ) = (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)))))) |
39 | 1, 38 | eqtrid 2222 |
1
โข (๐บ โ ๐ โ ยท = (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)))))) |