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 | | fvex 6852 |
. . . . . . . . 9
โข
(+gโ๐ค) โ V |
10 | | 1z 12491 |
. . . . . . . . 9
โข 1 โ
โค |
11 | 9, 10 | seqexw 13876 |
. . . . . . . 8
โข
seq1((+gโ๐ค), (โ ร {๐ฅ})) โ V |
12 | 11 | a1i 11 |
. . . . . . 7
โข (๐ค = ๐บ โ seq1((+gโ๐ค), (โ ร {๐ฅ})) โ V) |
13 | | id 22 |
. . . . . . . . . 10
โข (๐ =
seq1((+gโ๐ค), (โ ร {๐ฅ})) โ ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) |
14 | | fveq2 6839 |
. . . . . . . . . . . 12
โข (๐ค = ๐บ โ (+gโ๐ค) = (+gโ๐บ)) |
15 | | mulgval.p |
. . . . . . . . . . . 12
โข + =
(+gโ๐บ) |
16 | 14, 15 | eqtr4di 2795 |
. . . . . . . . . . 11
โข (๐ค = ๐บ โ (+gโ๐ค) = + ) |
17 | 16 | seqeq2d 13867 |
. . . . . . . . . 10
โข (๐ค = ๐บ โ seq1((+gโ๐ค), (โ ร {๐ฅ})) = seq1( + , (โ ร {๐ฅ}))) |
18 | 13, 17 | sylan9eqr 2799 |
. . . . . . . . 9
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ ๐ = seq1( + , (โ ร {๐ฅ}))) |
19 | 18 | fveq1d 6841 |
. . . . . . . 8
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ (๐ โ๐) = (seq1( + , (โ ร {๐ฅ}))โ๐)) |
20 | | simpl 483 |
. . . . . . . . . . 11
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ ๐ค = ๐บ) |
21 | 20 | fveq2d 6843 |
. . . . . . . . . 10
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ
(invgโ๐ค) =
(invgโ๐บ)) |
22 | | mulgval.i |
. . . . . . . . . 10
โข ๐ผ = (invgโ๐บ) |
23 | 21, 22 | eqtr4di 2795 |
. . . . . . . . 9
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ
(invgโ๐ค) =
๐ผ) |
24 | 18 | fveq1d 6841 |
. . . . . . . . 9
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ (๐ โ-๐) = (seq1( + , (โ ร {๐ฅ}))โ-๐)) |
25 | 23, 24 | fveq12d 6846 |
. . . . . . . 8
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ
((invgโ๐ค)โ(๐ โ-๐)) = (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))) |
26 | 19, 25 | ifeq12d 4505 |
. . . . . . 7
โข ((๐ค = ๐บ โง ๐ = seq1((+gโ๐ค), (โ ร {๐ฅ}))) โ if(0 < ๐, (๐ โ๐), ((invgโ๐ค)โ(๐ โ-๐))) = if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)))) |
27 | 12, 26 | csbied 3891 |
. . . . . 6
โข (๐ค = ๐บ โ
โฆseq1((+gโ๐ค), (โ ร {๐ฅ})) / ๐ โฆif(0 < ๐, (๐ โ๐), ((invgโ๐ค)โ(๐ โ-๐))) = if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)))) |
28 | 8, 27 | ifeq12d 4505 |
. . . . 5
โข (๐ค = ๐บ โ if(๐ = 0, (0gโ๐ค),
โฆseq1((+gโ๐ค), (โ ร {๐ฅ})) / ๐ โฆif(0 < ๐, (๐ โ๐), ((invgโ๐ค)โ(๐ โ-๐)))) = if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) |
29 | 2, 5, 28 | mpoeq123dv 7426 |
. . . 4
โข (๐ค = ๐บ โ (๐ โ โค, ๐ฅ โ (Baseโ๐ค) โฆ if(๐ = 0, (0gโ๐ค),
โฆseq1((+gโ๐ค), (โ ร {๐ฅ})) / ๐ โฆif(0 < ๐, (๐ โ๐), ((invgโ๐ค)โ(๐ โ-๐))))) = (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)))))) |
30 | | df-mulg 18832 |
. . . 4
โข
.g = (๐ค
โ V โฆ (๐ โ
โค, ๐ฅ โ
(Baseโ๐ค) โฆ
if(๐ = 0,
(0gโ๐ค),
โฆseq1((+gโ๐ค), (โ ร {๐ฅ})) / ๐ โฆif(0 < ๐, (๐ โ๐), ((invgโ๐ค)โ(๐ โ-๐)))))) |
31 | | zex 12466 |
. . . . 5
โข โค
โ V |
32 | 4 | fvexi 6853 |
. . . . 5
โข ๐ต โ V |
33 | | snex 5386 |
. . . . . 6
โข { 0 } โ
V |
34 | 15 | fvexi 6853 |
. . . . . . . . 9
โข + โ
V |
35 | 34 | rnex 7841 |
. . . . . . . 8
โข ran + โ
V |
36 | 35, 32 | unex 7672 |
. . . . . . 7
โข (ran
+ โช
๐ต) โ
V |
37 | 22 | fvexi 6853 |
. . . . . . . . 9
โข ๐ผ โ V |
38 | 37 | rnex 7841 |
. . . . . . . 8
โข ran ๐ผ โ V |
39 | | p0ex 5337 |
. . . . . . . 8
โข {โ
}
โ V |
40 | 38, 39 | unex 7672 |
. . . . . . 7
โข (ran
๐ผ โช {โ
}) โ
V |
41 | 36, 40 | unex 7672 |
. . . . . 6
โข ((ran
+ โช
๐ต) โช (ran ๐ผ โช {โ
})) โ
V |
42 | 33, 41 | unex 7672 |
. . . . 5
โข ({ 0 } โช ((ran
+ โช
๐ต) โช (ran ๐ผ โช {โ
}))) โ
V |
43 | | ssun1 4130 |
. . . . . . . . 9
โข { 0 } โ ({
0 } โช
((ran +
โช ๐ต) โช (ran ๐ผ โช
{โ
}))) |
44 | 7 | fvexi 6853 |
. . . . . . . . . 10
โข 0 โ
V |
45 | 44 | snid 4620 |
. . . . . . . . 9
โข 0 โ {
0
} |
46 | 43, 45 | sselii 3939 |
. . . . . . . 8
โข 0 โ ({
0 } โช
((ran +
โช ๐ต) โช (ran ๐ผ โช
{โ
}))) |
47 | 46 | a1i 11 |
. . . . . . 7
โข ((๐ โ โค โง ๐ฅ โ ๐ต) โ 0 โ ({ 0 } โช ((ran
+ โช
๐ต) โช (ran ๐ผ โช
{โ
})))) |
48 | | ssun2 4131 |
. . . . . . . . . . . . . 14
โข ๐ต โ (ran + โช ๐ต) |
49 | | ssun1 4130 |
. . . . . . . . . . . . . 14
โข (ran
+ โช
๐ต) โ ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
})) |
50 | 48, 49 | sstri 3951 |
. . . . . . . . . . . . 13
โข ๐ต โ ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
})) |
51 | | ssun2 4131 |
. . . . . . . . . . . . 13
โข ((ran
+ โช
๐ต) โช (ran ๐ผ โช {โ
})) โ ({
0 } โช
((ran +
โช ๐ต) โช (ran ๐ผ โช
{โ
}))) |
52 | 50, 51 | sstri 3951 |
. . . . . . . . . . . 12
โข ๐ต โ ({ 0 } โช ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
}))) |
53 | | fveq2 6839 |
. . . . . . . . . . . . . 14
โข (๐ = 1 โ (seq1( + , (โ
ร {๐ฅ}))โ๐) = (seq1( + , (โ ร {๐ฅ}))โ1)) |
54 | 53 | adantl 482 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ ๐ต โง ๐ = 1) โ (seq1( + , (โ ร {๐ฅ}))โ๐) = (seq1( + , (โ ร {๐ฅ}))โ1)) |
55 | | seq1 13873 |
. . . . . . . . . . . . . . . 16
โข (1 โ
โค โ (seq1( + , (โ ร {๐ฅ}))โ1) = ((โ ร
{๐ฅ})โ1)) |
56 | 10, 55 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข (seq1(
+ ,
(โ ร {๐ฅ}))โ1) = ((โ ร {๐ฅ})โ1) |
57 | | 1nn 12122 |
. . . . . . . . . . . . . . . . . 18
โข 1 โ
โ |
58 | | vex 3447 |
. . . . . . . . . . . . . . . . . . 19
โข ๐ฅ โ V |
59 | 58 | fvconst2 7149 |
. . . . . . . . . . . . . . . . . 18
โข (1 โ
โ โ ((โ ร {๐ฅ})โ1) = ๐ฅ) |
60 | 57, 59 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
โข ((โ
ร {๐ฅ})โ1) =
๐ฅ |
61 | 60 | eleq1i 2828 |
. . . . . . . . . . . . . . . 16
โข
(((โ ร {๐ฅ})โ1) โ ๐ต โ ๐ฅ โ ๐ต) |
62 | 61 | biimpri 227 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ ๐ต โ ((โ ร {๐ฅ})โ1) โ ๐ต) |
63 | 56, 62 | eqeltrid 2842 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ ๐ต โ (seq1( + , (โ ร {๐ฅ}))โ1) โ ๐ต) |
64 | 63 | adantr 481 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ ๐ต โง ๐ = 1) โ (seq1( + , (โ ร {๐ฅ}))โ1) โ ๐ต) |
65 | 54, 64 | eqeltrd 2838 |
. . . . . . . . . . . 12
โข ((๐ฅ โ ๐ต โง ๐ = 1) โ (seq1( + , (โ ร {๐ฅ}))โ๐) โ ๐ต) |
66 | 52, 65 | sselid 3940 |
. . . . . . . . . . 11
โข ((๐ฅ โ ๐ต โง ๐ = 1) โ (seq1( + , (โ ร {๐ฅ}))โ๐) โ ({ 0 } โช ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
})))) |
67 | 66 | ad4ant24 752 |
. . . . . . . . . 10
โข ((((๐ โ โค โง ๐ฅ โ ๐ต) โง ๐ โ (โคโฅโ1))
โง ๐ = 1) โ (seq1(
+ ,
(โ ร {๐ฅ}))โ๐) โ ({ 0 } โช ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
})))) |
68 | | zcn 12462 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ ๐ โ
โ) |
69 | | npcan1 11538 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ((๐ โ 1) + 1) = ๐) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ((๐ โ 1) + 1) = ๐) |
71 | 70 | fveq2d 6843 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ (seq1(
+ ,
(โ ร {๐ฅ}))โ((๐ โ 1) + 1)) = (seq1( + , (โ ร {๐ฅ}))โ๐)) |
72 | 71 | adantr 481 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง (๐ โ 1) โ
(โคโฅโ1)) โ (seq1( + , (โ ร {๐ฅ}))โ((๐ โ 1) + 1)) = (seq1( + , (โ ร {๐ฅ}))โ๐)) |
73 | | seqp1 13875 |
. . . . . . . . . . . . . 14
โข ((๐ โ 1) โ
(โคโฅโ1) โ (seq1( + , (โ ร {๐ฅ}))โ((๐ โ 1) + 1)) = ((seq1( + , (โ
ร {๐ฅ}))โ(๐ โ 1)) + ((โ ร {๐ฅ})โ((๐ โ 1) + 1)))) |
74 | | ssun1 4130 |
. . . . . . . . . . . . . . . . 17
โข ran + โ (ran
+ โช
๐ต) |
75 | | ssun2 4131 |
. . . . . . . . . . . . . . . . 17
โข {โ
}
โ (ran ๐ผ โช
{โ
}) |
76 | | unss12 4140 |
. . . . . . . . . . . . . . . . 17
โข ((ran
+ โ
(ran +
โช ๐ต) โง {โ
}
โ (ran ๐ผ โช
{โ
})) โ (ran + โช {โ
}) โ
((ran +
โช ๐ต) โช (ran ๐ผ โช
{โ
}))) |
77 | 74, 75, 76 | mp2an 690 |
. . . . . . . . . . . . . . . 16
โข (ran
+ โช
{โ
}) โ ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
})) |
78 | 77, 51 | sstri 3951 |
. . . . . . . . . . . . . . 15
โข (ran
+ โช
{โ
}) โ ({ 0 } โช ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
}))) |
79 | | df-ov 7354 |
. . . . . . . . . . . . . . . 16
โข ((seq1(
+ ,
(โ ร {๐ฅ}))โ(๐ โ 1)) + ((โ ร {๐ฅ})โ((๐ โ 1) + 1))) = ( + โโจ(seq1( + , (โ
ร {๐ฅ}))โ(๐ โ 1)), ((โ ร
{๐ฅ})โ((๐ โ 1) +
1))โฉ) |
80 | | fvrn0 6869 |
. . . . . . . . . . . . . . . 16
โข ( +
โโจ(seq1( + , (โ ร {๐ฅ}))โ(๐ โ 1)), ((โ ร {๐ฅ})โ((๐ โ 1) + 1))โฉ) โ (ran + โช
{โ
}) |
81 | 79, 80 | eqeltri 2834 |
. . . . . . . . . . . . . . 15
โข ((seq1(
+ ,
(โ ร {๐ฅ}))โ(๐ โ 1)) + ((โ ร {๐ฅ})โ((๐ โ 1) + 1))) โ (ran + โช
{โ
}) |
82 | 78, 81 | sselii 3939 |
. . . . . . . . . . . . . 14
โข ((seq1(
+ ,
(โ ร {๐ฅ}))โ(๐ โ 1)) + ((โ ร {๐ฅ})โ((๐ โ 1) + 1))) โ ({ 0 } โช ((ran
+ โช
๐ต) โช (ran ๐ผ โช
{โ
}))) |
83 | 73, 82 | eqeltrdi 2846 |
. . . . . . . . . . . . 13
โข ((๐ โ 1) โ
(โคโฅโ1) โ (seq1( + , (โ ร {๐ฅ}))โ((๐ โ 1) + 1)) โ ({ 0 } โช ((ran
+ โช
๐ต) โช (ran ๐ผ โช
{โ
})))) |
84 | 83 | adantl 482 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง (๐ โ 1) โ
(โคโฅโ1)) โ (seq1( + , (โ ร {๐ฅ}))โ((๐ โ 1) + 1)) โ ({ 0 } โช ((ran
+ โช
๐ต) โช (ran ๐ผ โช
{โ
})))) |
85 | 72, 84 | eqeltrrd 2839 |
. . . . . . . . . . 11
โข ((๐ โ โค โง (๐ โ 1) โ
(โคโฅโ1)) โ (seq1( + , (โ ร {๐ฅ}))โ๐) โ ({ 0 } โช ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
})))) |
86 | 85 | ad4ant14 750 |
. . . . . . . . . 10
โข ((((๐ โ โค โง ๐ฅ โ ๐ต) โง ๐ โ (โคโฅโ1))
โง (๐ โ 1) โ
(โคโฅโ1)) โ (seq1( + , (โ ร {๐ฅ}))โ๐) โ ({ 0 } โช ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
})))) |
87 | | uzm1 12755 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ1) โ (๐ = 1 โจ (๐ โ 1) โ
(โคโฅโ1))) |
88 | 87 | adantl 482 |
. . . . . . . . . 10
โข (((๐ โ โค โง ๐ฅ โ ๐ต) โง ๐ โ (โคโฅโ1))
โ (๐ = 1 โจ (๐ โ 1) โ
(โคโฅโ1))) |
89 | 67, 86, 88 | mpjaodan 957 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ฅ โ ๐ต) โง ๐ โ (โคโฅโ1))
โ (seq1( + , (โ ร {๐ฅ}))โ๐) โ ({ 0 } โช ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
})))) |
90 | | simpr 485 |
. . . . . . . . . . . 12
โข (((๐ โ โค โง ๐ฅ โ ๐ต) โง ยฌ ๐ โ (โคโฅโ1))
โ ยฌ ๐ โ
(โคโฅโ1)) |
91 | | seqfn 13872 |
. . . . . . . . . . . . . . 15
โข (1 โ
โค โ seq1( + , (โ ร {๐ฅ})) Fn
(โคโฅโ1)) |
92 | 10, 91 | ax-mp 5 |
. . . . . . . . . . . . . 14
โข seq1(
+ ,
(โ ร {๐ฅ})) Fn
(โคโฅโ1) |
93 | 92 | fndmi 6603 |
. . . . . . . . . . . . 13
โข dom seq1(
+ ,
(โ ร {๐ฅ})) =
(โคโฅโ1) |
94 | 93 | eleq2i 2829 |
. . . . . . . . . . . 12
โข (๐ โ dom seq1( + , (โ
ร {๐ฅ})) โ ๐ โ
(โคโฅโ1)) |
95 | 90, 94 | sylnibr 328 |
. . . . . . . . . . 11
โข (((๐ โ โค โง ๐ฅ โ ๐ต) โง ยฌ ๐ โ (โคโฅโ1))
โ ยฌ ๐ โ dom
seq1( + ,
(โ ร {๐ฅ}))) |
96 | | ndmfv 6874 |
. . . . . . . . . . 11
โข (ยฌ
๐ โ dom seq1( + , (โ
ร {๐ฅ})) โ (seq1(
+ ,
(โ ร {๐ฅ}))โ๐) = โ
) |
97 | 95, 96 | syl 17 |
. . . . . . . . . 10
โข (((๐ โ โค โง ๐ฅ โ ๐ต) โง ยฌ ๐ โ (โคโฅโ1))
โ (seq1( + , (โ ร {๐ฅ}))โ๐) = โ
) |
98 | | ssun2 4131 |
. . . . . . . . . . . . . 14
โข (ran
๐ผ โช {โ
}) โ
((ran +
โช ๐ต) โช (ran ๐ผ โช
{โ
})) |
99 | 75, 98 | sstri 3951 |
. . . . . . . . . . . . 13
โข {โ
}
โ ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
})) |
100 | 99, 51 | sstri 3951 |
. . . . . . . . . . . 12
โข {โ
}
โ ({ 0 } โช ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
}))) |
101 | | 0ex 5262 |
. . . . . . . . . . . . 13
โข โ
โ V |
102 | 101 | snid 4620 |
. . . . . . . . . . . 12
โข โ
โ {โ
} |
103 | 100, 102 | sselii 3939 |
. . . . . . . . . . 11
โข โ
โ ({ 0 } โช ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
}))) |
104 | 103 | a1i 11 |
. . . . . . . . . 10
โข (((๐ โ โค โง ๐ฅ โ ๐ต) โง ยฌ ๐ โ (โคโฅโ1))
โ โ
โ ({ 0 } โช ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
})))) |
105 | 97, 104 | eqeltrd 2838 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ฅ โ ๐ต) โง ยฌ ๐ โ (โคโฅโ1))
โ (seq1( + , (โ ร {๐ฅ}))โ๐) โ ({ 0 } โช ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
})))) |
106 | 89, 105 | pm2.61dan 811 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ฅ โ ๐ต) โ (seq1( + , (โ ร {๐ฅ}))โ๐) โ ({ 0 } โช ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
})))) |
107 | 98, 51 | sstri 3951 |
. . . . . . . . . 10
โข (ran
๐ผ โช {โ
}) โ
({ 0 }
โช ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
}))) |
108 | | fvrn0 6869 |
. . . . . . . . . 10
โข (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)) โ (ran ๐ผ โช {โ
}) |
109 | 107, 108 | sselii 3939 |
. . . . . . . . 9
โข (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)) โ ({ 0 } โช ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
}))) |
110 | 109 | a1i 11 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ฅ โ ๐ต) โ (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)) โ ({ 0 } โช ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
})))) |
111 | 106, 110 | ifcld 4530 |
. . . . . . 7
โข ((๐ โ โค โง ๐ฅ โ ๐ต) โ if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))) โ ({ 0 } โช ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
})))) |
112 | 47, 111 | ifcld 4530 |
. . . . . 6
โข ((๐ โ โค โง ๐ฅ โ ๐ต) โ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)))) โ ({ 0 } โช ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
})))) |
113 | 112 | rgen2 3192 |
. . . . 5
โข
โ๐ โ
โค โ๐ฅ โ
๐ต if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)))) โ ({ 0 } โช ((ran + โช ๐ต) โช (ran ๐ผ โช {โ
}))) |
114 | 31, 32, 42, 113 | mpoexw 8003 |
. . . 4
โข (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) โ V |
115 | 29, 30, 114 | fvmpt 6945 |
. . 3
โข (๐บ โ V โ
(.gโ๐บ) =
(๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)))))) |
116 | | fvprc 6831 |
. . . 4
โข (ยฌ
๐บ โ V โ
(.gโ๐บ) =
โ
) |
117 | | eqid 2737 |
. . . . . . 7
โข (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) = (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) |
118 | | fvex 6852 |
. . . . . . . . 9
โข (seq1(
+ ,
(โ ร {๐ฅ}))โ๐) โ V |
119 | | fvex 6852 |
. . . . . . . . 9
โข (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)) โ V |
120 | 118, 119 | ifex 4534 |
. . . . . . . 8
โข if(0 <
๐, (seq1( + , (โ
ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))) โ V |
121 | 44, 120 | ifex 4534 |
. . . . . . 7
โข if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)))) โ V |
122 | 117, 121 | fnmpoi 7994 |
. . . . . 6
โข (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) Fn (โค ร ๐ต) |
123 | | fvprc 6831 |
. . . . . . . . . 10
โข (ยฌ
๐บ โ V โ
(Baseโ๐บ) =
โ
) |
124 | 4, 123 | eqtrid 2789 |
. . . . . . . . 9
โข (ยฌ
๐บ โ V โ ๐ต = โ
) |
125 | 124 | xpeq2d 5661 |
. . . . . . . 8
โข (ยฌ
๐บ โ V โ (โค
ร ๐ต) = (โค
ร โ
)) |
126 | | xp0 6108 |
. . . . . . . 8
โข (โค
ร โ
) = โ
|
127 | 125, 126 | eqtrdi 2793 |
. . . . . . 7
โข (ยฌ
๐บ โ V โ (โค
ร ๐ต) =
โ
) |
128 | 127 | fneq2d 6593 |
. . . . . 6
โข (ยฌ
๐บ โ V โ ((๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) Fn (โค ร ๐ต) โ (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) Fn โ
)) |
129 | 122, 128 | mpbii 232 |
. . . . 5
โข (ยฌ
๐บ โ V โ (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) Fn โ
) |
130 | | fn0 6629 |
. . . . 5
โข ((๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) Fn โ
โ (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) = โ
) |
131 | 129, 130 | sylib 217 |
. . . 4
โข (ยฌ
๐บ โ V โ (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) = โ
) |
132 | 116, 131 | eqtr4d 2780 |
. . 3
โข (ยฌ
๐บ โ V โ
(.gโ๐บ) =
(๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐)))))) |
133 | 115, 132 | pm2.61i 182 |
. 2
โข
(.gโ๐บ) = (๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) |
134 | 1, 133 | eqtri 2765 |
1
โข ยท =
(๐ โ โค, ๐ฅ โ ๐ต โฆ if(๐ = 0, 0 , if(0 < ๐, (seq1( + , (โ ร {๐ฅ}))โ๐), (๐ผโ(seq1( + , (โ ร {๐ฅ}))โ-๐))))) |