Step | Hyp | Ref
| Expression |
1 | | lindsun.w |
. . 3
β’ (π β π β LVec) |
2 | | lveclmod 20611 |
. . 3
β’ (π β LVec β π β LMod) |
3 | 1, 2 | syl 17 |
. 2
β’ (π β π β LMod) |
4 | | lindsun.u |
. . . 4
β’ (π β π β (LIndSβπ)) |
5 | | eqid 2733 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
6 | 5 | linds1 21239 |
. . . 4
β’ (π β (LIndSβπ) β π β (Baseβπ)) |
7 | 4, 6 | syl 17 |
. . 3
β’ (π β π β (Baseβπ)) |
8 | | lindsun.v |
. . . 4
β’ (π β π β (LIndSβπ)) |
9 | 5 | linds1 21239 |
. . . 4
β’ (π β (LIndSβπ) β π β (Baseβπ)) |
10 | 8, 9 | syl 17 |
. . 3
β’ (π β π β (Baseβπ)) |
11 | 7, 10 | unssd 4150 |
. 2
β’ (π β (π βͺ π) β (Baseβπ)) |
12 | | lindsun.n |
. . . . . . . . . 10
β’ π = (LSpanβπ) |
13 | | lindsun.0 |
. . . . . . . . . 10
β’ 0 =
(0gβπ) |
14 | 1 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β π) β π β LVec) |
15 | 4 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β π) β π β (LIndSβπ)) |
16 | 8 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β π) β π β (LIndSβπ)) |
17 | | lindsun.2 |
. . . . . . . . . . 11
β’ (π β ((πβπ) β© (πβπ)) = { 0 }) |
18 | 17 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β π) β ((πβπ) β© (πβπ)) = { 0 }) |
19 | | eqid 2733 |
. . . . . . . . . 10
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
20 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
21 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β π) β π β π) |
22 | | simpllr 775 |
. . . . . . . . . 10
β’ ((((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β π) β π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) |
23 | | simplr 768 |
. . . . . . . . . 10
β’ ((((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β π) β (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) |
24 | 12, 13, 14, 15, 16, 18, 19, 20, 21, 22, 23 | lindsunlem 32383 |
. . . . . . . . 9
β’ ((((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β π) β β₯) |
25 | 24 | adantlr 714 |
. . . . . . . 8
β’
(((((π β§ π β
((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β (π βͺ π)) β§ π β π) β β₯) |
26 | 1 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β π) β π β LVec) |
27 | 8 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β π) β π β (LIndSβπ)) |
28 | 4 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β π) β π β (LIndSβπ)) |
29 | | incom 4165 |
. . . . . . . . . . . 12
β’ ((πβπ) β© (πβπ)) = ((πβπ) β© (πβπ)) |
30 | 29, 17 | eqtr3id 2787 |
. . . . . . . . . . 11
β’ (π β ((πβπ) β© (πβπ)) = { 0 }) |
31 | 30 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β π) β ((πβπ) β© (πβπ)) = { 0 }) |
32 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β π) β π β π) |
33 | | simpllr 775 |
. . . . . . . . . 10
β’ ((((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β π) β π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) |
34 | | simplr 768 |
. . . . . . . . . . 11
β’ ((((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β π) β (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) |
35 | | uncom 4117 |
. . . . . . . . . . . . 13
β’ (π βͺ π) = (π βͺ π) |
36 | 35 | difeq1i 4082 |
. . . . . . . . . . . 12
β’ ((π βͺ π) β {π}) = ((π βͺ π) β {π}) |
37 | 36 | fveq2i 6849 |
. . . . . . . . . . 11
β’ (πβ((π βͺ π) β {π})) = (πβ((π βͺ π) β {π})) |
38 | 34, 37 | eleqtrdi 2844 |
. . . . . . . . . 10
β’ ((((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β π) β (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) |
39 | 12, 13, 26, 27, 28, 31, 19, 20, 32, 33, 38 | lindsunlem 32383 |
. . . . . . . . 9
β’ ((((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β π) β β₯) |
40 | 39 | adantlr 714 |
. . . . . . . 8
β’
(((((π β§ π β
((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β (π βͺ π)) β§ π β π) β β₯) |
41 | | elun 4112 |
. . . . . . . . . 10
β’ (π β (π βͺ π) β (π β π β¨ π β π)) |
42 | 41 | biimpi 215 |
. . . . . . . . 9
β’ (π β (π βͺ π) β (π β π β¨ π β π)) |
43 | 42 | adantl 483 |
. . . . . . . 8
β’ ((((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β (π βͺ π)) β (π β π β¨ π β π)) |
44 | 25, 40, 43 | mpjaodan 958 |
. . . . . . 7
β’ ((((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β§ π β (π βͺ π)) β β₯) |
45 | 44 | an32s 651 |
. . . . . 6
β’ ((((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ π β (π βͺ π)) β§ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) β β₯) |
46 | 45 | inegd 1562 |
. . . . 5
β’ (((π β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β§ π β (π βͺ π)) β Β¬ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) |
47 | 46 | an32s 651 |
. . . 4
β’ (((π β§ π β (π βͺ π)) β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β Β¬ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) |
48 | 47 | anasss 468 |
. . 3
β’ ((π β§ (π β (π βͺ π) β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β Β¬ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) |
49 | 48 | ralrimivva 3194 |
. 2
β’ (π β βπ β (π βͺ π)βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))) |
50 | | eqid 2733 |
. . . 4
β’ (
Β·π βπ) = ( Β·π
βπ) |
51 | | eqid 2733 |
. . . 4
β’
(Scalarβπ) =
(Scalarβπ) |
52 | 5, 50, 12, 51, 20, 19 | islinds2 21242 |
. . 3
β’ (π β LMod β ((π βͺ π) β (LIndSβπ) β ((π βͺ π) β (Baseβπ) β§ βπ β (π βͺ π)βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π}))))) |
53 | 52 | biimpar 479 |
. 2
β’ ((π β LMod β§ ((π βͺ π) β (Baseβπ) β§ βπ β (π βͺ π)βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)π) β (πβ((π βͺ π) β {π})))) β (π βͺ π) β (LIndSβπ)) |
54 | 3, 11, 49, 53 | syl12anc 836 |
1
β’ (π β (π βͺ π) β (LIndSβπ)) |