Step | Hyp | Ref
| Expression |
1 | | prjsprel.1 |
. . 3
β’ βΌ =
{β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} |
2 | 1 | prjsprel 41033 |
. 2
β’ (π βΌ π β ((π β π΅ β§ π β π΅) β§ βπ β πΎ π = (π Β· π))) |
3 | | simprl 769 |
. . . . . . . 8
β’ (((π β LVec β§ (π β π΅ β§ π β π΅)) β§ (π β πΎ β§ π = (π Β· π))) β π β πΎ) |
4 | | simplrl 775 |
. . . . . . . . . . 11
β’ (((π β LVec β§ (π β π΅ β§ π β π΅)) β§ (π β πΎ β§ π = (π Β· π))) β π β π΅) |
5 | | eldifsni 4770 |
. . . . . . . . . . . 12
β’ (π β ((Baseβπ) β
{(0gβπ)})
β π β
(0gβπ)) |
6 | | prjspertr.b |
. . . . . . . . . . . 12
β’ π΅ = ((Baseβπ) β
{(0gβπ)}) |
7 | 5, 6 | eleq2s 2850 |
. . . . . . . . . . 11
β’ (π β π΅ β π β (0gβπ)) |
8 | 4, 7 | syl 17 |
. . . . . . . . . 10
β’ (((π β LVec β§ (π β π΅ β§ π β π΅)) β§ (π β πΎ β§ π = (π Β· π))) β π β (0gβπ)) |
9 | | simplrr 776 |
. . . . . . . . . . 11
β’ ((((π β LVec β§ (π β π΅ β§ π β π΅)) β§ (π β πΎ β§ π = (π Β· π))) β§ π = 0 ) β π = (π Β· π)) |
10 | | simpr 485 |
. . . . . . . . . . . 12
β’ ((((π β LVec β§ (π β π΅ β§ π β π΅)) β§ (π β πΎ β§ π = (π Β· π))) β§ π = 0 ) β π = 0 ) |
11 | 10 | oveq1d 7392 |
. . . . . . . . . . 11
β’ ((((π β LVec β§ (π β π΅ β§ π β π΅)) β§ (π β πΎ β§ π = (π Β· π))) β§ π = 0 ) β (π Β· π) = ( 0 Β· π)) |
12 | | lveclmod 20639 |
. . . . . . . . . . . . 13
β’ (π β LVec β π β LMod) |
13 | 12 | ad3antrrr 728 |
. . . . . . . . . . . 12
β’ ((((π β LVec β§ (π β π΅ β§ π β π΅)) β§ (π β πΎ β§ π = (π Β· π))) β§ π = 0 ) β π β LMod) |
14 | | difss 4111 |
. . . . . . . . . . . . . 14
β’
((Baseβπ)
β {(0gβπ)}) β (Baseβπ) |
15 | 6, 14 | eqsstri 3996 |
. . . . . . . . . . . . 13
β’ π΅ β (Baseβπ) |
16 | | simplrr 776 |
. . . . . . . . . . . . . 14
β’ (((π β LVec β§ (π β π΅ β§ π β π΅)) β§ ((π β πΎ β§ π = (π Β· π)) β§ π = 0 )) β π β π΅) |
17 | 16 | anassrs 468 |
. . . . . . . . . . . . 13
β’ ((((π β LVec β§ (π β π΅ β§ π β π΅)) β§ (π β πΎ β§ π = (π Β· π))) β§ π = 0 ) β π β π΅) |
18 | 15, 17 | sselid 3960 |
. . . . . . . . . . . 12
β’ ((((π β LVec β§ (π β π΅ β§ π β π΅)) β§ (π β πΎ β§ π = (π Β· π))) β§ π = 0 ) β π β (Baseβπ)) |
19 | | eqid 2731 |
. . . . . . . . . . . . 13
β’
(Baseβπ) =
(Baseβπ) |
20 | | prjspertr.s |
. . . . . . . . . . . . 13
β’ π = (Scalarβπ) |
21 | | prjspertr.x |
. . . . . . . . . . . . 13
β’ Β· = (
Β·π βπ) |
22 | | prjspreln0.z |
. . . . . . . . . . . . 13
β’ 0 =
(0gβπ) |
23 | | eqid 2731 |
. . . . . . . . . . . . 13
β’
(0gβπ) = (0gβπ) |
24 | 19, 20, 21, 22, 23 | lmod0vs 20427 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ π β (Baseβπ)) β ( 0 Β· π) = (0gβπ)) |
25 | 13, 18, 24 | syl2anc 584 |
. . . . . . . . . . 11
β’ ((((π β LVec β§ (π β π΅ β§ π β π΅)) β§ (π β πΎ β§ π = (π Β· π))) β§ π = 0 ) β ( 0 Β· π) = (0gβπ)) |
26 | 9, 11, 25 | 3eqtrd 2775 |
. . . . . . . . . 10
β’ ((((π β LVec β§ (π β π΅ β§ π β π΅)) β§ (π β πΎ β§ π = (π Β· π))) β§ π = 0 ) β π = (0gβπ)) |
27 | 8, 26 | mteqand 3032 |
. . . . . . . . 9
β’ (((π β LVec β§ (π β π΅ β§ π β π΅)) β§ (π β πΎ β§ π = (π Β· π))) β π β 0 ) |
28 | | nelsn 4646 |
. . . . . . . . 9
β’ (π β 0 β Β¬ π β { 0 }) |
29 | 27, 28 | syl 17 |
. . . . . . . 8
β’ (((π β LVec β§ (π β π΅ β§ π β π΅)) β§ (π β πΎ β§ π = (π Β· π))) β Β¬ π β { 0 }) |
30 | 3, 29 | eldifd 3939 |
. . . . . . 7
β’ (((π β LVec β§ (π β π΅ β§ π β π΅)) β§ (π β πΎ β§ π = (π Β· π))) β π β (πΎ β { 0 })) |
31 | 30 | ex 413 |
. . . . . 6
β’ ((π β LVec β§ (π β π΅ β§ π β π΅)) β ((π β πΎ β§ π = (π Β· π)) β π β (πΎ β { 0 }))) |
32 | | simpr 485 |
. . . . . 6
β’ ((π β πΎ β§ π = (π Β· π)) β π = (π Β· π)) |
33 | 31, 32 | jca2 514 |
. . . . 5
β’ ((π β LVec β§ (π β π΅ β§ π β π΅)) β ((π β πΎ β§ π = (π Β· π)) β (π β (πΎ β { 0 }) β§ π = (π Β· π)))) |
34 | 33 | reximdv2 3163 |
. . . 4
β’ ((π β LVec β§ (π β π΅ β§ π β π΅)) β (βπ β πΎ π = (π Β· π) β βπ β (πΎ β { 0 })π = (π Β· π))) |
35 | | difss 4111 |
. . . . 5
β’ (πΎ β { 0 }) β πΎ |
36 | | ssrexv 4031 |
. . . . 5
β’ ((πΎ β { 0 }) β πΎ β (βπ β (πΎ β { 0 })π = (π Β· π) β βπ β πΎ π = (π Β· π))) |
37 | 35, 36 | mp1i 13 |
. . . 4
β’ ((π β LVec β§ (π β π΅ β§ π β π΅)) β (βπ β (πΎ β { 0 })π = (π Β· π) β βπ β πΎ π = (π Β· π))) |
38 | 34, 37 | impbid 211 |
. . 3
β’ ((π β LVec β§ (π β π΅ β§ π β π΅)) β (βπ β πΎ π = (π Β· π) β βπ β (πΎ β { 0 })π = (π Β· π))) |
39 | 38 | pm5.32da 579 |
. 2
β’ (π β LVec β (((π β π΅ β§ π β π΅) β§ βπ β πΎ π = (π Β· π)) β ((π β π΅ β§ π β π΅) β§ βπ β (πΎ β { 0 })π = (π Β· π)))) |
40 | 2, 39 | bitrid 282 |
1
β’ (π β LVec β (π βΌ π β ((π β π΅ β§ π β π΅) β§ βπ β (πΎ β { 0 })π = (π Β· π)))) |