Step |
Hyp |
Ref |
Expression |
1 |
|
mply1topmat.a |
โข ๐ด = ( ๐ Mat ๐
) |
2 |
|
mply1topmat.q |
โข ๐ = ( Poly1 โ ๐ด ) |
3 |
|
mply1topmat.l |
โข ๐ฟ = ( Base โ ๐ ) |
4 |
|
mply1topmat.p |
โข ๐ = ( Poly1 โ ๐
) |
5 |
|
mply1topmat.m |
โข ยท = ( ยท๐ โ ๐ ) |
6 |
|
mply1topmat.e |
โข ๐ธ = ( .g โ ( mulGrp โ ๐ ) ) |
7 |
|
mply1topmat.y |
โข ๐ = ( var1 โ ๐
) |
8 |
|
nn0ex |
โข โ0 โ V |
9 |
8
|
a1i |
โข ( ( ( ๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ฟ ) โง ๐ผ โ ๐ โง ๐ฝ โ ๐ ) โ โ0 โ V ) |
10 |
4
|
ply1lmod |
โข ( ๐
โ Ring โ ๐ โ LMod ) |
11 |
10
|
3ad2ant2 |
โข ( ( ๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ฟ ) โ ๐ โ LMod ) |
12 |
11
|
3ad2ant1 |
โข ( ( ( ๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ฟ ) โง ๐ผ โ ๐ โง ๐ฝ โ ๐ ) โ ๐ โ LMod ) |
13 |
|
simp12 |
โข ( ( ( ๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ฟ ) โง ๐ผ โ ๐ โง ๐ฝ โ ๐ ) โ ๐
โ Ring ) |
14 |
4
|
ply1sca |
โข ( ๐
โ Ring โ ๐
= ( Scalar โ ๐ ) ) |
15 |
13 14
|
syl |
โข ( ( ( ๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ฟ ) โง ๐ผ โ ๐ โง ๐ฝ โ ๐ ) โ ๐
= ( Scalar โ ๐ ) ) |
16 |
|
eqid |
โข ( Base โ ๐ ) = ( Base โ ๐ ) |
17 |
|
ovexd |
โข ( ( ( ( ๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ฟ ) โง ๐ผ โ ๐ โง ๐ฝ โ ๐ ) โง ๐ โ โ0 ) โ ( ๐ผ ( ( coe1 โ ๐ ) โ ๐ ) ๐ฝ ) โ V ) |
18 |
|
eqid |
โข ( mulGrp โ ๐ ) = ( mulGrp โ ๐ ) |
19 |
18 16
|
mgpbas |
โข ( Base โ ๐ ) = ( Base โ ( mulGrp โ ๐ ) ) |
20 |
4
|
ply1ring |
โข ( ๐
โ Ring โ ๐ โ Ring ) |
21 |
18
|
ringmgp |
โข ( ๐ โ Ring โ ( mulGrp โ ๐ ) โ Mnd ) |
22 |
20 21
|
syl |
โข ( ๐
โ Ring โ ( mulGrp โ ๐ ) โ Mnd ) |
23 |
22
|
3ad2ant2 |
โข ( ( ๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ฟ ) โ ( mulGrp โ ๐ ) โ Mnd ) |
24 |
23
|
3ad2ant1 |
โข ( ( ( ๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ฟ ) โง ๐ผ โ ๐ โง ๐ฝ โ ๐ ) โ ( mulGrp โ ๐ ) โ Mnd ) |
25 |
24
|
adantr |
โข ( ( ( ( ๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ฟ ) โง ๐ผ โ ๐ โง ๐ฝ โ ๐ ) โง ๐ โ โ0 ) โ ( mulGrp โ ๐ ) โ Mnd ) |
26 |
|
simpr |
โข ( ( ( ( ๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ฟ ) โง ๐ผ โ ๐ โง ๐ฝ โ ๐ ) โง ๐ โ โ0 ) โ ๐ โ โ0 ) |
27 |
7 4 16
|
vr1cl |
โข ( ๐
โ Ring โ ๐ โ ( Base โ ๐ ) ) |
28 |
27
|
3ad2ant2 |
โข ( ( ๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ฟ ) โ ๐ โ ( Base โ ๐ ) ) |
29 |
28
|
3ad2ant1 |
โข ( ( ( ๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ฟ ) โง ๐ผ โ ๐ โง ๐ฝ โ ๐ ) โ ๐ โ ( Base โ ๐ ) ) |
30 |
29
|
adantr |
โข ( ( ( ( ๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ฟ ) โง ๐ผ โ ๐ โง ๐ฝ โ ๐ ) โง ๐ โ โ0 ) โ ๐ โ ( Base โ ๐ ) ) |
31 |
19 6 25 26 30
|
mulgnn0cld |
โข ( ( ( ( ๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ฟ ) โง ๐ผ โ ๐ โง ๐ฝ โ ๐ ) โง ๐ โ โ0 ) โ ( ๐ ๐ธ ๐ ) โ ( Base โ ๐ ) ) |
32 |
|
eqid |
โข ( 0g โ ๐ ) = ( 0g โ ๐ ) |
33 |
|
eqid |
โข ( 0g โ ๐
) = ( 0g โ ๐
) |
34 |
1 2 3
|
mptcoe1matfsupp |
โข ( ( ( ๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ฟ ) โง ๐ผ โ ๐ โง ๐ฝ โ ๐ ) โ ( ๐ โ โ0 โฆ ( ๐ผ ( ( coe1 โ ๐ ) โ ๐ ) ๐ฝ ) ) finSupp ( 0g โ ๐
) ) |
35 |
9 12 15 16 17 31 32 33 5 34
|
mptscmfsupp0 |
โข ( ( ( ๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ฟ ) โง ๐ผ โ ๐ โง ๐ฝ โ ๐ ) โ ( ๐ โ โ0 โฆ ( ( ๐ผ ( ( coe1 โ ๐ ) โ ๐ ) ๐ฝ ) ยท ( ๐ ๐ธ ๐ ) ) ) finSupp ( 0g โ ๐ ) ) |