Step | Hyp | Ref
| Expression |
1 | | mulgval.t |
. 2
โข ยท =
(.gโ๐บ) |
2 | | eqidd 2738 |
. . . . 5
โข (๐ค = ๐บ โ โค = โค) |
3 | | fveq2 6839 |
. . . . . 6
โข (๐ค = ๐บ โ (Baseโ๐ค) = (Baseโ๐บ)) |
4 | | mulgval.b |
. . . . . 6
โข ๐ต = (Baseโ๐บ) |
5 | 3, 4 | eqtr4di 2795 |
. . . . 5
โข (๐ค = ๐บ โ (Baseโ๐ค) = ๐ต) |
6 | | fveq2 6839 |
. . . . . . 7
โข (๐ค = ๐บ โ (0gโ๐ค) = (0gโ๐บ)) |
7 | | mulgval.o |
. . . . . . 7
โข 0 =
(0gโ๐บ) |
8 | 6, 7 | eqtr4di 2795 |
. . . . . 6
โข (๐ค = ๐บ โ (0gโ๐ค) = 0 ) |
9 | | seqex 13862 |
. . . . . . . 8
โข
seq1((+gโ๐ค), (โ ร {๐ฅ})) โ V |
10 | 9 | a1i 11 |
. . . . . . 7
โข (๐ค = ๐บ โ seq1((+gโ๐ค), (โ ร {๐ฅ})) โ V) |
11 | | id 22 |
. . . . . . . . . 10
โข (๐ =
seq1((+gโ๐ค), (โ ร {๐ฅ})) โ ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) |
12 | | fveq2 6839 |
. . . . . . . . . . . 12
โข (๐ค = ๐บ โ (+gโ๐ค) = (+gโ๐บ)) |
13 | | mulgval.p |
. . . . . . . . . . . 12
โข + =
(+gโ๐บ) |
14 | 12, 13 | eqtr4di 2795 |
. . . . . . . . . . 11
โข (๐ค = ๐บ โ (+gโ๐ค) = + ) |
15 | 14 | seqeq2d 13867 |
. . . . . . . . . 10
โข (๐ค = ๐บ โ seq1((+gโ๐ค), (โ ร {๐ฅ})) = seq1( + , (โ ร {๐ฅ}))) |
16 | 11, 15 | sylan9eqr 2799 |
. . . . . . . . 9
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ ๐ = seq1( + , (โ ร {๐ฅ}))) |
17 | 16 | fveq1d 6841 |
. . . . . . . 8
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ (๐ โ๐) = (seq1( + , (โ ร {๐ฅ}))โ๐)) |
18 | | simpl 483 |
. . . . . . . . . . 11
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ ๐ค = ๐บ) |
19 | 18 | fveq2d 6843 |
. . . . . . . . . 10
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ
(invgโ๐ค) =
(invgโ๐บ)) |
20 | | mulgval.i |
. . . . . . . . . 10
โข ๐ผ = (invgโ๐บ) |
21 | 19, 20 | eqtr4di 2795 |
. . . . . . . . 9
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ
(invgโ๐ค) =
๐ผ) |
22 | 16 | fveq1d 6841 |
. . . . . . . . 9
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ (๐ โ-๐) = (seq1( + , (โ ร {๐ฅ}))โ-๐)) |
23 | 21, 22 | fveq12d 6846 |
. . . . . . . 8
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ
((invgโ๐ค)โ(๐ โ-๐)) = (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))) |
24 | 17, 23 | ifeq12d 4505 |
. . . . . . 7
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ if(0 < ๐, (๐ โ๐), ((invgโ๐ค)โ(๐ โ-๐))) = if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)))) |
25 | 10, 24 | csbied 3891 |
. . . . . 6
โข (๐ค = ๐บ โ
โฆseq1((+gโ๐ค), (โ ร {๐ฅ})) / ๐ โฆif(0 < ๐, (๐ โ๐), ((invgโ๐ค)โ(๐ โ-๐))) = if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)))) |
26 | 8, 25 | ifeq12d 4505 |
. . . . 5
โข (๐ค = ๐บ โ if(๐ = 0, (0gโ๐ค),
โฆseq1((+gโ๐ค), (โ ร {๐ฅ})) / ๐ โฆif(0 < ๐, (๐ โ๐), ((invgโ๐ค)โ(๐ โ-๐)))) = if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) |
27 | 2, 5, 26 | mpoeq123dv 7426 |
. . . 4
โข (๐ค = ๐บ โ (๐ โ โค, ๐ฅ โ (Baseโ๐ค) โฆ if(๐ = 0, (0gโ๐ค),
โฆseq1((+gโ๐ค), (โ ร {๐ฅ})) / ๐ โฆif(0 < ๐, (๐ โ๐), ((invgโ๐ค)โ(๐ โ-๐))))) = (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)))))) |
28 | | df-mulg 18832 |
. . . 4
โข
.g = (๐ค
โ V โฆ (๐ โ
โค, ๐ฅ โ
(Baseโ๐ค) โฆ
if(๐ = 0,
(0gโ๐ค),
โฆseq1((+gโ๐ค), (โ ร {๐ฅ})) / ๐ โฆif(0 < ๐, (๐ โ๐), ((invgโ๐ค)โ(๐ โ-๐)))))) |
29 | | zex 12466 |
. . . . 5
โข โค
โ V |
30 | 4 | fvexi 6853 |
. . . . 5
โข ๐ต โ V |
31 | 29, 30 | mpoex 8004 |
. . . 4
โข (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) โ V |
32 | 27, 28, 31 | fvmpt 6945 |
. . 3
โข (๐บ โ V โ
(.gโ๐บ) =
(๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)))))) |
33 | | fvprc 6831 |
. . . 4
โข (ยฌ
๐บ โ V โ
(.gโ๐บ) =
โ
) |
34 | | eqid 2737 |
. . . . . . 7
โข (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) = (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) |
35 | 7 | fvexi 6853 |
. . . . . . . 8
โข 0 โ
V |
36 | | fvex 6852 |
. . . . . . . . 9
โข (seq1(
+ ,
(โ ร {๐ฅ}))โ๐) โ V |
37 | | fvex 6852 |
. . . . . . . . 9
โข (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)) โ V |
38 | 36, 37 | ifex 4534 |
. . . . . . . 8
โข if(0 <
๐, (seq1( + , (โ
ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))) โ V |
39 | 35, 38 | ifex 4534 |
. . . . . . 7
โข if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)))) โ V |
40 | 34, 39 | fnmpoi 7994 |
. . . . . 6
โข (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) Fn (โค ร ๐ต) |
41 | | fvprc 6831 |
. . . . . . . . . 10
โข (ยฌ
๐บ โ V โ
(Baseโ๐บ) =
โ
) |
42 | 4, 41 | eqtrid 2789 |
. . . . . . . . 9
โข (ยฌ
๐บ โ V โ ๐ต = โ
) |
43 | 42 | xpeq2d 5661 |
. . . . . . . 8
โข (ยฌ
๐บ โ V โ (โค
ร ๐ต) = (โค
ร โ
)) |
44 | | xp0 6108 |
. . . . . . . 8
โข (โค
ร โ
) = โ
|
45 | 43, 44 | eqtrdi 2793 |
. . . . . . 7
โข (ยฌ
๐บ โ V โ (โค
ร ๐ต) =
โ
) |
46 | 45 | fneq2d 6593 |
. . . . . 6
โข (ยฌ
๐บ โ V โ ((๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) Fn (โค ร ๐ต) โ (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) Fn โ
)) |
47 | 40, 46 | mpbii 232 |
. . . . 5
โข (ยฌ
๐บ โ V โ (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) Fn โ
) |
48 | | fn0 6629 |
. . . . 5
โข ((๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) Fn โ
โ (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) = โ
) |
49 | 47, 48 | sylib 217 |
. . . 4
โข (ยฌ
๐บ โ V โ (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) = โ
) |
50 | 33, 49 | eqtr4d 2780 |
. . 3
โข (ยฌ
๐บ โ V โ
(.gโ๐บ) =
(๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)))))) |
51 | 32, 50 | pm2.61i 182 |
. 2
โข
(.gโ๐บ) = (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) |
52 | 1, 51 | eqtri 2765 |
1
โข ยท =
(๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) |