Step | Hyp | Ref
| Expression |
1 | | rrxval.r |
. . 3
β’ π» = (β^βπΌ) |
2 | 1 | rrxval 24904 |
. 2
β’ (πΌ β π β π» =
(toβPreHilβ(βfld freeLMod πΌ))) |
3 | | eqid 2733 |
. . 3
β’
(toβPreHilβ(βfld freeLMod πΌ)) =
(toβPreHilβ(βfld freeLMod πΌ)) |
4 | | eqid 2733 |
. . 3
β’
(Baseβ(βfld freeLMod πΌ)) = (Baseβ(βfld
freeLMod πΌ)) |
5 | | eqid 2733 |
. . 3
β’
(Scalarβ(βfld freeLMod πΌ)) = (Scalarβ(βfld
freeLMod πΌ)) |
6 | | eqid 2733 |
. . . 4
β’
(βfld freeLMod πΌ) = (βfld freeLMod πΌ) |
7 | | rebase 21159 |
. . . 4
β’ β =
(Baseββfld) |
8 | | remulr 21164 |
. . . 4
β’ Β·
= (.rββfld) |
9 | | eqid 2733 |
. . . 4
β’
(Β·πβ(βfld
freeLMod πΌ)) =
(Β·πβ(βfld freeLMod
πΌ)) |
10 | | eqid 2733 |
. . . 4
β’
(0gβ(βfld freeLMod πΌ)) =
(0gβ(βfld freeLMod πΌ)) |
11 | | re0g 21165 |
. . . 4
β’ 0 =
(0gββfld) |
12 | | refldcj 21173 |
. . . 4
β’ β
= (*πββfld) |
13 | | refld 21172 |
. . . . 5
β’
βfld β Field |
14 | 13 | a1i 11 |
. . . 4
β’ (πΌ β π β βfld β
Field) |
15 | | fconstmpt 5739 |
. . . . 5
β’ (πΌ Γ {0}) = (π₯ β πΌ β¦ 0) |
16 | 6, 7, 4 | frlmbasf 21315 |
. . . . . . . 8
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β π:πΌβΆβ) |
17 | 16 | ffnd 6719 |
. . . . . . 7
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β π Fn πΌ) |
18 | 17 | 3adant3 1133 |
. . . . . 6
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β π Fn πΌ) |
19 | | simpl 484 |
. . . . . . . . . . . . . . . . 17
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β πΌ β π) |
20 | 13 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β
βfld β Field) |
21 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β π β
(Baseβ(βfld freeLMod πΌ))) |
22 | 6, 7, 8, 4, 9 | frlmipval 21334 |
. . . . . . . . . . . . . . . . 17
β’ (((πΌ β π β§ βfld β Field)
β§ (π β
(Baseβ(βfld freeLMod πΌ)) β§ π β (Baseβ(βfld
freeLMod πΌ)))) β
(π(Β·πβ(βfld
freeLMod πΌ))π) = (βfld Ξ£g (π βf Β· π))) |
23 | 19, 20, 21, 21, 22 | syl22anc 838 |
. . . . . . . . . . . . . . . 16
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β (π(Β·πβ(βfld
freeLMod πΌ))π) = (βfld Ξ£g (π βf Β· π))) |
24 | | inidm 4219 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΌ β© πΌ) = πΌ |
25 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β§ π₯ β πΌ) β (πβπ₯) = (πβπ₯)) |
26 | 17, 17, 19, 19, 24, 25, 25 | offval 7679 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β (π βf Β·
π) = (π₯ β πΌ β¦ ((πβπ₯) Β· (πβπ₯)))) |
27 | 16 | ffvelcdmda 7087 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β§ π₯ β πΌ) β (πβπ₯) β β) |
28 | 27, 27 | remulcld 11244 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β§ π₯ β πΌ) β ((πβπ₯) Β· (πβπ₯)) β β) |
29 | 26, 28 | fmpt3d 7116 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β (π βf Β·
π):πΌβΆβ) |
30 | | ovexd 7444 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β (π βf Β·
π) β
V) |
31 | 29 | ffund 6722 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β Fun
(π βf
Β· π)) |
32 | 6, 11, 4 | frlmbasfsupp 21313 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β π finSupp 0) |
33 | | 0red 11217 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β 0
β β) |
34 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β§ π₯ β β) β π₯ β
β) |
35 | 34 | recnd 11242 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β§ π₯ β β) β π₯ β
β) |
36 | 35 | mul02d 11412 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β§ π₯ β β) β (0
Β· π₯) =
0) |
37 | 19, 33, 16, 16, 36 | suppofss1d 8189 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β
((π βf
Β· π) supp 0) β
(π supp
0)) |
38 | | fsuppsssupp 9379 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π βf Β·
π) β V β§ Fun
(π βf
Β· π)) β§ (π finSupp 0 β§ ((π βf Β·
π) supp 0) β (π supp 0))) β (π βf Β·
π) finSupp
0) |
39 | 30, 31, 32, 37, 38 | syl22anc 838 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β (π βf Β·
π) finSupp
0) |
40 | | regsumsupp 21175 |
. . . . . . . . . . . . . . . . . 18
β’ (((π βf Β·
π):πΌβΆβ β§ (π βf Β· π) finSupp 0 β§ πΌ β π) β (βfld
Ξ£g (π βf Β· π)) = Ξ£π₯ β ((π βf Β· π) supp 0)((π βf Β· π)βπ₯)) |
41 | 29, 39, 19, 40 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β
(βfld Ξ£g (π βf Β· π)) = Ξ£π₯ β ((π βf Β· π) supp 0)((π βf Β· π)βπ₯)) |
42 | | suppssdm 8162 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π supp 0) β dom π |
43 | 42, 16 | fssdm 6738 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β (π supp 0) β πΌ) |
44 | 37, 43 | sstrd 3993 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β
((π βf
Β· π) supp 0) β
πΌ) |
45 | 44 | sselda 3983 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β§ π₯ β ((π βf Β· π) supp 0)) β π₯ β πΌ) |
46 | 17, 17, 19, 19, 24, 25, 25 | ofval 7681 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β§ π₯ β πΌ) β ((π βf Β· π)βπ₯) = ((πβπ₯) Β· (πβπ₯))) |
47 | 45, 46 | syldan 592 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β§ π₯ β ((π βf Β· π) supp 0)) β ((π βf Β·
π)βπ₯) = ((πβπ₯) Β· (πβπ₯))) |
48 | 47 | sumeq2dv 15649 |
. . . . . . . . . . . . . . . . 17
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β
Ξ£π₯ β ((π βf Β·
π) supp 0)((π βf Β·
π)βπ₯) = Ξ£π₯ β ((π βf Β· π) supp 0)((πβπ₯) Β· (πβπ₯))) |
49 | 41, 48 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β
(βfld Ξ£g (π βf Β· π)) = Ξ£π₯ β ((π βf Β· π) supp 0)((πβπ₯) Β· (πβπ₯))) |
50 | 23, 49 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β (π(Β·πβ(βfld
freeLMod πΌ))π) = Ξ£π₯
β ((π βf Β· π) supp 0)((πβπ₯)
Β· (πβπ₯))) |
51 | 50 | 3adant3 1133 |
. . . . . . . . . . . . . 14
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β (π(Β·πβ(βfld
freeLMod πΌ))π) = Ξ£π₯
β ((π βf Β· π) supp 0)((πβπ₯)
Β· (πβπ₯))) |
52 | | simp3 1139 |
. . . . . . . . . . . . . 14
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) |
53 | 51, 52 | eqtr3d 2775 |
. . . . . . . . . . . . 13
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β Ξ£π₯ β ((π
βf Β· π) supp 0)((πβπ₯) Β· (πβπ₯)) =
0) |
54 | 32 | fsuppimpd 9369 |
. . . . . . . . . . . . . . . 16
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β (π supp 0) β
Fin) |
55 | 54, 37 | ssfid 9267 |
. . . . . . . . . . . . . . 15
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β
((π βf
Β· π) supp 0) β
Fin) |
56 | 45, 28 | syldan 592 |
. . . . . . . . . . . . . . 15
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β§ π₯ β ((π βf Β· π) supp 0)) β ((πβπ₯) Β· (πβπ₯)) β β) |
57 | 27 | msqge0d 11782 |
. . . . . . . . . . . . . . . 16
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β§ π₯ β πΌ) β 0 β€ ((πβπ₯) Β· (πβπ₯))) |
58 | 45, 57 | syldan 592 |
. . . . . . . . . . . . . . 15
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β§ π₯ β ((π βf Β· π) supp 0)) β 0 β€ ((πβπ₯) Β· (πβπ₯))) |
59 | 55, 56, 58 | fsum00 15744 |
. . . . . . . . . . . . . 14
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β
(Ξ£π₯ β ((π βf Β·
π) supp 0)((πβπ₯) Β· (πβπ₯)) = 0 β βπ₯ β ((π βf Β· π) supp 0)((πβπ₯) Β· (πβπ₯)) = 0)) |
60 | 59 | 3adant3 1133 |
. . . . . . . . . . . . 13
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β (Ξ£π₯ β ((π
βf Β· π) supp 0)((πβπ₯) Β· (πβπ₯)) =
0 β βπ₯ β ((π βf Β· π) supp 0)((πβπ₯)
Β· (πβπ₯)) = 0)) |
61 | 53, 60 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β βπ₯ β ((π
βf Β· π) supp 0)((πβπ₯) Β· (πβπ₯)) =
0) |
62 | 61 | r19.21bi 3249 |
. . . . . . . . . . 11
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β ((π
βf Β· π) supp 0)) β
((πβπ₯) Β· (πβπ₯)) =
0) |
63 | 62 | adantlr 714 |
. . . . . . . . . 10
β’ ((((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β§ π₯ β ((π βf Β· π) supp 0)) β ((πβπ₯)
Β· (πβπ₯)) = 0) |
64 | 27 | 3adantl3 1169 |
. . . . . . . . . . . . 13
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β (πβπ₯) β β) |
65 | 64 | recnd 11242 |
. . . . . . . . . . . 12
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β (πβπ₯) β β) |
66 | 65, 65 | mul0ord 11864 |
. . . . . . . . . . 11
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β (((πβπ₯) Β· (πβπ₯)) =
0 β ((πβπ₯) = 0 β¨ (πβπ₯) =
0))) |
67 | 66 | adantr 482 |
. . . . . . . . . 10
β’ ((((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β§ π₯ β ((π βf Β· π) supp 0)) β (((πβπ₯)
Β· (πβπ₯)) = 0 β ((πβπ₯) = 0
β¨ (πβπ₯) = 0))) |
68 | 63, 67 | mpbid 231 |
. . . . . . . . 9
β’ ((((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β§ π₯ β ((π βf Β· π) supp 0)) β ((πβπ₯) = 0
β¨ (πβπ₯) = 0)) |
69 | | oridm 904 |
. . . . . . . . 9
β’ (((πβπ₯) = 0 β¨ (πβπ₯) = 0) β (πβπ₯) = 0) |
70 | 68, 69 | sylib 217 |
. . . . . . . 8
β’ ((((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β§ π₯ β ((π βf Β· π) supp 0)) β (πβπ₯) =
0) |
71 | 29 | 3adant3 1133 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β (π βf Β· π):πΌβΆβ) |
72 | 71 | adantr 482 |
. . . . . . . . . 10
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β (π βf Β· π):πΌβΆβ) |
73 | | ssidd 4006 |
. . . . . . . . . 10
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β ((π βf Β· π) supp 0) β ((π βf Β· π) supp 0)) |
74 | | simpl1 1192 |
. . . . . . . . . 10
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β πΌ β π) |
75 | | 0red 11217 |
. . . . . . . . . 10
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β 0 β β) |
76 | 72, 73, 74, 75 | suppssr 8181 |
. . . . . . . . 9
β’ ((((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β§ π₯ β (πΌ β ((π
βf Β· π) supp 0)))
β ((π βf Β· π)βπ₯) = 0) |
77 | 46 | 3adantl3 1169 |
. . . . . . . . . . . . 13
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β ((π βf Β· π)βπ₯) = ((πβπ₯)
Β· (πβπ₯))) |
78 | 77 | eqeq1d 2735 |
. . . . . . . . . . . 12
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β (((π βf Β· π)βπ₯) = 0 β ((πβπ₯)
Β· (πβπ₯)) = 0)) |
79 | 78, 66 | bitrd 279 |
. . . . . . . . . . 11
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β (((π βf Β· π)βπ₯) = 0 β ((πβπ₯) = 0
β¨ (πβπ₯) = 0))) |
80 | 79, 69 | bitrdi 287 |
. . . . . . . . . 10
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β (((π βf Β· π)βπ₯) = 0 β (πβπ₯) =
0)) |
81 | 80 | biimpa 478 |
. . . . . . . . 9
β’ ((((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β§ ((π βf Β· π)βπ₯) = 0) β (πβπ₯) =
0) |
82 | 76, 81 | syldan 592 |
. . . . . . . 8
β’ ((((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β§ π₯ β (πΌ β ((π
βf Β· π) supp 0)))
β (πβπ₯) = 0) |
83 | | undif 4482 |
. . . . . . . . . . . . 13
β’ (((π βf Β·
π) supp 0) β πΌ β (((π βf Β· π) supp 0) βͺ (πΌ β ((π βf Β· π) supp 0))) = πΌ) |
84 | 44, 83 | sylib 217 |
. . . . . . . . . . . 12
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β
(((π βf
Β· π) supp 0) βͺ
(πΌ β ((π βf Β·
π) supp 0))) = πΌ) |
85 | 84 | eleq2d 2820 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β (π₯ β (((π βf Β· π) supp 0) βͺ (πΌ β ((π βf Β· π) supp 0))) β π₯ β πΌ)) |
86 | 85 | 3adant3 1133 |
. . . . . . . . . 10
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β (π₯ β (((π
βf Β· π) supp 0) βͺ
(πΌ β ((π βf Β· π) supp 0))) β π₯ β πΌ)) |
87 | 86 | biimpar 479 |
. . . . . . . . 9
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β π₯ β (((π βf Β· π) supp 0) βͺ (πΌ β ((π
βf Β· π) supp
0)))) |
88 | | elun 4149 |
. . . . . . . . 9
β’ (π₯ β (((π βf Β· π) supp 0) βͺ (πΌ β ((π βf Β· π) supp 0))) β (π₯ β ((π βf Β· π) supp 0) β¨ π₯ β (πΌ β ((π βf Β· π) supp 0)))) |
89 | 87, 88 | sylib 217 |
. . . . . . . 8
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β (π₯ β ((π βf Β· π) supp 0) β¨ π₯ β (πΌ
β ((π βf Β· π) supp 0)))) |
90 | 70, 82, 89 | mpjaodan 958 |
. . . . . . 7
β’ (((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β§ π₯ β πΌ)
β (πβπ₯) = 0) |
91 | 90 | ralrimiva 3147 |
. . . . . 6
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β βπ₯ β πΌ
(πβπ₯) = 0) |
92 | | fconstfv 7214 |
. . . . . . 7
β’ (π:πΌβΆ{0} β (π Fn πΌ β§ βπ₯ β πΌ (πβπ₯) = 0)) |
93 | | c0ex 11208 |
. . . . . . . 8
β’ 0 β
V |
94 | 93 | fconst2 7206 |
. . . . . . 7
β’ (π:πΌβΆ{0} β π = (πΌ Γ {0})) |
95 | 92, 94 | sylbb1 236 |
. . . . . 6
β’ ((π Fn πΌ β§ βπ₯ β πΌ (πβπ₯) = 0) β π = (πΌ Γ {0})) |
96 | 18, 91, 95 | syl2anc 585 |
. . . . 5
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β π = (πΌ Γ
{0})) |
97 | | isfld 20368 |
. . . . . . . . . . 11
β’
(βfld β Field β (βfld β
DivRing β§ βfld β CRing)) |
98 | 13, 97 | mpbi 229 |
. . . . . . . . . 10
β’
(βfld β DivRing β§ βfld β
CRing) |
99 | 98 | simpli 485 |
. . . . . . . . 9
β’
βfld β DivRing |
100 | | drngring 20364 |
. . . . . . . . 9
β’
(βfld β DivRing β βfld
β Ring) |
101 | 99, 100 | ax-mp 5 |
. . . . . . . 8
β’
βfld β Ring |
102 | 6, 11 | frlm0 21309 |
. . . . . . . 8
β’
((βfld β Ring β§ πΌ β π) β (πΌ Γ {0}) =
(0gβ(βfld freeLMod πΌ))) |
103 | 101, 102 | mpan 689 |
. . . . . . 7
β’ (πΌ β π β (πΌ Γ {0}) =
(0gβ(βfld freeLMod πΌ))) |
104 | 103, 15 | eqtr3di 2788 |
. . . . . 6
β’ (πΌ β π β
(0gβ(βfld freeLMod πΌ)) = (π₯ β πΌ β¦ 0)) |
105 | 104 | 3ad2ant1 1134 |
. . . . 5
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β (0gβ(βfld
freeLMod πΌ)) = (π₯ β πΌ
β¦ 0)) |
106 | 15, 96, 105 | 3eqtr4a 2799 |
. . . 4
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ)) β§ (π(Β·πβ(βfld
freeLMod πΌ))π) = 0) β π = (0gβ(βfld freeLMod πΌ))) |
107 | | cjre 15086 |
. . . . 5
β’ (π₯ β β β
(ββπ₯) = π₯) |
108 | 107 | adantl 483 |
. . . 4
β’ ((πΌ β π β§ π₯ β β) β (ββπ₯) = π₯) |
109 | | id 22 |
. . . 4
β’ (πΌ β π β πΌ β π) |
110 | 6, 7, 8, 4, 9, 10,
11, 12, 14, 106, 108, 109 | frlmphl 21336 |
. . 3
β’ (πΌ β π β (βfld freeLMod
πΌ) β
PreHil) |
111 | 6 | frlmsca 21308 |
. . . . 5
β’
((βfld β Field β§ πΌ β π) β βfld =
(Scalarβ(βfld freeLMod πΌ))) |
112 | 13, 111 | mpan 689 |
. . . 4
β’ (πΌ β π β βfld =
(Scalarβ(βfld freeLMod πΌ))) |
113 | | df-refld 21158 |
. . . 4
β’
βfld = (βfld βΎs
β) |
114 | 112, 113 | eqtr3di 2788 |
. . 3
β’ (πΌ β π β (Scalarβ(βfld
freeLMod πΌ)) =
(βfld βΎs β)) |
115 | | simpr1 1195 |
. . . 4
β’ ((πΌ β π β§ (π β β β§ π β β β§ 0 β€ π)) β π β β) |
116 | | simpr3 1197 |
. . . 4
β’ ((πΌ β π β§ (π β β β§ π β β β§ 0 β€ π)) β 0 β€ π) |
117 | 115, 116 | resqrtcld 15364 |
. . 3
β’ ((πΌ β π β§ (π β β β§ π β β β§ 0 β€ π)) β (ββπ) β
β) |
118 | 55, 56, 58 | fsumge0 15741 |
. . . . 5
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β 0 β€
Ξ£π₯ β ((π βf Β·
π) supp 0)((πβπ₯) Β· (πβπ₯))) |
119 | 118, 49 | breqtrrd 5177 |
. . . 4
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β 0 β€
(βfld Ξ£g (π βf Β· π))) |
120 | 119, 23 | breqtrrd 5177 |
. . 3
β’ ((πΌ β π β§ π β (Baseβ(βfld
freeLMod πΌ))) β 0 β€
(π(Β·πβ(βfld
freeLMod πΌ))π)) |
121 | 3, 4, 5, 110, 114, 9, 117, 120 | tcphcph 24754 |
. 2
β’ (πΌ β π β
(toβPreHilβ(βfld freeLMod πΌ)) β βPreHil) |
122 | 2, 121 | eqeltrd 2834 |
1
β’ (πΌ β π β π» β βPreHil) |