Step | Hyp | Ref
| Expression |
1 | | oveq2 7370 |
. . . . . 6
β’ (π₯ = 0 β (π( Β·π
βπ)π₯) = (π( Β·π
βπ) 0
)) |
2 | | sneq 4601 |
. . . . . . . 8
β’ (π₯ = 0 β {π₯} = { 0 }) |
3 | 2 | difeq2d 4087 |
. . . . . . 7
β’ (π₯ = 0 β (πΉ β {π₯}) = (πΉ β { 0 })) |
4 | 3 | fveq2d 6851 |
. . . . . 6
β’ (π₯ = 0 β ((LSpanβπ)β(πΉ β {π₯})) = ((LSpanβπ)β(πΉ β { 0 }))) |
5 | 1, 4 | eleq12d 2832 |
. . . . 5
β’ (π₯ = 0 β ((π(
Β·π βπ)π₯) β ((LSpanβπ)β(πΉ β {π₯})) β (π( Β·π
βπ) 0 ) β
((LSpanβπ)β(πΉ β { 0 })))) |
6 | 5 | notbid 318 |
. . . 4
β’ (π₯ = 0 β (Β¬ (π(
Β·π βπ)π₯) β ((LSpanβπ)β(πΉ β {π₯})) β Β¬ (π( Β·π
βπ) 0 ) β
((LSpanβπ)β(πΉ β { 0 })))) |
7 | 6 | ralbidv 3175 |
. . 3
β’ (π₯ = 0 β (βπ β
((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)π₯) β ((LSpanβπ)β(πΉ β {π₯})) β βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ) 0 ) β
((LSpanβπ)β(πΉ β { 0 })))) |
8 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
9 | | eqid 2737 |
. . . . . 6
β’ (
Β·π βπ) = ( Β·π
βπ) |
10 | | eqid 2737 |
. . . . . 6
β’
(LSpanβπ) =
(LSpanβπ) |
11 | | eqid 2737 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
12 | | eqid 2737 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
13 | | eqid 2737 |
. . . . . 6
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
14 | 8, 9, 10, 11, 12, 13 | islinds2 21235 |
. . . . 5
β’ (π β LVec β (πΉ β (LIndSβπ) β (πΉ β (Baseβπ) β§ βπ₯ β πΉ βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)π₯) β ((LSpanβπ)β(πΉ β {π₯}))))) |
15 | 14 | simplbda 501 |
. . . 4
β’ ((π β LVec β§ πΉ β (LIndSβπ)) β βπ₯ β πΉ βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)π₯) β ((LSpanβπ)β(πΉ β {π₯}))) |
16 | 15 | adantr 482 |
. . 3
β’ (((π β LVec β§ πΉ β (LIndSβπ)) β§ 0 β πΉ) β βπ₯ β πΉ βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)π₯) β ((LSpanβπ)β(πΉ β {π₯}))) |
17 | | simpr 486 |
. . 3
β’ (((π β LVec β§ πΉ β (LIndSβπ)) β§ 0 β πΉ) β 0 β πΉ) |
18 | 7, 16, 17 | rspcdva 3585 |
. 2
β’ (((π β LVec β§ πΉ β (LIndSβπ)) β§ 0 β πΉ) β βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ) 0 ) β
((LSpanβπ)β(πΉ β { 0 }))) |
19 | | lveclmod 20583 |
. . . . . . . 8
β’ (π β LVec β π β LMod) |
20 | | eqid 2737 |
. . . . . . . . 9
β’
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ)) |
21 | 11, 12, 20 | lmod1cl 20365 |
. . . . . . . 8
β’ (π β LMod β
(1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) |
22 | 19, 21 | syl 17 |
. . . . . . 7
β’ (π β LVec β
(1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) |
23 | 22 | adantr 482 |
. . . . . 6
β’ ((π β LVec β§ πΉ β (LIndSβπ)) β
(1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) |
24 | 11 | lvecdrng 20582 |
. . . . . . . 8
β’ (π β LVec β
(Scalarβπ) β
DivRing) |
25 | 13, 20 | drngunz 20217 |
. . . . . . . 8
β’
((Scalarβπ)
β DivRing β (1rβ(Scalarβπ)) β
(0gβ(Scalarβπ))) |
26 | 24, 25 | syl 17 |
. . . . . . 7
β’ (π β LVec β
(1rβ(Scalarβπ)) β
(0gβ(Scalarβπ))) |
27 | 26 | adantr 482 |
. . . . . 6
β’ ((π β LVec β§ πΉ β (LIndSβπ)) β
(1rβ(Scalarβπ)) β
(0gβ(Scalarβπ))) |
28 | | eldifsn 4752 |
. . . . . 6
β’
((1rβ(Scalarβπ)) β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) β
((1rβ(Scalarβπ)) β (Baseβ(Scalarβπ)) β§
(1rβ(Scalarβπ)) β
(0gβ(Scalarβπ)))) |
29 | 23, 27, 28 | sylanbrc 584 |
. . . . 5
β’ ((π β LVec β§ πΉ β (LIndSβπ)) β
(1rβ(Scalarβπ)) β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) |
30 | 29 | adantr 482 |
. . . 4
β’ (((π β LVec β§ πΉ β (LIndSβπ)) β§ 0 β πΉ) β
(1rβ(Scalarβπ)) β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) |
31 | 19 | ad2antrr 725 |
. . . . . 6
β’ (((π β LVec β§ πΉ β (LIndSβπ)) β§ 0 β πΉ) β π β LMod) |
32 | | 0nellinds.1 |
. . . . . . 7
β’ 0 =
(0gβπ) |
33 | 11, 9, 12, 32 | lmodvs0 20372 |
. . . . . 6
β’ ((π β LMod β§
(1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) β
((1rβ(Scalarβπ))( Β·π
βπ) 0 ) = 0
) |
34 | 31, 21, 33 | syl2anc2 586 |
. . . . 5
β’ (((π β LVec β§ πΉ β (LIndSβπ)) β§ 0 β πΉ) β
((1rβ(Scalarβπ))( Β·π
βπ) 0 ) = 0
) |
35 | 8 | linds1 21232 |
. . . . . . . 8
β’ (πΉ β (LIndSβπ) β πΉ β (Baseβπ)) |
36 | 35 | ad2antlr 726 |
. . . . . . 7
β’ (((π β LVec β§ πΉ β (LIndSβπ)) β§ 0 β πΉ) β πΉ β (Baseβπ)) |
37 | 36 | ssdifssd 4107 |
. . . . . 6
β’ (((π β LVec β§ πΉ β (LIndSβπ)) β§ 0 β πΉ) β (πΉ β { 0 }) β
(Baseβπ)) |
38 | 32, 8, 10 | 0ellsp 32198 |
. . . . . 6
β’ ((π β LMod β§ (πΉ β { 0 }) β
(Baseβπ)) β
0 β
((LSpanβπ)β(πΉ β { 0 }))) |
39 | 31, 37, 38 | syl2anc 585 |
. . . . 5
β’ (((π β LVec β§ πΉ β (LIndSβπ)) β§ 0 β πΉ) β 0 β ((LSpanβπ)β(πΉ β { 0 }))) |
40 | 34, 39 | eqeltrd 2838 |
. . . 4
β’ (((π β LVec β§ πΉ β (LIndSβπ)) β§ 0 β πΉ) β
((1rβ(Scalarβπ))( Β·π
βπ) 0 ) β
((LSpanβπ)β(πΉ β { 0 }))) |
41 | | oveq1 7369 |
. . . . . 6
β’ (π =
(1rβ(Scalarβπ)) β (π( Β·π
βπ) 0 ) =
((1rβ(Scalarβπ))( Β·π
βπ) 0
)) |
42 | 41 | eleq1d 2823 |
. . . . 5
β’ (π =
(1rβ(Scalarβπ)) β ((π( Β·π
βπ) 0 ) β
((LSpanβπ)β(πΉ β { 0 })) β
((1rβ(Scalarβπ))( Β·π
βπ) 0 ) β
((LSpanβπ)β(πΉ β { 0 })))) |
43 | 42 | rspcev 3584 |
. . . 4
β’
(((1rβ(Scalarβπ)) β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) β§
((1rβ(Scalarβπ))( Β·π
βπ) 0 ) β
((LSpanβπ)β(πΉ β { 0 }))) β βπ β
((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})(π( Β·π
βπ) 0 ) β
((LSpanβπ)β(πΉ β { 0 }))) |
44 | 30, 40, 43 | syl2anc 585 |
. . 3
β’ (((π β LVec β§ πΉ β (LIndSβπ)) β§ 0 β πΉ) β βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})(π( Β·π
βπ) 0 ) β
((LSpanβπ)β(πΉ β { 0 }))) |
45 | | dfrex2 3077 |
. . 3
β’
(βπ β
((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})(π( Β·π
βπ) 0 ) β
((LSpanβπ)β(πΉ β { 0 })) β Β¬
βπ β
((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ) 0 ) β
((LSpanβπ)β(πΉ β { 0 }))) |
46 | 44, 45 | sylib 217 |
. 2
β’ (((π β LVec β§ πΉ β (LIndSβπ)) β§ 0 β πΉ) β Β¬ βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ) 0 ) β
((LSpanβπ)β(πΉ β { 0 }))) |
47 | 18, 46 | pm2.65da 816 |
1
β’ ((π β LVec β§ πΉ β (LIndSβπ)) β Β¬ 0 β πΉ) |