Step | Hyp | Ref
| Expression |
1 | | ocvss.v |
. . . 4
β’ π = (Baseβπ) |
2 | | ocvss.o |
. . . 4
β’ β₯ =
(ocvβπ) |
3 | 1, 2 | ocvss 21090 |
. . 3
β’ ( β₯
βπ) β π |
4 | 3 | a1i 11 |
. 2
β’ ((π β PreHil β§ π β π) β ( β₯ βπ) β π) |
5 | | simpr 486 |
. . . 4
β’ ((π β PreHil β§ π β π) β π β π) |
6 | | phllmod 21050 |
. . . . . 6
β’ (π β PreHil β π β LMod) |
7 | 6 | adantr 482 |
. . . . 5
β’ ((π β PreHil β§ π β π) β π β LMod) |
8 | | eqid 2733 |
. . . . . 6
β’
(0gβπ) = (0gβπ) |
9 | 1, 8 | lmod0vcl 20366 |
. . . . 5
β’ (π β LMod β
(0gβπ)
β π) |
10 | 7, 9 | syl 17 |
. . . 4
β’ ((π β PreHil β§ π β π) β (0gβπ) β π) |
11 | | simpll 766 |
. . . . . 6
β’ (((π β PreHil β§ π β π) β§ π₯ β π) β π β PreHil) |
12 | 5 | sselda 3945 |
. . . . . 6
β’ (((π β PreHil β§ π β π) β§ π₯ β π) β π₯ β π) |
13 | | eqid 2733 |
. . . . . . 7
β’
(Scalarβπ) =
(Scalarβπ) |
14 | | eqid 2733 |
. . . . . . 7
β’
(Β·πβπ) =
(Β·πβπ) |
15 | | eqid 2733 |
. . . . . . 7
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
16 | 13, 14, 1, 15, 8 | ip0l 21056 |
. . . . . 6
β’ ((π β PreHil β§ π₯ β π) β ((0gβπ)(Β·πβπ)π₯) = (0gβ(Scalarβπ))) |
17 | 11, 12, 16 | syl2anc 585 |
. . . . 5
β’ (((π β PreHil β§ π β π) β§ π₯ β π) β ((0gβπ)(Β·πβπ)π₯) = (0gβ(Scalarβπ))) |
18 | 17 | ralrimiva 3140 |
. . . 4
β’ ((π β PreHil β§ π β π) β βπ₯ β π ((0gβπ)(Β·πβπ)π₯) = (0gβ(Scalarβπ))) |
19 | 1, 14, 13, 15, 2 | elocv 21088 |
. . . 4
β’
((0gβπ) β ( β₯ βπ) β (π β π β§ (0gβπ) β π β§ βπ₯ β π ((0gβπ)(Β·πβπ)π₯) = (0gβ(Scalarβπ)))) |
20 | 5, 10, 18, 19 | syl3anbrc 1344 |
. . 3
β’ ((π β PreHil β§ π β π) β (0gβπ) β ( β₯ βπ)) |
21 | 20 | ne0d 4296 |
. 2
β’ ((π β PreHil β§ π β π) β ( β₯ βπ) β β
) |
22 | 5 | adantr 482 |
. . . 4
β’ (((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β π β π) |
23 | 7 | adantr 482 |
. . . . 5
β’ (((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β π β LMod) |
24 | | simpr1 1195 |
. . . . . 6
β’ (((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β π β (Baseβ(Scalarβπ))) |
25 | | simpr2 1196 |
. . . . . . 7
β’ (((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β π¦ β ( β₯ βπ)) |
26 | 3, 25 | sselid 3943 |
. . . . . 6
β’ (((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β π¦ β π) |
27 | | eqid 2733 |
. . . . . . 7
β’ (
Β·π βπ) = ( Β·π
βπ) |
28 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
29 | 1, 13, 27, 28 | lmodvscl 20354 |
. . . . . 6
β’ ((π β LMod β§ π β
(Baseβ(Scalarβπ)) β§ π¦ β π) β (π( Β·π
βπ)π¦) β π) |
30 | 23, 24, 26, 29 | syl3anc 1372 |
. . . . 5
β’ (((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β (π( Β·π
βπ)π¦) β π) |
31 | | simpr3 1197 |
. . . . . 6
β’ (((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β π§ β ( β₯ βπ)) |
32 | 3, 31 | sselid 3943 |
. . . . 5
β’ (((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β π§ β π) |
33 | | eqid 2733 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
34 | 1, 33 | lmodvacl 20351 |
. . . . 5
β’ ((π β LMod β§ (π(
Β·π βπ)π¦) β π β§ π§ β π) β ((π( Β·π
βπ)π¦)(+gβπ)π§) β π) |
35 | 23, 30, 32, 34 | syl3anc 1372 |
. . . 4
β’ (((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β ((π( Β·π
βπ)π¦)(+gβπ)π§) β π) |
36 | 11 | adantlr 714 |
. . . . . . 7
β’ ((((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β§ π₯ β π) β π β PreHil) |
37 | 30 | adantr 482 |
. . . . . . 7
β’ ((((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β§ π₯ β π) β (π( Β·π
βπ)π¦) β π) |
38 | 32 | adantr 482 |
. . . . . . 7
β’ ((((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β§ π₯ β π) β π§ β π) |
39 | 12 | adantlr 714 |
. . . . . . 7
β’ ((((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β§ π₯ β π) β π₯ β π) |
40 | | eqid 2733 |
. . . . . . . 8
β’
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ)) |
41 | 13, 14, 1, 33, 40 | ipdir 21059 |
. . . . . . 7
β’ ((π β PreHil β§ ((π(
Β·π βπ)π¦) β π β§ π§ β π β§ π₯ β π)) β (((π( Β·π
βπ)π¦)(+gβπ)π§)(Β·πβπ)π₯) = (((π( Β·π
βπ)π¦)(Β·πβπ)π₯)(+gβ(Scalarβπ))(π§(Β·πβπ)π₯))) |
42 | 36, 37, 38, 39, 41 | syl13anc 1373 |
. . . . . 6
β’ ((((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β§ π₯ β π) β (((π( Β·π
βπ)π¦)(+gβπ)π§)(Β·πβπ)π₯) = (((π( Β·π
βπ)π¦)(Β·πβπ)π₯)(+gβ(Scalarβπ))(π§(Β·πβπ)π₯))) |
43 | 24 | adantr 482 |
. . . . . . . . 9
β’ ((((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β§ π₯ β π) β π β (Baseβ(Scalarβπ))) |
44 | 26 | adantr 482 |
. . . . . . . . 9
β’ ((((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β§ π₯ β π) β π¦ β π) |
45 | | eqid 2733 |
. . . . . . . . . 10
β’
(.rβ(Scalarβπ)) =
(.rβ(Scalarβπ)) |
46 | 13, 14, 1, 28, 27, 45 | ipass 21065 |
. . . . . . . . 9
β’ ((π β PreHil β§ (π β
(Baseβ(Scalarβπ)) β§ π¦ β π β§ π₯ β π)) β ((π( Β·π
βπ)π¦)(Β·πβπ)π₯) = (π(.rβ(Scalarβπ))(π¦(Β·πβπ)π₯))) |
47 | 36, 43, 44, 39, 46 | syl13anc 1373 |
. . . . . . . 8
β’ ((((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β§ π₯ β π) β ((π( Β·π
βπ)π¦)(Β·πβπ)π₯) = (π(.rβ(Scalarβπ))(π¦(Β·πβπ)π₯))) |
48 | 1, 14, 13, 15, 2 | ocvi 21089 |
. . . . . . . . . 10
β’ ((π¦ β ( β₯ βπ) β§ π₯ β π) β (π¦(Β·πβπ)π₯) = (0gβ(Scalarβπ))) |
49 | 25, 48 | sylan 581 |
. . . . . . . . 9
β’ ((((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β§ π₯ β π) β (π¦(Β·πβπ)π₯) = (0gβ(Scalarβπ))) |
50 | 49 | oveq2d 7374 |
. . . . . . . 8
β’ ((((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β§ π₯ β π) β (π(.rβ(Scalarβπ))(π¦(Β·πβπ)π₯)) = (π(.rβ(Scalarβπ))(0gβ(Scalarβπ)))) |
51 | 23 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β§ π₯ β π) β π β LMod) |
52 | 13 | lmodring 20344 |
. . . . . . . . . 10
β’ (π β LMod β
(Scalarβπ) β
Ring) |
53 | 51, 52 | syl 17 |
. . . . . . . . 9
β’ ((((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β§ π₯ β π) β (Scalarβπ) β Ring) |
54 | 28, 45, 15 | ringrz 20017 |
. . . . . . . . 9
β’
(((Scalarβπ)
β Ring β§ π β
(Baseβ(Scalarβπ))) β (π(.rβ(Scalarβπ))(0gβ(Scalarβπ))) =
(0gβ(Scalarβπ))) |
55 | 53, 43, 54 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β§ π₯ β π) β (π(.rβ(Scalarβπ))(0gβ(Scalarβπ))) =
(0gβ(Scalarβπ))) |
56 | 47, 50, 55 | 3eqtrd 2777 |
. . . . . . 7
β’ ((((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β§ π₯ β π) β ((π( Β·π
βπ)π¦)(Β·πβπ)π₯) = (0gβ(Scalarβπ))) |
57 | 1, 14, 13, 15, 2 | ocvi 21089 |
. . . . . . . 8
β’ ((π§ β ( β₯ βπ) β§ π₯ β π) β (π§(Β·πβπ)π₯) = (0gβ(Scalarβπ))) |
58 | 31, 57 | sylan 581 |
. . . . . . 7
β’ ((((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β§ π₯ β π) β (π§(Β·πβπ)π₯) = (0gβ(Scalarβπ))) |
59 | 56, 58 | oveq12d 7376 |
. . . . . 6
β’ ((((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β§ π₯ β π) β (((π( Β·π
βπ)π¦)(Β·πβπ)π₯)(+gβ(Scalarβπ))(π§(Β·πβπ)π₯)) = ((0gβ(Scalarβπ))(+gβ(Scalarβπ))(0gβ(Scalarβπ)))) |
60 | 13 | lmodfgrp 20345 |
. . . . . . 7
β’ (π β LMod β
(Scalarβπ) β
Grp) |
61 | 28, 15 | grpidcl 18783 |
. . . . . . . 8
β’
((Scalarβπ)
β Grp β (0gβ(Scalarβπ)) β (Baseβ(Scalarβπ))) |
62 | 28, 40, 15 | grplid 18785 |
. . . . . . . 8
β’
(((Scalarβπ)
β Grp β§ (0gβ(Scalarβπ)) β (Baseβ(Scalarβπ))) β
((0gβ(Scalarβπ))(+gβ(Scalarβπ))(0gβ(Scalarβπ))) =
(0gβ(Scalarβπ))) |
63 | 61, 62 | mpdan 686 |
. . . . . . 7
β’
((Scalarβπ)
β Grp β ((0gβ(Scalarβπ))(+gβ(Scalarβπ))(0gβ(Scalarβπ))) =
(0gβ(Scalarβπ))) |
64 | 51, 60, 63 | 3syl 18 |
. . . . . 6
β’ ((((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β§ π₯ β π) β
((0gβ(Scalarβπ))(+gβ(Scalarβπ))(0gβ(Scalarβπ))) =
(0gβ(Scalarβπ))) |
65 | 42, 59, 64 | 3eqtrd 2777 |
. . . . 5
β’ ((((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β§ π₯ β π) β (((π( Β·π
βπ)π¦)(+gβπ)π§)(Β·πβπ)π₯) = (0gβ(Scalarβπ))) |
66 | 65 | ralrimiva 3140 |
. . . 4
β’ (((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β βπ₯ β π (((π( Β·π
βπ)π¦)(+gβπ)π§)(Β·πβπ)π₯) = (0gβ(Scalarβπ))) |
67 | 1, 14, 13, 15, 2 | elocv 21088 |
. . . 4
β’ (((π(
Β·π βπ)π¦)(+gβπ)π§) β ( β₯ βπ) β (π β π β§ ((π( Β·π
βπ)π¦)(+gβπ)π§) β π β§ βπ₯ β π (((π( Β·π
βπ)π¦)(+gβπ)π§)(Β·πβπ)π₯) = (0gβ(Scalarβπ)))) |
68 | 22, 35, 66, 67 | syl3anbrc 1344 |
. . 3
β’ (((π β PreHil β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π¦ β ( β₯ βπ) β§ π§ β ( β₯ βπ))) β ((π( Β·π
βπ)π¦)(+gβπ)π§) β ( β₯ βπ)) |
69 | 68 | ralrimivvva 3197 |
. 2
β’ ((π β PreHil β§ π β π) β βπ β (Baseβ(Scalarβπ))βπ¦ β ( β₯ βπ)βπ§ β ( β₯ βπ)((π( Β·π
βπ)π¦)(+gβπ)π§) β ( β₯ βπ)) |
70 | | ocvlss.l |
. . 3
β’ πΏ = (LSubSpβπ) |
71 | 13, 28, 1, 33, 27, 70 | islss 20410 |
. 2
β’ (( β₯
βπ) β πΏ β (( β₯ βπ) β π β§ ( β₯ βπ) β β
β§
βπ β
(Baseβ(Scalarβπ))βπ¦ β ( β₯ βπ)βπ§ β ( β₯ βπ)((π( Β·π
βπ)π¦)(+gβπ)π§) β ( β₯ βπ))) |
72 | 4, 21, 69, 71 | syl3anbrc 1344 |
1
β’ ((π β PreHil β§ π β π) β ( β₯ βπ) β πΏ) |