Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . 5
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) |
2 | | lindsun.w |
. . . . . . . . . . . . . 14
β’ (π β π β LVec) |
3 | | lveclmod 20583 |
. . . . . . . . . . . . . 14
β’ (π β LVec β π β LMod) |
4 | 2, 3 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β LMod) |
5 | | lmodgrp 20345 |
. . . . . . . . . . . . 13
β’ (π β LMod β π β Grp) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β Grp) |
7 | 6 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β π β Grp) |
8 | | lmodabl 20385 |
. . . . . . . . . . . . . . 15
β’ (π β LMod β π β Abel) |
9 | 4, 8 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π β Abel) |
10 | 9 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β π β Abel) |
11 | | lindsun.u |
. . . . . . . . . . . . . . . . 17
β’ (π β π β (LIndSβπ)) |
12 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
β’
(Baseβπ) =
(Baseβπ) |
13 | 12 | linds1 21232 |
. . . . . . . . . . . . . . . . 17
β’ (π β (LIndSβπ) β π β (Baseβπ)) |
14 | 11, 13 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π β (Baseβπ)) |
15 | | lindsun.n |
. . . . . . . . . . . . . . . . 17
β’ π = (LSpanβπ) |
16 | 12, 15 | lspssv 20460 |
. . . . . . . . . . . . . . . 16
β’ ((π β LMod β§ π β (Baseβπ)) β (πβπ) β (Baseβπ)) |
17 | 4, 14, 16 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (πβπ) β (Baseβπ)) |
18 | 17 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β (πβπ) β (Baseβπ)) |
19 | | difssd 4097 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π β {πΆ}) β π) |
20 | 12, 15 | lspss 20461 |
. . . . . . . . . . . . . . . . 17
β’ ((π β LMod β§ π β (Baseβπ) β§ (π β {πΆ}) β π) β (πβ(π β {πΆ})) β (πβπ)) |
21 | 4, 14, 19, 20 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (π β (πβ(π β {πΆ})) β (πβπ)) |
22 | 21 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β (πβ(π β {πΆ})) β (πβπ)) |
23 | | simpllr 775 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β π₯ β (πβ(π β {πΆ}))) |
24 | 22, 23 | sseldd 3950 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β π₯ β (πβπ)) |
25 | 18, 24 | sseldd 3950 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β π₯ β (Baseβπ)) |
26 | | lindsun.v |
. . . . . . . . . . . . . . . . 17
β’ (π β π β (LIndSβπ)) |
27 | 12 | linds1 21232 |
. . . . . . . . . . . . . . . . 17
β’ (π β (LIndSβπ) β π β (Baseβπ)) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π β (Baseβπ)) |
29 | 12, 15 | lspssv 20460 |
. . . . . . . . . . . . . . . 16
β’ ((π β LMod β§ π β (Baseβπ)) β (πβπ) β (Baseβπ)) |
30 | 4, 28, 29 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (πβπ) β (Baseβπ)) |
31 | 30 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β (πβπ) β (Baseβπ)) |
32 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β π¦ β (πβπ)) |
33 | 31, 32 | sseldd 3950 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β π¦ β (Baseβπ)) |
34 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(+gβπ) = (+gβπ) |
35 | 12, 34 | ablcom 19588 |
. . . . . . . . . . . . 13
β’ ((π β Abel β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯(+gβπ)π¦) = (π¦(+gβπ)π₯)) |
36 | 10, 25, 33, 35 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β (π₯(+gβπ)π¦) = (π¦(+gβπ)π₯)) |
37 | 1, 36 | eqtr2d 2778 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β (π¦(+gβπ)π₯) = (πΎ( Β·π
βπ)πΆ)) |
38 | | lindsunlem.k |
. . . . . . . . . . . . . 14
β’ (π β πΎ β (πΉ β {π})) |
39 | 38 | eldifad 3927 |
. . . . . . . . . . . . 13
β’ (π β πΎ β πΉ) |
40 | | lindsunlem.c |
. . . . . . . . . . . . . 14
β’ (π β πΆ β π) |
41 | 14, 40 | sseldd 3950 |
. . . . . . . . . . . . 13
β’ (π β πΆ β (Baseβπ)) |
42 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(Scalarβπ) =
(Scalarβπ) |
43 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’ (
Β·π βπ) = ( Β·π
βπ) |
44 | | lindsunlem.f |
. . . . . . . . . . . . . 14
β’ πΉ =
(Baseβ(Scalarβπ)) |
45 | 12, 42, 43, 44 | lmodvscl 20355 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ πΎ β πΉ β§ πΆ β (Baseβπ)) β (πΎ( Β·π
βπ)πΆ) β (Baseβπ)) |
46 | 4, 39, 41, 45 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (π β (πΎ( Β·π
βπ)πΆ) β (Baseβπ)) |
47 | 46 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β (πΎ( Β·π
βπ)πΆ) β (Baseβπ)) |
48 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(-gβπ) = (-gβπ) |
49 | 12, 34, 48 | grpsubadd 18842 |
. . . . . . . . . . . . 13
β’ ((π β Grp β§ ((πΎ(
Β·π βπ)πΆ) β (Baseβπ) β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (((πΎ( Β·π
βπ)πΆ)(-gβπ)π₯) = π¦ β (π¦(+gβπ)π₯) = (πΎ( Β·π
βπ)πΆ))) |
50 | 49 | biimpar 479 |
. . . . . . . . . . . 12
β’ (((π β Grp β§ ((πΎ(
Β·π βπ)πΆ) β (Baseβπ) β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π¦(+gβπ)π₯) = (πΎ( Β·π
βπ)πΆ)) β ((πΎ( Β·π
βπ)πΆ)(-gβπ)π₯) = π¦) |
51 | 50 | an32s 651 |
. . . . . . . . . . 11
β’ (((π β Grp β§ (π¦(+gβπ)π₯) = (πΎ( Β·π
βπ)πΆ)) β§ ((πΎ( Β·π
βπ)πΆ) β (Baseβπ) β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β ((πΎ( Β·π
βπ)πΆ)(-gβπ)π₯) = π¦) |
52 | 7, 37, 47, 25, 33, 51 | syl23anc 1378 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β ((πΎ( Β·π
βπ)πΆ)(-gβπ)π₯) = π¦) |
53 | 4 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β π β LMod) |
54 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(LSubSpβπ) =
(LSubSpβπ) |
55 | 12, 54, 15 | lspcl 20453 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ π β (Baseβπ)) β (πβπ) β (LSubSpβπ)) |
56 | 4, 14, 55 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (πβπ) β (LSubSpβπ)) |
57 | 56 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β (πβπ) β (LSubSpβπ)) |
58 | 39 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β πΎ β πΉ) |
59 | 12, 15 | lspssid 20462 |
. . . . . . . . . . . . . . 15
β’ ((π β LMod β§ π β (Baseβπ)) β π β (πβπ)) |
60 | 4, 14, 59 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β π β (πβπ)) |
61 | 60, 40 | sseldd 3950 |
. . . . . . . . . . . . 13
β’ (π β πΆ β (πβπ)) |
62 | 61 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β πΆ β (πβπ)) |
63 | 42, 43, 44, 54 | lssvscl 20432 |
. . . . . . . . . . . 12
β’ (((π β LMod β§ (πβπ) β (LSubSpβπ)) β§ (πΎ β πΉ β§ πΆ β (πβπ))) β (πΎ( Β·π
βπ)πΆ) β (πβπ)) |
64 | 53, 57, 58, 62, 63 | syl22anc 838 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β (πΎ( Β·π
βπ)πΆ) β (πβπ)) |
65 | 48, 54 | lssvsubcl 20420 |
. . . . . . . . . . 11
β’ (((π β LMod β§ (πβπ) β (LSubSpβπ)) β§ ((πΎ( Β·π
βπ)πΆ) β (πβπ) β§ π₯ β (πβπ))) β ((πΎ( Β·π
βπ)πΆ)(-gβπ)π₯) β (πβπ)) |
66 | 53, 57, 64, 24, 65 | syl22anc 838 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β ((πΎ( Β·π
βπ)πΆ)(-gβπ)π₯) β (πβπ)) |
67 | 52, 66 | eqeltrrd 2839 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β π¦ β (πβπ)) |
68 | 67, 32 | elind 4159 |
. . . . . . . 8
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β π¦ β ((πβπ) β© (πβπ))) |
69 | | lindsun.2 |
. . . . . . . . 9
β’ (π β ((πβπ) β© (πβπ)) = { 0 }) |
70 | 69 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β ((πβπ) β© (πβπ)) = { 0 }) |
71 | 68, 70 | eleqtrd 2840 |
. . . . . . 7
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β π¦ β { 0 }) |
72 | | elsni 4608 |
. . . . . . 7
β’ (π¦ β { 0 } β π¦ = 0 ) |
73 | 71, 72 | syl 17 |
. . . . . 6
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β π¦ = 0 ) |
74 | 73 | oveq2d 7378 |
. . . . 5
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β (π₯(+gβπ)π¦) = (π₯(+gβπ) 0 )) |
75 | | lindsun.0 |
. . . . . . 7
β’ 0 =
(0gβπ) |
76 | 12, 34, 75 | grprid 18788 |
. . . . . 6
β’ ((π β Grp β§ π₯ β (Baseβπ)) β (π₯(+gβπ) 0 ) = π₯) |
77 | 7, 25, 76 | syl2anc 585 |
. . . . 5
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β (π₯(+gβπ) 0 ) = π₯) |
78 | 1, 74, 77 | 3eqtrd 2781 |
. . . 4
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β (πΎ( Β·π
βπ)πΆ) = π₯) |
79 | 78, 23 | eqeltrd 2838 |
. . 3
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β (πΎ( Β·π
βπ)πΆ) β (πβ(π β {πΆ}))) |
80 | 40 | ad3antrrr 729 |
. . . 4
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β πΆ β π) |
81 | 38 | ad3antrrr 729 |
. . . 4
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β πΎ β (πΉ β {π})) |
82 | 2 | ad3antrrr 729 |
. . . . 5
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β π β LVec) |
83 | 11 | ad3antrrr 729 |
. . . . 5
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β π β (LIndSβπ)) |
84 | | lindsunlem.o |
. . . . . . 7
β’ π =
(0gβ(Scalarβπ)) |
85 | 12, 43, 15, 42, 44, 84 | islinds2 21235 |
. . . . . 6
β’ (π β LVec β (π β (LIndSβπ) β (π β (Baseβπ) β§ βπ β π βπ β (πΉ β {π}) Β¬ (π( Β·π
βπ)π) β (πβ(π β {π}))))) |
86 | 85 | simplbda 501 |
. . . . 5
β’ ((π β LVec β§ π β (LIndSβπ)) β βπ β π βπ β (πΉ β {π}) Β¬ (π( Β·π
βπ)π) β (πβ(π β {π}))) |
87 | 82, 83, 86 | syl2anc 585 |
. . . 4
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β βπ β π βπ β (πΉ β {π}) Β¬ (π( Β·π
βπ)π) β (πβ(π β {π}))) |
88 | | oveq2 7370 |
. . . . . . 7
β’ (π = πΆ β (π( Β·π
βπ)π) = (π( Β·π
βπ)πΆ)) |
89 | | sneq 4601 |
. . . . . . . . 9
β’ (π = πΆ β {π} = {πΆ}) |
90 | 89 | difeq2d 4087 |
. . . . . . . 8
β’ (π = πΆ β (π β {π}) = (π β {πΆ})) |
91 | 90 | fveq2d 6851 |
. . . . . . 7
β’ (π = πΆ β (πβ(π β {π})) = (πβ(π β {πΆ}))) |
92 | 88, 91 | eleq12d 2832 |
. . . . . 6
β’ (π = πΆ β ((π( Β·π
βπ)π) β (πβ(π β {π})) β (π( Β·π
βπ)πΆ) β (πβ(π β {πΆ})))) |
93 | 92 | notbid 318 |
. . . . 5
β’ (π = πΆ β (Β¬ (π( Β·π
βπ)π) β (πβ(π β {π})) β Β¬ (π( Β·π
βπ)πΆ) β (πβ(π β {πΆ})))) |
94 | | oveq1 7369 |
. . . . . . 7
β’ (π = πΎ β (π( Β·π
βπ)πΆ) = (πΎ( Β·π
βπ)πΆ)) |
95 | 94 | eleq1d 2823 |
. . . . . 6
β’ (π = πΎ β ((π( Β·π
βπ)πΆ) β (πβ(π β {πΆ})) β (πΎ( Β·π
βπ)πΆ) β (πβ(π β {πΆ})))) |
96 | 95 | notbid 318 |
. . . . 5
β’ (π = πΎ β (Β¬ (π( Β·π
βπ)πΆ) β (πβ(π β {πΆ})) β Β¬ (πΎ( Β·π
βπ)πΆ) β (πβ(π β {πΆ})))) |
97 | 93, 96 | rspc2va 3594 |
. . . 4
β’ (((πΆ β π β§ πΎ β (πΉ β {π})) β§ βπ β π βπ β (πΉ β {π}) Β¬ (π( Β·π
βπ)π) β (πβ(π β {π}))) β Β¬ (πΎ( Β·π
βπ)πΆ) β (πβ(π β {πΆ}))) |
98 | 80, 81, 87, 97 | syl21anc 837 |
. . 3
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β Β¬ (πΎ( Β·π
βπ)πΆ) β (πβ(π β {πΆ}))) |
99 | 79, 98 | pm2.21fal 1564 |
. 2
β’ ((((π β§ π₯ β (πβ(π β {πΆ}))) β§ π¦ β (πβπ)) β§ (πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) β β₯) |
100 | 14 | ssdifssd 4107 |
. . . . 5
β’ (π β (π β {πΆ}) β (Baseβπ)) |
101 | 12, 54, 15 | lspcl 20453 |
. . . . 5
β’ ((π β LMod β§ (π β {πΆ}) β (Baseβπ)) β (πβ(π β {πΆ})) β (LSubSpβπ)) |
102 | 4, 100, 101 | syl2anc 585 |
. . . 4
β’ (π β (πβ(π β {πΆ})) β (LSubSpβπ)) |
103 | 54 | lsssubg 20434 |
. . . 4
β’ ((π β LMod β§ (πβ(π β {πΆ})) β (LSubSpβπ)) β (πβ(π β {πΆ})) β (SubGrpβπ)) |
104 | 4, 102, 103 | syl2anc 585 |
. . 3
β’ (π β (πβ(π β {πΆ})) β (SubGrpβπ)) |
105 | 12, 54, 15 | lspcl 20453 |
. . . . 5
β’ ((π β LMod β§ π β (Baseβπ)) β (πβπ) β (LSubSpβπ)) |
106 | 4, 28, 105 | syl2anc 585 |
. . . 4
β’ (π β (πβπ) β (LSubSpβπ)) |
107 | 54 | lsssubg 20434 |
. . . 4
β’ ((π β LMod β§ (πβπ) β (LSubSpβπ)) β (πβπ) β (SubGrpβπ)) |
108 | 4, 106, 107 | syl2anc 585 |
. . 3
β’ (π β (πβπ) β (SubGrpβπ)) |
109 | | lindsunlem.1 |
. . . 4
β’ (π β (πΎ( Β·π
βπ)πΆ) β (πβ((π βͺ π) β {πΆ}))) |
110 | | eqid 2737 |
. . . . . . 7
β’
(LSSumβπ) =
(LSSumβπ) |
111 | 12, 15, 110 | lsmsp2 20564 |
. . . . . 6
β’ ((π β LMod β§ (π β {πΆ}) β (Baseβπ) β§ π β (Baseβπ)) β ((πβ(π β {πΆ}))(LSSumβπ)(πβπ)) = (πβ((π β {πΆ}) βͺ π))) |
112 | 4, 100, 28, 111 | syl3anc 1372 |
. . . . 5
β’ (π β ((πβ(π β {πΆ}))(LSSumβπ)(πβπ)) = (πβ((π β {πΆ}) βͺ π))) |
113 | 61 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ πΆ β π) β πΆ β (πβπ)) |
114 | 12, 15 | lspssid 20462 |
. . . . . . . . . . . . . . 15
β’ ((π β LMod β§ π β (Baseβπ)) β π β (πβπ)) |
115 | 4, 28, 114 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β π β (πβπ)) |
116 | 115 | sselda 3949 |
. . . . . . . . . . . . 13
β’ ((π β§ πΆ β π) β πΆ β (πβπ)) |
117 | 113, 116 | elind 4159 |
. . . . . . . . . . . 12
β’ ((π β§ πΆ β π) β πΆ β ((πβπ) β© (πβπ))) |
118 | 69 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ πΆ β π) β ((πβπ) β© (πβπ)) = { 0 }) |
119 | 117, 118 | eleqtrd 2840 |
. . . . . . . . . . 11
β’ ((π β§ πΆ β π) β πΆ β { 0 }) |
120 | | elsni 4608 |
. . . . . . . . . . 11
β’ (πΆ β { 0 } β πΆ = 0 ) |
121 | 119, 120 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ πΆ β π) β πΆ = 0 ) |
122 | 75 | 0nellinds 32199 |
. . . . . . . . . . . . . 14
β’ ((π β LVec β§ π β (LIndSβπ)) β Β¬ 0 β π) |
123 | 2, 11, 122 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β Β¬ 0 β π) |
124 | | nelne2 3043 |
. . . . . . . . . . . . 13
β’ ((πΆ β π β§ Β¬ 0 β π) β πΆ β 0 ) |
125 | 40, 123, 124 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β πΆ β 0 ) |
126 | 125 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ πΆ β π) β πΆ β 0 ) |
127 | 126 | neneqd 2949 |
. . . . . . . . . 10
β’ ((π β§ πΆ β π) β Β¬ πΆ = 0 ) |
128 | 121, 127 | pm2.65da 816 |
. . . . . . . . 9
β’ (π β Β¬ πΆ β π) |
129 | | disjsn 4677 |
. . . . . . . . 9
β’ ((π β© {πΆ}) = β
β Β¬ πΆ β π) |
130 | 128, 129 | sylibr 233 |
. . . . . . . 8
β’ (π β (π β© {πΆ}) = β
) |
131 | | undif4 4431 |
. . . . . . . 8
β’ ((π β© {πΆ}) = β
β (π βͺ (π β {πΆ})) = ((π βͺ π) β {πΆ})) |
132 | 130, 131 | syl 17 |
. . . . . . 7
β’ (π β (π βͺ (π β {πΆ})) = ((π βͺ π) β {πΆ})) |
133 | | uncom 4118 |
. . . . . . 7
β’ ((π β {πΆ}) βͺ π) = (π βͺ (π β {πΆ})) |
134 | | uncom 4118 |
. . . . . . . 8
β’ (π βͺ π) = (π βͺ π) |
135 | 134 | difeq1i 4083 |
. . . . . . 7
β’ ((π βͺ π) β {πΆ}) = ((π βͺ π) β {πΆ}) |
136 | 132, 133,
135 | 3eqtr4g 2802 |
. . . . . 6
β’ (π β ((π β {πΆ}) βͺ π) = ((π βͺ π) β {πΆ})) |
137 | 136 | fveq2d 6851 |
. . . . 5
β’ (π β (πβ((π β {πΆ}) βͺ π)) = (πβ((π βͺ π) β {πΆ}))) |
138 | 112, 137 | eqtrd 2777 |
. . . 4
β’ (π β ((πβ(π β {πΆ}))(LSSumβπ)(πβπ)) = (πβ((π βͺ π) β {πΆ}))) |
139 | 109, 138 | eleqtrrd 2841 |
. . 3
β’ (π β (πΎ( Β·π
βπ)πΆ) β ((πβ(π β {πΆ}))(LSSumβπ)(πβπ))) |
140 | 34, 110 | lsmelval 19438 |
. . . 4
β’ (((πβ(π β {πΆ})) β (SubGrpβπ) β§ (πβπ) β (SubGrpβπ)) β ((πΎ( Β·π
βπ)πΆ) β ((πβ(π β {πΆ}))(LSSumβπ)(πβπ)) β βπ₯ β (πβ(π β {πΆ}))βπ¦ β (πβπ)(πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦))) |
141 | 140 | biimpa 478 |
. . 3
β’ ((((πβ(π β {πΆ})) β (SubGrpβπ) β§ (πβπ) β (SubGrpβπ)) β§ (πΎ( Β·π
βπ)πΆ) β ((πβ(π β {πΆ}))(LSSumβπ)(πβπ))) β βπ₯ β (πβ(π β {πΆ}))βπ¦ β (πβπ)(πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) |
142 | 104, 108,
139, 141 | syl21anc 837 |
. 2
β’ (π β βπ₯ β (πβ(π β {πΆ}))βπ¦ β (πβπ)(πΎ( Β·π
βπ)πΆ) = (π₯(+gβπ)π¦)) |
143 | 99, 142 | r19.29vva 3208 |
1
β’ (π β β₯) |