Step | Hyp | Ref
| Expression |
1 | | lsmcss.3 |
. . . . . . 7
β’ (π β ( β₯ β( β₯
βπ)) β (π β ( β₯
βπ))) |
2 | 1 | sseld 3944 |
. . . . . 6
β’ (π β (π₯ β ( β₯ β( β₯
βπ)) β π₯ β (π β ( β₯
βπ)))) |
3 | | lsmcss.1 |
. . . . . . . 8
β’ (π β π β PreHil) |
4 | | phllmod 21050 |
. . . . . . . 8
β’ (π β PreHil β π β LMod) |
5 | 3, 4 | syl 17 |
. . . . . . 7
β’ (π β π β LMod) |
6 | | lsmcss.2 |
. . . . . . 7
β’ (π β π β π) |
7 | | lsmcss.j |
. . . . . . . . 9
β’ π = (Baseβπ) |
8 | | lsmcss.o |
. . . . . . . . 9
β’ β₯ =
(ocvβπ) |
9 | 7, 8 | ocvss 21090 |
. . . . . . . 8
β’ ( β₯
βπ) β π |
10 | 9 | a1i 11 |
. . . . . . 7
β’ (π β ( β₯ βπ) β π) |
11 | | eqid 2733 |
. . . . . . . 8
β’
(+gβπ) = (+gβπ) |
12 | | lsmcss.p |
. . . . . . . 8
β’ β =
(LSSumβπ) |
13 | 7, 11, 12 | lsmelvalx 19427 |
. . . . . . 7
β’ ((π β LMod β§ π β π β§ ( β₯ βπ) β π) β (π₯ β (π β ( β₯
βπ)) β
βπ¦ β π βπ§ β ( β₯ βπ)π₯ = (π¦(+gβπ)π§))) |
14 | 5, 6, 10, 13 | syl3anc 1372 |
. . . . . 6
β’ (π β (π₯ β (π β ( β₯
βπ)) β
βπ¦ β π βπ§ β ( β₯ βπ)π₯ = (π¦(+gβπ)π§))) |
15 | 2, 14 | sylibd 238 |
. . . . 5
β’ (π β (π₯ β ( β₯ β( β₯
βπ)) β
βπ¦ β π βπ§ β ( β₯ βπ)π₯ = (π¦(+gβπ)π§))) |
16 | 3 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β π β PreHil) |
17 | 6 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β π β π) |
18 | | simplrl 776 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β π¦ β π) |
19 | 17, 18 | sseldd 3946 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β π¦ β π) |
20 | | simplrr 777 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β π§ β ( β₯ βπ)) |
21 | 9, 20 | sselid 3943 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β π§ β π) |
22 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(Scalarβπ) =
(Scalarβπ) |
23 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(Β·πβπ) =
(Β·πβπ) |
24 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ)) |
25 | 22, 23, 7, 11, 24 | ipdir 21059 |
. . . . . . . . . . . . . . 15
β’ ((π β PreHil β§ (π¦ β π β§ π§ β π β§ π§ β π)) β ((π¦(+gβπ)π§)(Β·πβπ)π§) = ((π¦(Β·πβπ)π§)(+gβ(Scalarβπ))(π§(Β·πβπ)π§))) |
26 | 16, 19, 21, 21, 25 | syl13anc 1373 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β ((π¦(+gβπ)π§)(Β·πβπ)π§) = ((π¦(Β·πβπ)π§)(+gβ(Scalarβπ))(π§(Β·πβπ)π§))) |
27 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
28 | 7, 23, 22, 27, 8 | ocvi 21089 |
. . . . . . . . . . . . . . . . 17
β’ ((π§ β ( β₯ βπ) β§ π¦ β π) β (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) |
29 | 20, 18, 28 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) |
30 | 22, 23, 7, 27 | iporthcom 21055 |
. . . . . . . . . . . . . . . . 17
β’ ((π β PreHil β§ π§ β π β§ π¦ β π) β ((π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)) β (π¦(Β·πβπ)π§) = (0gβ(Scalarβπ)))) |
31 | 16, 21, 19, 30 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β ((π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)) β (π¦(Β·πβπ)π§) = (0gβ(Scalarβπ)))) |
32 | 29, 31 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β (π¦(Β·πβπ)π§) = (0gβ(Scalarβπ))) |
33 | 32 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β ((π¦(Β·πβπ)π§)(+gβ(Scalarβπ))(π§(Β·πβπ)π§)) = ((0gβ(Scalarβπ))(+gβ(Scalarβπ))(π§(Β·πβπ)π§))) |
34 | 16, 4 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β π β LMod) |
35 | 22 | lmodfgrp 20345 |
. . . . . . . . . . . . . . . 16
β’ (π β LMod β
(Scalarβπ) β
Grp) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β
(Scalarβπ) β
Grp) |
37 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
38 | 22, 23, 7, 37 | ipcl 21053 |
. . . . . . . . . . . . . . . 16
β’ ((π β PreHil β§ π§ β π β§ π§ β π) β (π§(Β·πβπ)π§) β (Baseβ(Scalarβπ))) |
39 | 16, 21, 21, 38 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β (π§(Β·πβπ)π§) β (Baseβ(Scalarβπ))) |
40 | 37, 24, 27 | grplid 18785 |
. . . . . . . . . . . . . . 15
β’
(((Scalarβπ)
β Grp β§ (π§(Β·πβπ)π§) β (Baseβ(Scalarβπ))) β
((0gβ(Scalarβπ))(+gβ(Scalarβπ))(π§(Β·πβπ)π§)) = (π§(Β·πβπ)π§)) |
41 | 36, 39, 40 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β
((0gβ(Scalarβπ))(+gβ(Scalarβπ))(π§(Β·πβπ)π§)) = (π§(Β·πβπ)π§)) |
42 | 26, 33, 41 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β ((π¦(+gβπ)π§)(Β·πβπ)π§) = (π§(Β·πβπ)π§)) |
43 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) |
44 | 7, 23, 22, 27, 8 | ocvi 21089 |
. . . . . . . . . . . . . 14
β’ (((π¦(+gβπ)π§) β ( β₯ β( β₯
βπ)) β§ π§ β ( β₯ βπ)) β ((π¦(+gβπ)π§)(Β·πβπ)π§) = (0gβ(Scalarβπ))) |
45 | 43, 20, 44 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β ((π¦(+gβπ)π§)(Β·πβπ)π§) = (0gβ(Scalarβπ))) |
46 | 42, 45 | eqtr3d 2775 |
. . . . . . . . . . . 12
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β (π§(Β·πβπ)π§) = (0gβ(Scalarβπ))) |
47 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(0gβπ) = (0gβπ) |
48 | 22, 23, 7, 27, 47 | ipeq0 21058 |
. . . . . . . . . . . . 13
β’ ((π β PreHil β§ π§ β π) β ((π§(Β·πβπ)π§) = (0gβ(Scalarβπ)) β π§ = (0gβπ))) |
49 | 16, 21, 48 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β ((π§(Β·πβπ)π§) = (0gβ(Scalarβπ)) β π§ = (0gβπ))) |
50 | 46, 49 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β π§ = (0gβπ)) |
51 | 50 | oveq2d 7374 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β (π¦(+gβπ)π§) = (π¦(+gβπ)(0gβπ))) |
52 | | lmodgrp 20343 |
. . . . . . . . . . . . 13
β’ (π β LMod β π β Grp) |
53 | 5, 52 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β Grp) |
54 | 53 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β π β Grp) |
55 | 7, 11, 47 | grprid 18786 |
. . . . . . . . . . 11
β’ ((π β Grp β§ π¦ β π) β (π¦(+gβπ)(0gβπ)) = π¦) |
56 | 54, 19, 55 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β (π¦(+gβπ)(0gβπ)) = π¦) |
57 | 51, 56 | eqtrd 2773 |
. . . . . . . . 9
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β (π¦(+gβπ)π§) = π¦) |
58 | 57, 18 | eqeltrd 2834 |
. . . . . . . 8
β’ (((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β§ (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ))) β (π¦(+gβπ)π§) β π) |
59 | 58 | ex 414 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β ((π¦(+gβπ)π§) β ( β₯ β( β₯
βπ)) β (π¦(+gβπ)π§) β π)) |
60 | | eleq1 2822 |
. . . . . . . 8
β’ (π₯ = (π¦(+gβπ)π§) β (π₯ β ( β₯ β( β₯
βπ)) β (π¦(+gβπ)π§) β ( β₯ β( β₯
βπ)))) |
61 | | eleq1 2822 |
. . . . . . . 8
β’ (π₯ = (π¦(+gβπ)π§) β (π₯ β π β (π¦(+gβπ)π§) β π)) |
62 | 60, 61 | imbi12d 345 |
. . . . . . 7
β’ (π₯ = (π¦(+gβπ)π§) β ((π₯ β ( β₯ β( β₯
βπ)) β π₯ β π) β ((π¦(+gβπ)π§) β ( β₯ β( β₯
βπ)) β (π¦(+gβπ)π§) β π))) |
63 | 59, 62 | syl5ibrcom 247 |
. . . . . 6
β’ ((π β§ (π¦ β π β§ π§ β ( β₯ βπ))) β (π₯ = (π¦(+gβπ)π§) β (π₯ β ( β₯ β( β₯
βπ)) β π₯ β π))) |
64 | 63 | rexlimdvva 3202 |
. . . . 5
β’ (π β (βπ¦ β π βπ§ β ( β₯ βπ)π₯ = (π¦(+gβπ)π§) β (π₯ β ( β₯ β( β₯
βπ)) β π₯ β π))) |
65 | 15, 64 | syld 47 |
. . . 4
β’ (π β (π₯ β ( β₯ β( β₯
βπ)) β (π₯ β ( β₯ β( β₯
βπ)) β π₯ β π))) |
66 | 65 | pm2.43d 53 |
. . 3
β’ (π β (π₯ β ( β₯ β( β₯
βπ)) β π₯ β π)) |
67 | 66 | ssrdv 3951 |
. 2
β’ (π β ( β₯ β( β₯
βπ)) β π) |
68 | | lsmcss.c |
. . . 4
β’ πΆ = (ClSubSpβπ) |
69 | 7, 68, 8 | iscss2 21106 |
. . 3
β’ ((π β PreHil β§ π β π) β (π β πΆ β ( β₯ β( β₯
βπ)) β π)) |
70 | 3, 6, 69 | syl2anc 585 |
. 2
β’ (π β (π β πΆ β ( β₯ β( β₯
βπ)) β π)) |
71 | 67, 70 | mpbird 257 |
1
β’ (π β π β πΆ) |