Step | Hyp | Ref
| Expression |
1 | | frlmlbs.u |
. . . 4
β’ π = (π
unitVec πΌ) |
2 | | frlmlbs.f |
. . . 4
β’ πΉ = (π
freeLMod πΌ) |
3 | | eqid 2733 |
. . . 4
β’
(BaseβπΉ) =
(BaseβπΉ) |
4 | 1, 2, 3 | uvcff 21213 |
. . 3
β’ ((π
β Ring β§ πΌ β π) β π:πΌβΆ(BaseβπΉ)) |
5 | 4 | frnd 6677 |
. 2
β’ ((π
β Ring β§ πΌ β π) β ran π β (BaseβπΉ)) |
6 | | suppssdm 8109 |
. . . . . 6
β’ (π supp (0gβπ
)) β dom π |
7 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβπ
) =
(Baseβπ
) |
8 | 2, 7, 3 | frlmbasf 21182 |
. . . . . . 7
β’ ((πΌ β π β§ π β (BaseβπΉ)) β π:πΌβΆ(Baseβπ
)) |
9 | 8 | adantll 713 |
. . . . . 6
β’ (((π
β Ring β§ πΌ β π) β§ π β (BaseβπΉ)) β π:πΌβΆ(Baseβπ
)) |
10 | 6, 9 | fssdm 6689 |
. . . . 5
β’ (((π
β Ring β§ πΌ β π) β§ π β (BaseβπΉ)) β (π supp (0gβπ
)) β πΌ) |
11 | 10 | ralrimiva 3140 |
. . . 4
β’ ((π
β Ring β§ πΌ β π) β βπ β (BaseβπΉ)(π supp (0gβπ
)) β πΌ) |
12 | | rabid2 3435 |
. . . 4
β’
((BaseβπΉ) =
{π β (BaseβπΉ) β£ (π supp (0gβπ
)) β πΌ} β βπ β (BaseβπΉ)(π supp (0gβπ
)) β πΌ) |
13 | 11, 12 | sylibr 233 |
. . 3
β’ ((π
β Ring β§ πΌ β π) β (BaseβπΉ) = {π β (BaseβπΉ) β£ (π supp (0gβπ
)) β πΌ}) |
14 | | ssid 3967 |
. . . 4
β’ πΌ β πΌ |
15 | | eqid 2733 |
. . . . 5
β’
(LSpanβπΉ) =
(LSpanβπΉ) |
16 | | eqid 2733 |
. . . . 5
β’
(0gβπ
) = (0gβπ
) |
17 | | eqid 2733 |
. . . . 5
β’ {π β (BaseβπΉ) β£ (π supp (0gβπ
)) β πΌ} = {π β (BaseβπΉ) β£ (π supp (0gβπ
)) β πΌ} |
18 | 2, 1, 15, 3, 16, 17 | frlmsslsp 21218 |
. . . 4
β’ ((π
β Ring β§ πΌ β π β§ πΌ β πΌ) β ((LSpanβπΉ)β(π β πΌ)) = {π β (BaseβπΉ) β£ (π supp (0gβπ
)) β πΌ}) |
19 | 14, 18 | mp3an3 1451 |
. . 3
β’ ((π
β Ring β§ πΌ β π) β ((LSpanβπΉ)β(π β πΌ)) = {π β (BaseβπΉ) β£ (π supp (0gβπ
)) β πΌ}) |
20 | | ffn 6669 |
. . . . 5
β’ (π:πΌβΆ(BaseβπΉ) β π Fn πΌ) |
21 | | fnima 6632 |
. . . . 5
β’ (π Fn πΌ β (π β πΌ) = ran π) |
22 | 4, 20, 21 | 3syl 18 |
. . . 4
β’ ((π
β Ring β§ πΌ β π) β (π β πΌ) = ran π) |
23 | 22 | fveq2d 6847 |
. . 3
β’ ((π
β Ring β§ πΌ β π) β ((LSpanβπΉ)β(π β πΌ)) = ((LSpanβπΉ)βran π)) |
24 | 13, 19, 23 | 3eqtr2rd 2780 |
. 2
β’ ((π
β Ring β§ πΌ β π) β ((LSpanβπΉ)βran π) = (BaseβπΉ)) |
25 | | eqid 2733 |
. . . . . 6
β’ (
Β·π βπΉ) = ( Β·π
βπΉ) |
26 | | eqid 2733 |
. . . . . 6
β’ {π β (BaseβπΉ) β£ (π supp (0gβπ
)) β (πΌ β {π})} = {π β (BaseβπΉ) β£ (π supp (0gβπ
)) β (πΌ β {π})} |
27 | | simpll 766 |
. . . . . 6
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β π
β Ring) |
28 | | simplr 768 |
. . . . . 6
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β πΌ β π) |
29 | | difssd 4093 |
. . . . . 6
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β (πΌ β {π}) β πΌ) |
30 | | vsnid 4624 |
. . . . . . 7
β’ π β {π} |
31 | | snssi 4769 |
. . . . . . . . 9
β’ (π β πΌ β {π} β πΌ) |
32 | 31 | ad2antrl 727 |
. . . . . . . 8
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β {π} β πΌ) |
33 | | dfss4 4219 |
. . . . . . . 8
β’ ({π} β πΌ β (πΌ β (πΌ β {π})) = {π}) |
34 | 32, 33 | sylib 217 |
. . . . . . 7
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β (πΌ β (πΌ β {π})) = {π}) |
35 | 30, 34 | eleqtrrid 2841 |
. . . . . 6
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β π β (πΌ β (πΌ β {π}))) |
36 | 2 | frlmsca 21175 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ πΌ β π) β π
= (ScalarβπΉ)) |
37 | 36 | fveq2d 6847 |
. . . . . . . . . 10
β’ ((π
β Ring β§ πΌ β π) β (Baseβπ
) = (Baseβ(ScalarβπΉ))) |
38 | 36 | fveq2d 6847 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ πΌ β π) β (0gβπ
) =
(0gβ(ScalarβπΉ))) |
39 | 38 | sneqd 4599 |
. . . . . . . . . 10
β’ ((π
β Ring β§ πΌ β π) β {(0gβπ
)} =
{(0gβ(ScalarβπΉ))}) |
40 | 37, 39 | difeq12d 4084 |
. . . . . . . . 9
β’ ((π
β Ring β§ πΌ β π) β ((Baseβπ
) β {(0gβπ
)}) =
((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))})) |
41 | 40 | eleq2d 2820 |
. . . . . . . 8
β’ ((π
β Ring β§ πΌ β π) β (π β ((Baseβπ
) β {(0gβπ
)}) β π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) |
42 | 41 | biimpar 479 |
. . . . . . 7
β’ (((π
β Ring β§ πΌ β π) β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))})) β π β ((Baseβπ
) β {(0gβπ
)})) |
43 | 42 | adantrl 715 |
. . . . . 6
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β π β ((Baseβπ
) β {(0gβπ
)})) |
44 | 2, 1, 3, 7, 25, 16, 26, 27, 28, 29, 35, 43 | frlmssuvc2 21217 |
. . . . 5
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β Β¬ (π( Β·π
βπΉ)(πβπ)) β {π β (BaseβπΉ) β£ (π supp (0gβπ
)) β (πΌ β {π})}) |
45 | 16, 7 | ringelnzr 20752 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ π β ((Baseβπ
) β
{(0gβπ
)}))
β π
β
NzRing) |
46 | 27, 43, 45 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β π
β NzRing) |
47 | 1, 2, 3 | uvcf1 21214 |
. . . . . . . . . 10
β’ ((π
β NzRing β§ πΌ β π) β π:πΌβ1-1β(BaseβπΉ)) |
48 | 46, 28, 47 | syl2anc 585 |
. . . . . . . . 9
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β π:πΌβ1-1β(BaseβπΉ)) |
49 | | df-f1 6502 |
. . . . . . . . . 10
β’ (π:πΌβ1-1β(BaseβπΉ) β (π:πΌβΆ(BaseβπΉ) β§ Fun β‘π)) |
50 | 49 | simprbi 498 |
. . . . . . . . 9
β’ (π:πΌβ1-1β(BaseβπΉ) β Fun β‘π) |
51 | | imadif 6586 |
. . . . . . . . 9
β’ (Fun
β‘π β (π β (πΌ β {π})) = ((π β πΌ) β (π β {π}))) |
52 | 48, 50, 51 | 3syl 18 |
. . . . . . . 8
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β (π β (πΌ β {π})) = ((π β πΌ) β (π β {π}))) |
53 | | f1fn 6740 |
. . . . . . . . . 10
β’ (π:πΌβ1-1β(BaseβπΉ) β π Fn πΌ) |
54 | 48, 53, 21 | 3syl 18 |
. . . . . . . . 9
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β (π β πΌ) = ran π) |
55 | 48, 53 | syl 17 |
. . . . . . . . . . 11
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β π Fn πΌ) |
56 | | simprl 770 |
. . . . . . . . . . 11
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β π β πΌ) |
57 | | fnsnfv 6921 |
. . . . . . . . . . 11
β’ ((π Fn πΌ β§ π β πΌ) β {(πβπ)} = (π β {π})) |
58 | 55, 56, 57 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β {(πβπ)} = (π β {π})) |
59 | 58 | eqcomd 2739 |
. . . . . . . . 9
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β (π β {π}) = {(πβπ)}) |
60 | 54, 59 | difeq12d 4084 |
. . . . . . . 8
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β ((π β πΌ) β (π β {π})) = (ran π β {(πβπ)})) |
61 | 52, 60 | eqtr2d 2774 |
. . . . . . 7
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β (ran π β {(πβπ)}) = (π β (πΌ β {π}))) |
62 | 61 | fveq2d 6847 |
. . . . . 6
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β ((LSpanβπΉ)β(ran π β {(πβπ)})) = ((LSpanβπΉ)β(π β (πΌ β {π})))) |
63 | 2, 1, 15, 3, 16, 26 | frlmsslsp 21218 |
. . . . . . 7
β’ ((π
β Ring β§ πΌ β π β§ (πΌ β {π}) β πΌ) β ((LSpanβπΉ)β(π β (πΌ β {π}))) = {π β (BaseβπΉ) β£ (π supp (0gβπ
)) β (πΌ β {π})}) |
64 | 27, 28, 29, 63 | syl3anc 1372 |
. . . . . 6
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β ((LSpanβπΉ)β(π β (πΌ β {π}))) = {π β (BaseβπΉ) β£ (π supp (0gβπ
)) β (πΌ β {π})}) |
65 | 62, 64 | eqtrd 2773 |
. . . . 5
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β ((LSpanβπΉ)β(ran π β {(πβπ)})) = {π β (BaseβπΉ) β£ (π supp (0gβπ
)) β (πΌ β {π})}) |
66 | 44, 65 | neleqtrrd 2857 |
. . . 4
β’ (((π
β Ring β§ πΌ β π) β§ (π β πΌ β§ π β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}))) β Β¬ (π( Β·π
βπΉ)(πβπ)) β ((LSpanβπΉ)β(ran π β {(πβπ)}))) |
67 | 66 | ralrimivva 3194 |
. . 3
β’ ((π
β Ring β§ πΌ β π) β βπ β πΌ βπ β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}) Β¬ (π( Β·π
βπΉ)(πβπ)) β ((LSpanβπΉ)β(ran π β {(πβπ)}))) |
68 | | oveq2 7366 |
. . . . . . . 8
β’ (π = (πβπ) β (π( Β·π
βπΉ)π) = (π( Β·π
βπΉ)(πβπ))) |
69 | | sneq 4597 |
. . . . . . . . . 10
β’ (π = (πβπ) β {π} = {(πβπ)}) |
70 | 69 | difeq2d 4083 |
. . . . . . . . 9
β’ (π = (πβπ) β (ran π β {π}) = (ran π β {(πβπ)})) |
71 | 70 | fveq2d 6847 |
. . . . . . . 8
β’ (π = (πβπ) β ((LSpanβπΉ)β(ran π β {π})) = ((LSpanβπΉ)β(ran π β {(πβπ)}))) |
72 | 68, 71 | eleq12d 2828 |
. . . . . . 7
β’ (π = (πβπ) β ((π( Β·π
βπΉ)π) β ((LSpanβπΉ)β(ran π β {π})) β (π( Β·π
βπΉ)(πβπ)) β ((LSpanβπΉ)β(ran π β {(πβπ)})))) |
73 | 72 | notbid 318 |
. . . . . 6
β’ (π = (πβπ) β (Β¬ (π( Β·π
βπΉ)π) β ((LSpanβπΉ)β(ran π β {π})) β Β¬ (π( Β·π
βπΉ)(πβπ)) β ((LSpanβπΉ)β(ran π β {(πβπ)})))) |
74 | 73 | ralbidv 3171 |
. . . . 5
β’ (π = (πβπ) β (βπ β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}) Β¬ (π( Β·π
βπΉ)π) β ((LSpanβπΉ)β(ran π β {π})) β βπ β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}) Β¬ (π( Β·π
βπΉ)(πβπ)) β ((LSpanβπΉ)β(ran π β {(πβπ)})))) |
75 | 74 | ralrn 7039 |
. . . 4
β’ (π Fn πΌ β (βπ β ran πβπ β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}) Β¬ (π( Β·π
βπΉ)π) β ((LSpanβπΉ)β(ran π β {π})) β βπ β πΌ βπ β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}) Β¬ (π( Β·π
βπΉ)(πβπ)) β ((LSpanβπΉ)β(ran π β {(πβπ)})))) |
76 | 4, 20, 75 | 3syl 18 |
. . 3
β’ ((π
β Ring β§ πΌ β π) β (βπ β ran πβπ β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}) Β¬ (π( Β·π
βπΉ)π) β ((LSpanβπΉ)β(ran π β {π})) β βπ β πΌ βπ β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}) Β¬ (π( Β·π
βπΉ)(πβπ)) β ((LSpanβπΉ)β(ran π β {(πβπ)})))) |
77 | 67, 76 | mpbird 257 |
. 2
β’ ((π
β Ring β§ πΌ β π) β βπ β ran πβπ β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}) Β¬ (π( Β·π
βπΉ)π) β ((LSpanβπΉ)β(ran π β {π}))) |
78 | 2 | ovexi 7392 |
. . 3
β’ πΉ β V |
79 | | eqid 2733 |
. . . 4
β’
(ScalarβπΉ) =
(ScalarβπΉ) |
80 | | eqid 2733 |
. . . 4
β’
(Baseβ(ScalarβπΉ)) = (Baseβ(ScalarβπΉ)) |
81 | | frlmlbs.j |
. . . 4
β’ π½ = (LBasisβπΉ) |
82 | | eqid 2733 |
. . . 4
β’
(0gβ(ScalarβπΉ)) =
(0gβ(ScalarβπΉ)) |
83 | 3, 79, 25, 80, 81, 15, 82 | islbs 20552 |
. . 3
β’ (πΉ β V β (ran π β π½ β (ran π β (BaseβπΉ) β§ ((LSpanβπΉ)βran π) = (BaseβπΉ) β§ βπ β ran πβπ β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}) Β¬ (π( Β·π
βπΉ)π) β ((LSpanβπΉ)β(ran π β {π}))))) |
84 | 78, 83 | ax-mp 5 |
. 2
β’ (ran
π β π½ β (ran π β (BaseβπΉ) β§ ((LSpanβπΉ)βran π) = (BaseβπΉ) β§ βπ β ran πβπ β ((Baseβ(ScalarβπΉ)) β
{(0gβ(ScalarβπΉ))}) Β¬ (π( Β·π
βπΉ)π) β ((LSpanβπΉ)β(ran π β {π})))) |
85 | 5, 24, 77, 84 | syl3anbrc 1344 |
1
β’ ((π
β Ring β§ πΌ β π) β ran π β π½) |