Step | Hyp | Ref
| Expression |
1 | | fvexd 6861 |
. 2
โข ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ (0gโ๐
) โ V) |
2 | | ovexd 7396 |
. 2
โข (((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โง ๐ โ โ0) โ (๐
ฮฃg
(๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) โ V) |
3 | | ply1mulgsum.p |
. . . 4
โข ๐ = (Poly1โ๐
) |
4 | | ply1mulgsum.b |
. . . 4
โข ๐ต = (Baseโ๐) |
5 | | ply1mulgsum.a |
. . . 4
โข ๐ด = (coe1โ๐พ) |
6 | | ply1mulgsum.c |
. . . 4
โข ๐ถ = (coe1โ๐ฟ) |
7 | | ply1mulgsum.x |
. . . 4
โข ๐ = (var1โ๐
) |
8 | | ply1mulgsum.pm |
. . . 4
โข ร =
(.rโ๐) |
9 | | ply1mulgsum.sm |
. . . 4
โข ยท = (
ยท๐ โ๐) |
10 | | ply1mulgsum.rm |
. . . 4
โข โ =
(.rโ๐
) |
11 | | ply1mulgsum.m |
. . . 4
โข ๐ = (mulGrpโ๐) |
12 | | ply1mulgsum.e |
. . . 4
โข โ =
(.gโ๐) |
13 | 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 | ply1mulgsumlem2 46558 |
. . 3
โข ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
))) |
14 | | vex 3451 |
. . . . . . . . 9
โข ๐ โ V |
15 | | csbov2g 7407 |
. . . . . . . . . 10
โข (๐ โ V โ
โฆ๐ / ๐โฆ(๐
ฮฃg
(๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (๐
ฮฃg
โฆ๐ / ๐โฆ(๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐)))))) |
16 | | id 22 |
. . . . . . . . . . . 12
โข (๐ โ V โ ๐ โ V) |
17 | | oveq2 7369 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ (0...๐) = (0...๐)) |
18 | | fvoveq1 7384 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ (๐ถโ(๐ โ ๐)) = (๐ถโ(๐ โ ๐))) |
19 | 18 | oveq2d 7377 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))) = ((๐ดโ๐) โ (๐ถโ(๐ โ ๐)))) |
20 | 17, 19 | mpteq12dv 5200 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐)))) = (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) |
21 | 20 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ โ V โง ๐ = ๐) โ (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐)))) = (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) |
22 | 16, 21 | csbied 3897 |
. . . . . . . . . . 11
โข (๐ โ V โ
โฆ๐ / ๐โฆ(๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐)))) = (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) |
23 | 22 | oveq2d 7377 |
. . . . . . . . . 10
โข (๐ โ V โ (๐
ฮฃg
โฆ๐ / ๐โฆ(๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐)))))) |
24 | 15, 23 | eqtrd 2773 |
. . . . . . . . 9
โข (๐ โ V โ
โฆ๐ / ๐โฆ(๐
ฮฃg
(๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐)))))) |
25 | 14, 24 | ax-mp 5 |
. . . . . . . 8
โข
โฆ๐ /
๐โฆ(๐
ฮฃg
(๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) |
26 | | simpr 486 |
. . . . . . . 8
โข
(((((๐
โ Ring
โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โง ๐ โ โ0) โง ๐ โ โ0)
โง (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
)) โ (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
)) |
27 | 25, 26 | eqtrid 2785 |
. . . . . . 7
โข
(((((๐
โ Ring
โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โง ๐ โ โ0) โง ๐ โ โ0)
โง (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
)) โ โฆ๐ / ๐โฆ(๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
)) |
28 | 27 | ex 414 |
. . . . . 6
โข ((((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โง ๐ โ โ0) โง ๐ โ โ0)
โ ((๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
) โ โฆ๐ / ๐โฆ(๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
))) |
29 | 28 | imim2d 57 |
. . . . 5
โข ((((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โง ๐ โ โ0) โง ๐ โ โ0)
โ ((๐ < ๐ โ (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
)) โ (๐ < ๐ โ โฆ๐ / ๐โฆ(๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
)))) |
30 | 29 | ralimdva 3161 |
. . . 4
โข (((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โง ๐ โ โ0) โ
(โ๐ โ
โ0 (๐ <
๐ โ (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
)) โ โ๐ โ โ0
(๐ < ๐ โ โฆ๐ / ๐โฆ(๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
)))) |
31 | 30 | reximdva 3162 |
. . 3
โข ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ (โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
)) โ โ๐ โ โ0
โ๐ โ
โ0 (๐ <
๐ โ
โฆ๐ / ๐โฆ(๐
ฮฃg
(๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
)))) |
32 | 13, 31 | mpd 15 |
. 2
โข ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ โฆ๐ / ๐โฆ(๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
))) |
33 | 1, 2, 32 | mptnn0fsupp 13911 |
1
โข ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ (๐ โ โ0 โฆ (๐
ฮฃg
(๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐)))))) finSupp (0gโ๐
)) |