Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
2 | | eqid 2733 |
. . . . . . . . 9
β’
(Β·πβπ) =
(Β·πβπ) |
3 | | eqid 2733 |
. . . . . . . . 9
β’
(Scalarβπ) =
(Scalarβπ) |
4 | | eqid 2733 |
. . . . . . . . 9
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
5 | | ocv2ss.o |
. . . . . . . . 9
β’ β₯ =
(ocvβπ) |
6 | 1, 2, 3, 4, 5 | ocvi 21089 |
. . . . . . . 8
β’ ((π₯ β ( β₯ βπ) β§ π₯ β π) β (π₯(Β·πβπ)π₯) = (0gβ(Scalarβπ))) |
7 | 6 | ancoms 460 |
. . . . . . 7
β’ ((π₯ β π β§ π₯ β ( β₯ βπ)) β (π₯(Β·πβπ)π₯) = (0gβ(Scalarβπ))) |
8 | 7 | adantl 483 |
. . . . . 6
β’ (((π β PreHil β§ π β πΏ) β§ (π₯ β π β§ π₯ β ( β₯ βπ))) β (π₯(Β·πβπ)π₯) = (0gβ(Scalarβπ))) |
9 | | simpll 766 |
. . . . . . 7
β’ (((π β PreHil β§ π β πΏ) β§ (π₯ β π β§ π₯ β ( β₯ βπ))) β π β PreHil) |
10 | | ocvin.l |
. . . . . . . . 9
β’ πΏ = (LSubSpβπ) |
11 | 1, 10 | lssel 20413 |
. . . . . . . 8
β’ ((π β πΏ β§ π₯ β π) β π₯ β (Baseβπ)) |
12 | 11 | ad2ant2lr 747 |
. . . . . . 7
β’ (((π β PreHil β§ π β πΏ) β§ (π₯ β π β§ π₯ β ( β₯ βπ))) β π₯ β (Baseβπ)) |
13 | | ocvin.z |
. . . . . . . 8
β’ 0 =
(0gβπ) |
14 | 3, 2, 1, 4, 13 | ipeq0 21058 |
. . . . . . 7
β’ ((π β PreHil β§ π₯ β (Baseβπ)) β ((π₯(Β·πβπ)π₯) = (0gβ(Scalarβπ)) β π₯ = 0 )) |
15 | 9, 12, 14 | syl2anc 585 |
. . . . . 6
β’ (((π β PreHil β§ π β πΏ) β§ (π₯ β π β§ π₯ β ( β₯ βπ))) β ((π₯(Β·πβπ)π₯) = (0gβ(Scalarβπ)) β π₯ = 0 )) |
16 | 8, 15 | mpbid 231 |
. . . . 5
β’ (((π β PreHil β§ π β πΏ) β§ (π₯ β π β§ π₯ β ( β₯ βπ))) β π₯ = 0 ) |
17 | 16 | ex 414 |
. . . 4
β’ ((π β PreHil β§ π β πΏ) β ((π₯ β π β§ π₯ β ( β₯ βπ)) β π₯ = 0 )) |
18 | | elin 3927 |
. . . 4
β’ (π₯ β (π β© ( β₯ βπ)) β (π₯ β π β§ π₯ β ( β₯ βπ))) |
19 | | velsn 4603 |
. . . 4
β’ (π₯ β { 0 } β π₯ = 0 ) |
20 | 17, 18, 19 | 3imtr4g 296 |
. . 3
β’ ((π β PreHil β§ π β πΏ) β (π₯ β (π β© ( β₯ βπ)) β π₯ β { 0 })) |
21 | 20 | ssrdv 3951 |
. 2
β’ ((π β PreHil β§ π β πΏ) β (π β© ( β₯ βπ)) β { 0 }) |
22 | | phllmod 21050 |
. . 3
β’ (π β PreHil β π β LMod) |
23 | 1, 10 | lssss 20412 |
. . . . 5
β’ (π β πΏ β π β (Baseβπ)) |
24 | 1, 5, 10 | ocvlss 21092 |
. . . . 5
β’ ((π β PreHil β§ π β (Baseβπ)) β ( β₯ βπ) β πΏ) |
25 | 23, 24 | sylan2 594 |
. . . 4
β’ ((π β PreHil β§ π β πΏ) β ( β₯ βπ) β πΏ) |
26 | 10 | lssincl 20441 |
. . . . 5
β’ ((π β LMod β§ π β πΏ β§ ( β₯ βπ) β πΏ) β (π β© ( β₯ βπ)) β πΏ) |
27 | 22, 26 | syl3an1 1164 |
. . . 4
β’ ((π β PreHil β§ π β πΏ β§ ( β₯ βπ) β πΏ) β (π β© ( β₯ βπ)) β πΏ) |
28 | 25, 27 | mpd3an3 1463 |
. . 3
β’ ((π β PreHil β§ π β πΏ) β (π β© ( β₯ βπ)) β πΏ) |
29 | 13, 10 | lss0ss 20424 |
. . 3
β’ ((π β LMod β§ (π β© ( β₯ βπ)) β πΏ) β { 0 } β (π β© ( β₯ βπ))) |
30 | 22, 28, 29 | syl2an2r 684 |
. 2
β’ ((π β PreHil β§ π β πΏ) β { 0 } β (π β© ( β₯ βπ))) |
31 | 21, 30 | eqssd 3962 |
1
β’ ((π β PreHil β§ π β πΏ) β (π β© ( β₯ βπ)) = { 0 }) |