Step | Hyp | Ref
| Expression |
1 | | elex 2749 |
. . . . . . 7
β’ (πΊ β π β πΊ β V) |
2 | | fn0g 12794 |
. . . . . . . 8
β’
0g Fn V |
3 | | funfvex 5533 |
. . . . . . . . 9
β’ ((Fun
0g β§ πΊ
β dom 0g) β (0gβπΊ) β V) |
4 | 3 | funfni 5317 |
. . . . . . . 8
β’
((0g Fn V β§ πΊ β V) β (0gβπΊ) β V) |
5 | 2, 4 | mpan 424 |
. . . . . . 7
β’ (πΊ β V β
(0gβπΊ)
β V) |
6 | 1, 5 | syl 14 |
. . . . . 6
β’ (πΊ β π β (0gβπΊ) β V) |
7 | 6 | ad2antrr 488 |
. . . . 5
β’ (((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ π = 0) β (0gβπΊ) β V) |
8 | | nnuz 9563 |
. . . . . . . . . 10
β’ β =
(β€β₯β1) |
9 | | 1zzd 9280 |
. . . . . . . . . 10
β’ ((πΊ β π β§ π₯ β π΅) β 1 β β€) |
10 | | fvconst2g 5731 |
. . . . . . . . . . . . 13
β’ ((π₯ β π΅ β§ π’ β β) β ((β Γ
{π₯})βπ’) = π₯) |
11 | | simpl 109 |
. . . . . . . . . . . . 13
β’ ((π₯ β π΅ β§ π’ β β) β π₯ β π΅) |
12 | 10, 11 | eqeltrd 2254 |
. . . . . . . . . . . 12
β’ ((π₯ β π΅ β§ π’ β β) β ((β Γ
{π₯})βπ’) β π΅) |
13 | 12 | elexd 2751 |
. . . . . . . . . . 11
β’ ((π₯ β π΅ β§ π’ β β) β ((β Γ
{π₯})βπ’) β V) |
14 | 13 | adantll 476 |
. . . . . . . . . 10
β’ (((πΊ β π β§ π₯ β π΅) β§ π’ β β) β ((β Γ
{π₯})βπ’) β V) |
15 | | simprl 529 |
. . . . . . . . . . 11
β’ (((πΊ β π β§ π₯ β π΅) β§ (π’ β V β§ π£ β V)) β π’ β V) |
16 | | plusgslid 12571 |
. . . . . . . . . . . . 13
β’
(+g = Slot (+gβndx) β§
(+gβndx) β β) |
17 | 16 | slotex 12489 |
. . . . . . . . . . . 12
β’ (πΊ β π β (+gβπΊ) β V) |
18 | 17 | ad2antrr 488 |
. . . . . . . . . . 11
β’ (((πΊ β π β§ π₯ β π΅) β§ (π’ β V β§ π£ β V)) β (+gβπΊ) β V) |
19 | | simprr 531 |
. . . . . . . . . . 11
β’ (((πΊ β π β§ π₯ β π΅) β§ (π’ β V β§ π£ β V)) β π£ β V) |
20 | | ovexg 5909 |
. . . . . . . . . . 11
β’ ((π’ β V β§
(+gβπΊ)
β V β§ π£ β V)
β (π’(+gβπΊ)π£) β V) |
21 | 15, 18, 19, 20 | syl3anc 1238 |
. . . . . . . . . 10
β’ (((πΊ β π β§ π₯ β π΅) β§ (π’ β V β§ π£ β V)) β (π’(+gβπΊ)π£) β V) |
22 | 8, 9, 14, 21 | seqf 10461 |
. . . . . . . . 9
β’ ((πΊ β π β§ π₯ β π΅) β seq1((+gβπΊ), (β Γ {π₯})):ββΆV) |
23 | 22 | adantrl 478 |
. . . . . . . 8
β’ ((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β seq1((+gβπΊ), (β Γ {π₯})):ββΆV) |
24 | 23 | ad2antrr 488 |
. . . . . . 7
β’ ((((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β§ 0 < π) β seq1((+gβπΊ), (β Γ {π₯})):ββΆV) |
25 | | simprl 529 |
. . . . . . . . 9
β’ ((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β π β β€) |
26 | 25 | ad2antrr 488 |
. . . . . . . 8
β’ ((((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β§ 0 < π) β π β β€) |
27 | | simpr 110 |
. . . . . . . 8
β’ ((((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β§ 0 < π) β 0 < π) |
28 | | elnnz 9263 |
. . . . . . . 8
β’ (π β β β (π β β€ β§ 0 <
π)) |
29 | 26, 27, 28 | sylanbrc 417 |
. . . . . . 7
β’ ((((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β§ 0 < π) β π β β) |
30 | 24, 29 | ffvelcdmd 5653 |
. . . . . 6
β’ ((((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β§ 0 < π) β (seq1((+gβπΊ), (β Γ {π₯}))βπ) β V) |
31 | | mulgfn.b |
. . . . . . . . . 10
β’ π΅ = (BaseβπΊ) |
32 | | eqid 2177 |
. . . . . . . . . 10
β’
(invgβπΊ) = (invgβπΊ) |
33 | 31, 32 | grpinvfng 12917 |
. . . . . . . . 9
β’ (πΊ β π β (invgβπΊ) Fn π΅) |
34 | | basfn 12520 |
. . . . . . . . . . . 12
β’ Base Fn
V |
35 | | funfvex 5533 |
. . . . . . . . . . . . 13
β’ ((Fun
Base β§ πΊ β dom
Base) β (BaseβπΊ)
β V) |
36 | 35 | funfni 5317 |
. . . . . . . . . . . 12
β’ ((Base Fn
V β§ πΊ β V) β
(BaseβπΊ) β
V) |
37 | 34, 36 | mpan 424 |
. . . . . . . . . . 11
β’ (πΊ β V β
(BaseβπΊ) β
V) |
38 | 31, 37 | eqeltrid 2264 |
. . . . . . . . . 10
β’ (πΊ β V β π΅ β V) |
39 | 1, 38 | syl 14 |
. . . . . . . . 9
β’ (πΊ β π β π΅ β V) |
40 | | fnex 5739 |
. . . . . . . . 9
β’
(((invgβπΊ) Fn π΅ β§ π΅ β V) β
(invgβπΊ)
β V) |
41 | 33, 39, 40 | syl2anc 411 |
. . . . . . . 8
β’ (πΊ β π β (invgβπΊ) β V) |
42 | 41 | ad3antrrr 492 |
. . . . . . 7
β’ ((((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β (invgβπΊ) β V) |
43 | 23 | ad2antrr 488 |
. . . . . . . 8
β’ ((((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β seq1((+gβπΊ), (β Γ {π₯})):ββΆV) |
44 | 25 | znegcld 9377 |
. . . . . . . . . 10
β’ ((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β -π β β€) |
45 | 44 | ad2antrr 488 |
. . . . . . . . 9
β’ ((((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β -π β β€) |
46 | | simplr 528 |
. . . . . . . . . . 11
β’ ((((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β Β¬ π = 0) |
47 | | simpr 110 |
. . . . . . . . . . 11
β’ ((((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β Β¬ 0 < π) |
48 | | ztri3or0 9295 |
. . . . . . . . . . . . 13
β’ (π β β€ β (π < 0 β¨ π = 0 β¨ 0 < π)) |
49 | 25, 48 | syl 14 |
. . . . . . . . . . . 12
β’ ((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β (π < 0 β¨ π = 0 β¨ 0 < π)) |
50 | 49 | ad2antrr 488 |
. . . . . . . . . . 11
β’ ((((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β (π < 0 β¨ π = 0 β¨ 0 < π)) |
51 | 46, 47, 50 | ecase23d 1350 |
. . . . . . . . . 10
β’ ((((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β π < 0) |
52 | 25 | zred 9375 |
. . . . . . . . . . . 12
β’ ((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β π β β) |
53 | 52 | ad2antrr 488 |
. . . . . . . . . . 11
β’ ((((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β π β β) |
54 | 53 | lt0neg1d 8472 |
. . . . . . . . . 10
β’ ((((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β (π < 0 β 0 < -π)) |
55 | 51, 54 | mpbid 147 |
. . . . . . . . 9
β’ ((((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β 0 < -π) |
56 | | elnnz 9263 |
. . . . . . . . 9
β’ (-π β β β (-π β β€ β§ 0 <
-π)) |
57 | 45, 55, 56 | sylanbrc 417 |
. . . . . . . 8
β’ ((((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β -π β β) |
58 | 43, 57 | ffvelcdmd 5653 |
. . . . . . 7
β’ ((((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β (seq1((+gβπΊ), (β Γ {π₯}))β-π) β V) |
59 | | fvexg 5535 |
. . . . . . 7
β’
(((invgβπΊ) β V β§
(seq1((+gβπΊ), (β Γ {π₯}))β-π) β V) β
((invgβπΊ)β(seq1((+gβπΊ), (β Γ {π₯}))β-π)) β V) |
60 | 42, 58, 59 | syl2anc 411 |
. . . . . 6
β’ ((((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β ((invgβπΊ)β(seq1((+gβπΊ), (β Γ {π₯}))β-π)) β V) |
61 | | 0zd 9265 |
. . . . . . 7
β’ (((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β 0 β
β€) |
62 | | simplrl 535 |
. . . . . . 7
β’ (((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β π β β€) |
63 | | zdclt 9330 |
. . . . . . 7
β’ ((0
β β€ β§ π
β β€) β DECID 0 < π) |
64 | 61, 62, 63 | syl2anc 411 |
. . . . . 6
β’ (((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β DECID 0 <
π) |
65 | 30, 60, 64 | ifcldadc 3564 |
. . . . 5
β’ (((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β§ Β¬ π = 0) β if(0 < π, (seq1((+gβπΊ), (β Γ {π₯}))βπ), ((invgβπΊ)β(seq1((+gβπΊ), (β Γ {π₯}))β-π))) β V) |
66 | | 0zd 9265 |
. . . . . 6
β’ ((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β 0 β β€) |
67 | | zdceq 9328 |
. . . . . 6
β’ ((π β β€ β§ 0 β
β€) β DECID π = 0) |
68 | 25, 66, 67 | syl2anc 411 |
. . . . 5
β’ ((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β DECID π = 0) |
69 | 7, 65, 68 | ifcldadc 3564 |
. . . 4
β’ ((πΊ β π β§ (π β β€ β§ π₯ β π΅)) β if(π = 0, (0gβπΊ), if(0 < π, (seq1((+gβπΊ), (β Γ {π₯}))βπ), ((invgβπΊ)β(seq1((+gβπΊ), (β Γ {π₯}))β-π)))) β V) |
70 | 69 | ralrimivva 2559 |
. . 3
β’ (πΊ β π β βπ β β€ βπ₯ β π΅ if(π = 0, (0gβπΊ), if(0 < π, (seq1((+gβπΊ), (β Γ {π₯}))βπ), ((invgβπΊ)β(seq1((+gβπΊ), (β Γ {π₯}))β-π)))) β V) |
71 | | eqid 2177 |
. . . 4
β’ (π β β€, π₯ β π΅ β¦ if(π = 0, (0gβπΊ), if(0 < π, (seq1((+gβπΊ), (β Γ {π₯}))βπ), ((invgβπΊ)β(seq1((+gβπΊ), (β Γ {π₯}))β-π))))) = (π β β€, π₯ β π΅ β¦ if(π = 0, (0gβπΊ), if(0 < π, (seq1((+gβπΊ), (β Γ {π₯}))βπ), ((invgβπΊ)β(seq1((+gβπΊ), (β Γ {π₯}))β-π))))) |
72 | 71 | fnmpo 6203 |
. . 3
β’
(βπ β
β€ βπ₯ β
π΅ if(π = 0, (0gβπΊ), if(0 < π, (seq1((+gβπΊ), (β Γ {π₯}))βπ), ((invgβπΊ)β(seq1((+gβπΊ), (β Γ {π₯}))β-π)))) β V β (π β β€, π₯ β π΅ β¦ if(π = 0, (0gβπΊ), if(0 < π, (seq1((+gβπΊ), (β Γ {π₯}))βπ), ((invgβπΊ)β(seq1((+gβπΊ), (β Γ {π₯}))β-π))))) Fn (β€ Γ π΅)) |
73 | 70, 72 | syl 14 |
. 2
β’ (πΊ β π β (π β β€, π₯ β π΅ β¦ if(π = 0, (0gβπΊ), if(0 < π, (seq1((+gβπΊ), (β Γ {π₯}))βπ), ((invgβπΊ)β(seq1((+gβπΊ), (β Γ {π₯}))β-π))))) Fn (β€ Γ π΅)) |
74 | | eqid 2177 |
. . . 4
β’
(+gβπΊ) = (+gβπΊ) |
75 | | eqid 2177 |
. . . 4
β’
(0gβπΊ) = (0gβπΊ) |
76 | | mulgfn.t |
. . . 4
β’ Β· =
(.gβπΊ) |
77 | 31, 74, 75, 32, 76 | mulgfvalg 12985 |
. . 3
β’ (πΊ β π β Β· = (π β β€, π₯ β π΅ β¦ if(π = 0, (0gβπΊ), if(0 < π, (seq1((+gβπΊ), (β Γ {π₯}))βπ), ((invgβπΊ)β(seq1((+gβπΊ), (β Γ {π₯}))β-π)))))) |
78 | 77 | fneq1d 5307 |
. 2
β’ (πΊ β π β ( Β· Fn (β€ Γ
π΅) β (π β β€, π₯ β π΅ β¦ if(π = 0, (0gβπΊ), if(0 < π, (seq1((+gβπΊ), (β Γ {π₯}))βπ), ((invgβπΊ)β(seq1((+gβπΊ), (β Γ {π₯}))β-π))))) Fn (β€ Γ π΅))) |
79 | 73, 78 | mpbird 167 |
1
β’ (πΊ β π β Β· Fn (β€ Γ
π΅)) |