Step | Hyp | Ref
| Expression |
1 | | mplbas2.s |
. . . . 5
β’ π = (πΌ mPwSer π
) |
2 | | mplbas2.i |
. . . . 5
β’ (π β πΌ β π) |
3 | | mplbas2.r |
. . . . 5
β’ (π β π
β CRing) |
4 | 1, 2, 3 | psrassa 21534 |
. . . 4
β’ (π β π β AssAlg) |
5 | | mplbas2.p |
. . . . . 6
β’ π = (πΌ mPoly π
) |
6 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
7 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
8 | 5, 1, 6, 7 | mplbasss 21556 |
. . . . 5
β’
(Baseβπ)
β (Baseβπ) |
9 | 8 | a1i 11 |
. . . 4
β’ (π β (Baseβπ) β (Baseβπ)) |
10 | | mplbas2.v |
. . . . . . . 8
β’ π = (πΌ mVar π
) |
11 | | crngring 20068 |
. . . . . . . . 9
β’ (π
β CRing β π
β Ring) |
12 | 3, 11 | syl 17 |
. . . . . . . 8
β’ (π β π
β Ring) |
13 | 1, 10, 7, 2, 12 | mvrf 21544 |
. . . . . . 7
β’ (π β π:πΌβΆ(Baseβπ)) |
14 | 13 | ffnd 6719 |
. . . . . 6
β’ (π β π Fn πΌ) |
15 | 2 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β πΌ) β πΌ β π) |
16 | 12 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β πΌ) β π
β Ring) |
17 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π₯ β πΌ) β π₯ β πΌ) |
18 | 5, 10, 6, 15, 16, 17 | mvrcl 21551 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β (πβπ₯) β (Baseβπ)) |
19 | 18 | ralrimiva 3147 |
. . . . . 6
β’ (π β βπ₯ β πΌ (πβπ₯) β (Baseβπ)) |
20 | | ffnfv 7118 |
. . . . . 6
β’ (π:πΌβΆ(Baseβπ) β (π Fn πΌ β§ βπ₯ β πΌ (πβπ₯) β (Baseβπ))) |
21 | 14, 19, 20 | sylanbrc 584 |
. . . . 5
β’ (π β π:πΌβΆ(Baseβπ)) |
22 | 21 | frnd 6726 |
. . . 4
β’ (π β ran π β (Baseβπ)) |
23 | | mplbas2.a |
. . . . 5
β’ π΄ = (AlgSpanβπ) |
24 | 23, 7 | aspss 21431 |
. . . 4
β’ ((π β AssAlg β§
(Baseβπ) β
(Baseβπ) β§ ran
π β (Baseβπ)) β (π΄βran π) β (π΄β(Baseβπ))) |
25 | 4, 9, 22, 24 | syl3anc 1372 |
. . 3
β’ (π β (π΄βran π) β (π΄β(Baseβπ))) |
26 | 1, 5, 6, 2, 12 | mplsubrg 21564 |
. . . 4
β’ (π β (Baseβπ) β (SubRingβπ)) |
27 | 1, 5, 6, 2, 12 | mpllss 21562 |
. . . 4
β’ (π β (Baseβπ) β (LSubSpβπ)) |
28 | | eqid 2733 |
. . . . 5
β’
(LSubSpβπ) =
(LSubSpβπ) |
29 | 23, 7, 28 | aspid 21429 |
. . . 4
β’ ((π β AssAlg β§
(Baseβπ) β
(SubRingβπ) β§
(Baseβπ) β
(LSubSpβπ)) β
(π΄β(Baseβπ)) = (Baseβπ)) |
30 | 4, 26, 27, 29 | syl3anc 1372 |
. . 3
β’ (π β (π΄β(Baseβπ)) = (Baseβπ)) |
31 | 25, 30 | sseqtrd 4023 |
. 2
β’ (π β (π΄βran π) β (Baseβπ)) |
32 | | eqid 2733 |
. . . 4
β’ {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
33 | | eqid 2733 |
. . . 4
β’
(0gβπ
) = (0gβπ
) |
34 | | eqid 2733 |
. . . 4
β’
(1rβπ
) = (1rβπ
) |
35 | 2 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β (Baseβπ)) β πΌ β π) |
36 | | eqid 2733 |
. . . 4
β’ (
Β·π βπ) = ( Β·π
βπ) |
37 | 12 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β (Baseβπ)) β π
β Ring) |
38 | | simpr 486 |
. . . 4
β’ ((π β§ π₯ β (Baseβπ)) β π₯ β (Baseβπ)) |
39 | 5, 32, 33, 34, 35, 6, 36, 37, 38 | mplcoe1 21592 |
. . 3
β’ ((π β§ π₯ β (Baseβπ)) β π₯ = (π Ξ£g (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ ((π₯βπ)( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
))))))) |
40 | | eqid 2733 |
. . . 4
β’
(0gβπ) = (0gβπ) |
41 | 5 | mplring 21578 |
. . . . . . 7
β’ ((πΌ β π β§ π
β Ring) β π β Ring) |
42 | 2, 12, 41 | syl2anc 585 |
. . . . . 6
β’ (π β π β Ring) |
43 | | ringabl 20098 |
. . . . . 6
β’ (π β Ring β π β Abel) |
44 | 42, 43 | syl 17 |
. . . . 5
β’ (π β π β Abel) |
45 | 44 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β (Baseβπ)) β π β Abel) |
46 | | ovex 7442 |
. . . . . 6
β’
(β0 βm πΌ) β V |
47 | 46 | rabex 5333 |
. . . . 5
β’ {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β
V |
48 | 47 | a1i 11 |
. . . 4
β’ ((π β§ π₯ β (Baseβπ)) β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β
V) |
49 | 13 | frnd 6726 |
. . . . . . . 8
β’ (π β ran π β (Baseβπ)) |
50 | 23, 7 | aspsubrg 21430 |
. . . . . . . 8
β’ ((π β AssAlg β§ ran π β (Baseβπ)) β (π΄βran π) β (SubRingβπ)) |
51 | 4, 49, 50 | syl2anc 585 |
. . . . . . 7
β’ (π β (π΄βran π) β (SubRingβπ)) |
52 | 5, 1, 6 | mplval2 21555 |
. . . . . . . . 9
β’ π = (π βΎs (Baseβπ)) |
53 | 52 | subsubrg 20345 |
. . . . . . . 8
β’
((Baseβπ)
β (SubRingβπ)
β ((π΄βran π) β (SubRingβπ) β ((π΄βran π) β (SubRingβπ) β§ (π΄βran π) β (Baseβπ)))) |
54 | 26, 53 | syl 17 |
. . . . . . 7
β’ (π β ((π΄βran π) β (SubRingβπ) β ((π΄βran π) β (SubRingβπ) β§ (π΄βran π) β (Baseβπ)))) |
55 | 51, 31, 54 | mpbir2and 712 |
. . . . . 6
β’ (π β (π΄βran π) β (SubRingβπ)) |
56 | | subrgsubg 20325 |
. . . . . 6
β’ ((π΄βran π) β (SubRingβπ) β (π΄βran π) β (SubGrpβπ)) |
57 | 55, 56 | syl 17 |
. . . . 5
β’ (π β (π΄βran π) β (SubGrpβπ)) |
58 | 57 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β (Baseβπ)) β (π΄βran π) β (SubGrpβπ)) |
59 | 5 | mpllmod 21577 |
. . . . . . . 8
β’ ((πΌ β π β§ π
β Ring) β π β LMod) |
60 | 2, 12, 59 | syl2anc 585 |
. . . . . . 7
β’ (π β π β LMod) |
61 | 60 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β π β LMod) |
62 | 23, 7, 28 | asplss 21428 |
. . . . . . . . 9
β’ ((π β AssAlg β§ ran π β (Baseβπ)) β (π΄βran π) β (LSubSpβπ)) |
63 | 4, 49, 62 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π΄βran π) β (LSubSpβπ)) |
64 | 1, 2, 12 | psrlmod 21521 |
. . . . . . . . 9
β’ (π β π β LMod) |
65 | | eqid 2733 |
. . . . . . . . . 10
β’
(LSubSpβπ) =
(LSubSpβπ) |
66 | 52, 28, 65 | lsslss 20572 |
. . . . . . . . 9
β’ ((π β LMod β§
(Baseβπ) β
(LSubSpβπ)) β
((π΄βran π) β (LSubSpβπ) β ((π΄βran π) β (LSubSpβπ) β§ (π΄βran π) β (Baseβπ)))) |
67 | 64, 27, 66 | syl2anc 585 |
. . . . . . . 8
β’ (π β ((π΄βran π) β (LSubSpβπ) β ((π΄βran π) β (LSubSpβπ) β§ (π΄βran π) β (Baseβπ)))) |
68 | 63, 31, 67 | mpbir2and 712 |
. . . . . . 7
β’ (π β (π΄βran π) β (LSubSpβπ)) |
69 | 68 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π΄βran π) β (LSubSpβπ)) |
70 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβπ
) =
(Baseβπ
) |
71 | 5, 70, 6, 32, 38 | mplelf 21557 |
. . . . . . . 8
β’ ((π β§ π₯ β (Baseβπ)) β π₯:{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ
)) |
72 | 71 | ffvelcdmda 7087 |
. . . . . . 7
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π₯βπ) β (Baseβπ
)) |
73 | 5, 35, 37 | mplsca 21572 |
. . . . . . . . 9
β’ ((π β§ π₯ β (Baseβπ)) β π
= (Scalarβπ)) |
74 | 73 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β π
= (Scalarβπ)) |
75 | 74 | fveq2d 6896 |
. . . . . . 7
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β
(Baseβπ
) =
(Baseβ(Scalarβπ))) |
76 | 72, 75 | eleqtrd 2836 |
. . . . . 6
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π₯βπ) β (Baseβ(Scalarβπ))) |
77 | 2 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β πΌ β π) |
78 | | eqid 2733 |
. . . . . . . 8
β’
(mulGrpβπ) =
(mulGrpβπ) |
79 | | eqid 2733 |
. . . . . . . 8
β’
(.gβ(mulGrpβπ)) =
(.gβ(mulGrpβπ)) |
80 | 3 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β π
β CRing) |
81 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β π β {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}) |
82 | 5, 32, 33, 34, 77, 78, 79, 10, 80, 81 | mplcoe2 21596 |
. . . . . . 7
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
))) = ((mulGrpβπ) Ξ£g (π§ β πΌ β¦ ((πβπ§)(.gβ(mulGrpβπ))(πβπ§))))) |
83 | | eqid 2733 |
. . . . . . . . 9
β’
(1rβπ) = (1rβπ) |
84 | 78, 83 | ringidval 20006 |
. . . . . . . 8
β’
(1rβπ) = (0gβ(mulGrpβπ)) |
85 | 5 | mplcrng 21580 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ π
β CRing) β π β CRing) |
86 | 2, 3, 85 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β π β CRing) |
87 | 78 | crngmgp 20064 |
. . . . . . . . . 10
β’ (π β CRing β
(mulGrpβπ) β
CMnd) |
88 | 86, 87 | syl 17 |
. . . . . . . . 9
β’ (π β (mulGrpβπ) β CMnd) |
89 | 88 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β
(mulGrpβπ) β
CMnd) |
90 | 55 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π΄βran π) β (SubRingβπ)) |
91 | 78 | subrgsubm 20332 |
. . . . . . . . 9
β’ ((π΄βran π) β (SubRingβπ) β (π΄βran π) β (SubMndβ(mulGrpβπ))) |
92 | 90, 91 | syl 17 |
. . . . . . . 8
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π΄βran π) β (SubMndβ(mulGrpβπ))) |
93 | | simplll 774 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π§ β πΌ) β π) |
94 | 32 | psrbag 21470 |
. . . . . . . . . . . . . 14
β’ (πΌ β π β (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β (π:πΌβΆβ0 β§ (β‘π β β) β
Fin))) |
95 | 35, 94 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (Baseβπ)) β (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β (π:πΌβΆβ0 β§ (β‘π β β) β
Fin))) |
96 | 95 | biimpa 478 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π:πΌβΆβ0 β§ (β‘π β β) β
Fin)) |
97 | 96 | simpld 496 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β π:πΌβΆβ0) |
98 | 97 | ffvelcdmda 7087 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π§ β πΌ) β (πβπ§) β
β0) |
99 | 23, 7 | aspssid 21432 |
. . . . . . . . . . . . 13
β’ ((π β AssAlg β§ ran π β (Baseβπ)) β ran π β (π΄βran π)) |
100 | 4, 49, 99 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β ran π β (π΄βran π)) |
101 | 100 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π§ β πΌ) β ran π β (π΄βran π)) |
102 | 14 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β π Fn πΌ) |
103 | | fnfvelrn 7083 |
. . . . . . . . . . . 12
β’ ((π Fn πΌ β§ π§ β πΌ) β (πβπ§) β ran π) |
104 | 102, 103 | sylan 581 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π§ β πΌ) β (πβπ§) β ran π) |
105 | 101, 104 | sseldd 3984 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π§ β πΌ) β (πβπ§) β (π΄βran π)) |
106 | 78, 6 | mgpbas 19993 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβ(mulGrpβπ)) |
107 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(.rβπ) = (.rβπ) |
108 | 78, 107 | mgpplusg 19991 |
. . . . . . . . . . 11
β’
(.rβπ) = (+gβ(mulGrpβπ)) |
109 | 107 | subrgmcl 20331 |
. . . . . . . . . . . 12
β’ (((π΄βran π) β (SubRingβπ) β§ π’ β (π΄βran π) β§ π£ β (π΄βran π)) β (π’(.rβπ)π£) β (π΄βran π)) |
110 | 55, 109 | syl3an1 1164 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π΄βran π) β§ π£ β (π΄βran π)) β (π’(.rβπ)π£) β (π΄βran π)) |
111 | 83 | subrg1cl 20327 |
. . . . . . . . . . . 12
β’ ((π΄βran π) β (SubRingβπ) β (1rβπ) β (π΄βran π)) |
112 | 55, 111 | syl 17 |
. . . . . . . . . . 11
β’ (π β (1rβπ) β (π΄βran π)) |
113 | 106, 79, 108, 88, 31, 110, 84, 112 | mulgnn0subcl 18967 |
. . . . . . . . . 10
β’ ((π β§ (πβπ§) β β0 β§ (πβπ§) β (π΄βran π)) β ((πβπ§)(.gβ(mulGrpβπ))(πβπ§)) β (π΄βran π)) |
114 | 93, 98, 105, 113 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π§ β πΌ) β ((πβπ§)(.gβ(mulGrpβπ))(πβπ§)) β (π΄βran π)) |
115 | 114 | fmpttd 7115 |
. . . . . . . 8
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π§ β πΌ β¦ ((πβπ§)(.gβ(mulGrpβπ))(πβπ§))):πΌβΆ(π΄βran π)) |
116 | 2 | mptexd 7226 |
. . . . . . . . . 10
β’ (π β (π§ β πΌ β¦ ((πβπ§)(.gβ(mulGrpβπ))(πβπ§))) β V) |
117 | 116 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π§ β πΌ β¦ ((πβπ§)(.gβ(mulGrpβπ))(πβπ§))) β V) |
118 | | funmpt 6587 |
. . . . . . . . . 10
β’ Fun
(π§ β πΌ β¦ ((πβπ§)(.gβ(mulGrpβπ))(πβπ§))) |
119 | 118 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β Fun
(π§ β πΌ β¦ ((πβπ§)(.gβ(mulGrpβπ))(πβπ§)))) |
120 | | fvexd 6907 |
. . . . . . . . 9
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β
(1rβπ)
β V) |
121 | 96 | simprd 497 |
. . . . . . . . 9
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (β‘π β β) β
Fin) |
122 | | elrabi 3678 |
. . . . . . . . . . . . 13
β’ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β π β (β0
βm πΌ)) |
123 | | elmapi 8843 |
. . . . . . . . . . . . . . 15
β’ (π β (β0
βm πΌ)
β π:πΌβΆβ0) |
124 | 123 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (Baseβπ)) β§ π β (β0
βm πΌ))
β π:πΌβΆβ0) |
125 | 2 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (Baseβπ)) β§ π β (β0
βm πΌ))
β πΌ β π) |
126 | | fcdmnn0supp 12528 |
. . . . . . . . . . . . . . . 16
β’ ((πΌ β π β§ π:πΌβΆβ0) β (π supp 0) = (β‘π β β)) |
127 | 125, 124,
126 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (Baseβπ)) β§ π β (β0
βm πΌ))
β (π supp 0) = (β‘π β β)) |
128 | | eqimss 4041 |
. . . . . . . . . . . . . . 15
β’ ((π supp 0) = (β‘π β β) β (π supp 0) β (β‘π β β)) |
129 | 127, 128 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (Baseβπ)) β§ π β (β0
βm πΌ))
β (π supp 0) β
(β‘π β β)) |
130 | | c0ex 11208 |
. . . . . . . . . . . . . . 15
β’ 0 β
V |
131 | 130 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (Baseβπ)) β§ π β (β0
βm πΌ))
β 0 β V) |
132 | 124, 129,
125, 131 | suppssr 8181 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β (Baseβπ)) β§ π β (β0
βm πΌ))
β§ π§ β (πΌ β (β‘π β β))) β (πβπ§) = 0) |
133 | 122, 132 | sylanl2 680 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π§ β (πΌ β (β‘π β β))) β (πβπ§) = 0) |
134 | 133 | oveq1d 7424 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π§ β (πΌ β (β‘π β β))) β ((πβπ§)(.gβ(mulGrpβπ))(πβπ§)) =
(0(.gβ(mulGrpβπ))(πβπ§))) |
135 | 2 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π§ β (πΌ β (β‘π β β))) β πΌ β π) |
136 | 12 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π§ β (πΌ β (β‘π β β))) β π
β Ring) |
137 | | eldifi 4127 |
. . . . . . . . . . . . . 14
β’ (π§ β (πΌ β (β‘π β β)) β π§ β πΌ) |
138 | 137 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π§ β (πΌ β (β‘π β β))) β π§ β πΌ) |
139 | 5, 10, 6, 135, 136, 138 | mvrcl 21551 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π§ β (πΌ β (β‘π β β))) β (πβπ§) β (Baseβπ)) |
140 | 106, 84, 79 | mulg0 18957 |
. . . . . . . . . . . 12
β’ ((πβπ§) β (Baseβπ) β
(0(.gβ(mulGrpβπ))(πβπ§)) = (1rβπ)) |
141 | 139, 140 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π§ β (πΌ β (β‘π β β))) β
(0(.gβ(mulGrpβπ))(πβπ§)) = (1rβπ)) |
142 | 134, 141 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ π§ β (πΌ β (β‘π β β))) β ((πβπ§)(.gβ(mulGrpβπ))(πβπ§)) = (1rβπ)) |
143 | 142, 77 | suppss2 8185 |
. . . . . . . . 9
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β ((π§ β πΌ β¦ ((πβπ§)(.gβ(mulGrpβπ))(πβπ§))) supp (1rβπ)) β (β‘π β β)) |
144 | | suppssfifsupp 9378 |
. . . . . . . . 9
β’ ((((π§ β πΌ β¦ ((πβπ§)(.gβ(mulGrpβπ))(πβπ§))) β V β§ Fun (π§ β πΌ β¦ ((πβπ§)(.gβ(mulGrpβπ))(πβπ§))) β§ (1rβπ) β V) β§ ((β‘π β β) β Fin β§ ((π§ β πΌ β¦ ((πβπ§)(.gβ(mulGrpβπ))(πβπ§))) supp (1rβπ)) β (β‘π β β))) β (π§ β πΌ β¦ ((πβπ§)(.gβ(mulGrpβπ))(πβπ§))) finSupp (1rβπ)) |
145 | 117, 119,
120, 121, 143, 144 | syl32anc 1379 |
. . . . . . . 8
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π§ β πΌ β¦ ((πβπ§)(.gβ(mulGrpβπ))(πβπ§))) finSupp (1rβπ)) |
146 | 84, 89, 77, 92, 115, 145 | gsumsubmcl 19787 |
. . . . . . 7
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β
((mulGrpβπ)
Ξ£g (π§ β πΌ β¦ ((πβπ§)(.gβ(mulGrpβπ))(πβπ§)))) β (π΄βran π)) |
147 | 82, 146 | eqeltrd 2834 |
. . . . . 6
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
))) β (π΄βran π)) |
148 | | eqid 2733 |
. . . . . . 7
β’
(Scalarβπ) =
(Scalarβπ) |
149 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
150 | 148, 36, 149, 65 | lssvscl 20566 |
. . . . . 6
β’ (((π β LMod β§ (π΄βran π) β (LSubSpβπ)) β§ ((π₯βπ) β (Baseβ(Scalarβπ)) β§ (π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
))) β (π΄βran π))) β ((π₯βπ)( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
)))) β (π΄βran π)) |
151 | 61, 69, 76, 147, 150 | syl22anc 838 |
. . . . 5
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β ((π₯βπ)( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
)))) β (π΄βran π)) |
152 | 151 | fmpttd 7115 |
. . . 4
β’ ((π β§ π₯ β (Baseβπ)) β (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ ((π₯βπ)( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
))))):{π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}βΆ(π΄βran π)) |
153 | 46 | mptrabex 7227 |
. . . . . . 7
β’ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ ((π₯βπ)( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
))))) β V |
154 | | funmpt 6587 |
. . . . . . 7
β’ Fun
(π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ ((π₯βπ)( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
))))) |
155 | | fvex 6905 |
. . . . . . 7
β’
(0gβπ) β V |
156 | 153, 154,
155 | 3pm3.2i 1340 |
. . . . . 6
β’ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ ((π₯βπ)( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
))))) β V β§ Fun (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ ((π₯βπ)( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
))))) β§ (0gβπ) β V) |
157 | 156 | a1i 11 |
. . . . 5
β’ ((π β§ π₯ β (Baseβπ)) β ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ ((π₯βπ)( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
))))) β V β§ Fun (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ ((π₯βπ)( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
))))) β§ (0gβπ) β V)) |
158 | 5, 1, 7, 33, 6 | mplelbas 21550 |
. . . . . . . 8
β’ (π₯ β (Baseβπ) β (π₯ β (Baseβπ) β§ π₯ finSupp (0gβπ
))) |
159 | 158 | simprbi 498 |
. . . . . . 7
β’ (π₯ β (Baseβπ) β π₯ finSupp (0gβπ
)) |
160 | 159 | adantl 483 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβπ)) β π₯ finSupp (0gβπ
)) |
161 | 160 | fsuppimpd 9369 |
. . . . 5
β’ ((π β§ π₯ β (Baseβπ)) β (π₯ supp (0gβπ
)) β Fin) |
162 | | ssidd 4006 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ)) β (π₯ supp (0gβπ
)) β (π₯ supp (0gβπ
))) |
163 | | fvexd 6907 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ)) β (0gβπ
) β V) |
164 | 71, 162, 48, 163 | suppssr 8181 |
. . . . . . . . 9
β’ (((π β§ π₯ β (Baseβπ)) β§ π β ({π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β (π₯ supp (0gβπ
)))) β (π₯βπ) = (0gβπ
)) |
165 | 73 | fveq2d 6896 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ)) β (0gβπ
) =
(0gβ(Scalarβπ))) |
166 | 165 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π₯ β (Baseβπ)) β§ π β ({π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β (π₯ supp (0gβπ
)))) β
(0gβπ
) =
(0gβ(Scalarβπ))) |
167 | 164, 166 | eqtrd 2773 |
. . . . . . . 8
β’ (((π β§ π₯ β (Baseβπ)) β§ π β ({π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β (π₯ supp (0gβπ
)))) β (π₯βπ) = (0gβ(Scalarβπ))) |
168 | 167 | oveq1d 7424 |
. . . . . . 7
β’ (((π β§ π₯ β (Baseβπ)) β§ π β ({π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β (π₯ supp (0gβπ
)))) β ((π₯βπ)( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
)))) =
((0gβ(Scalarβπ))( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
))))) |
169 | | eldifi 4127 |
. . . . . . . 8
β’ (π β ({π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β (π₯ supp (0gβπ
))) β π β {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}) |
170 | 12 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β π
β Ring) |
171 | 5, 6, 33, 34, 32, 77, 170, 81 | mplmon 21590 |
. . . . . . . . 9
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
))) β (Baseβπ)) |
172 | | eqid 2733 |
. . . . . . . . . 10
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
173 | 6, 148, 36, 172, 40 | lmod0vs 20505 |
. . . . . . . . 9
β’ ((π β LMod β§ (π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
))) β (Baseβπ)) β
((0gβ(Scalarβπ))( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
)))) = (0gβπ)) |
174 | 61, 171, 173 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π₯ β (Baseβπ)) β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β
((0gβ(Scalarβπ))( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
)))) = (0gβπ)) |
175 | 169, 174 | sylan2 594 |
. . . . . . 7
β’ (((π β§ π₯ β (Baseβπ)) β§ π β ({π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β (π₯ supp (0gβπ
)))) β
((0gβ(Scalarβπ))( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
)))) = (0gβπ)) |
176 | 168, 175 | eqtrd 2773 |
. . . . . 6
β’ (((π β§ π₯ β (Baseβπ)) β§ π β ({π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β (π₯ supp (0gβπ
)))) β ((π₯βπ)( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
)))) = (0gβπ)) |
177 | 176, 48 | suppss2 8185 |
. . . . 5
β’ ((π β§ π₯ β (Baseβπ)) β ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ ((π₯βπ)( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
))))) supp (0gβπ)) β (π₯ supp (0gβπ
))) |
178 | | suppssfifsupp 9378 |
. . . . 5
β’ ((((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ ((π₯βπ)( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
))))) β V β§ Fun (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ ((π₯βπ)( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
))))) β§ (0gβπ) β V) β§ ((π₯ supp (0gβπ
)) β Fin β§ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ ((π₯βπ)( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
))))) supp (0gβπ)) β (π₯ supp (0gβπ
)))) β (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ ((π₯βπ)( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
))))) finSupp (0gβπ)) |
179 | 157, 161,
177, 178 | syl12anc 836 |
. . . 4
β’ ((π β§ π₯ β (Baseβπ)) β (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ ((π₯βπ)( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
))))) finSupp (0gβπ)) |
180 | 40, 45, 48, 58, 152, 179 | gsumsubgcl 19788 |
. . 3
β’ ((π β§ π₯ β (Baseβπ)) β (π Ξ£g (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ ((π₯βπ)( Β·π
βπ)(π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = π, (1rβπ
), (0gβπ
)))))) β (π΄βran π)) |
181 | 39, 180 | eqeltrd 2834 |
. 2
β’ ((π β§ π₯ β (Baseβπ)) β π₯ β (π΄βran π)) |
182 | 31, 181 | eqelssd 4004 |
1
β’ (π β (π΄βran π) = (Baseβπ)) |