Step | Hyp | Ref
| Expression |
1 | | lveclmod 20611 |
. . . . . 6
β’ (π β LVec β π β LMod) |
2 | 1 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β LVec β§ π β π΅ β§ π β (πΎ β { 0 })) β π β LMod) |
3 | | eldifi 4090 |
. . . . . 6
β’ (π β (πΎ β { 0 }) β π β πΎ) |
4 | 3 | 3ad2ant3 1136 |
. . . . 5
β’ ((π β LVec β§ π β π΅ β§ π β (πΎ β { 0 })) β π β πΎ) |
5 | | prjspertr.b |
. . . . . . . 8
β’ π΅ = ((Baseβπ) β
{(0gβπ)}) |
6 | | difss 4095 |
. . . . . . . 8
β’
((Baseβπ)
β {(0gβπ)}) β (Baseβπ) |
7 | 5, 6 | eqsstri 3982 |
. . . . . . 7
β’ π΅ β (Baseβπ) |
8 | 7 | sseli 3944 |
. . . . . 6
β’ (π β π΅ β π β (Baseβπ)) |
9 | 8 | 3ad2ant2 1135 |
. . . . 5
β’ ((π β LVec β§ π β π΅ β§ π β (πΎ β { 0 })) β π β (Baseβπ)) |
10 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
11 | | prjspertr.s |
. . . . . 6
β’ π = (Scalarβπ) |
12 | | prjspertr.x |
. . . . . 6
β’ Β· = (
Β·π βπ) |
13 | | prjspertr.k |
. . . . . 6
β’ πΎ = (Baseβπ) |
14 | 10, 11, 12, 13 | lmodvscl 20383 |
. . . . 5
β’ ((π β LMod β§ π β πΎ β§ π β (Baseβπ)) β (π Β· π) β (Baseβπ)) |
15 | 2, 4, 9, 14 | syl3anc 1372 |
. . . 4
β’ ((π β LVec β§ π β π΅ β§ π β (πΎ β { 0 })) β (π Β· π) β (Baseβπ)) |
16 | | eldifsni 4754 |
. . . . . . 7
β’ (π β (πΎ β { 0 }) β π β 0 ) |
17 | 16 | 3ad2ant3 1136 |
. . . . . 6
β’ ((π β LVec β§ π β π΅ β§ π β (πΎ β { 0 })) β π β 0 ) |
18 | | eldifsni 4754 |
. . . . . . . 8
β’ (π β ((Baseβπ) β
{(0gβπ)})
β π β
(0gβπ)) |
19 | 18, 5 | eleq2s 2852 |
. . . . . . 7
β’ (π β π΅ β π β (0gβπ)) |
20 | 19 | 3ad2ant2 1135 |
. . . . . 6
β’ ((π β LVec β§ π β π΅ β§ π β (πΎ β { 0 })) β π β (0gβπ)) |
21 | | prjspreln0.z |
. . . . . . 7
β’ 0 =
(0gβπ) |
22 | | eqid 2733 |
. . . . . . 7
β’
(0gβπ) = (0gβπ) |
23 | | simp1 1137 |
. . . . . . 7
β’ ((π β LVec β§ π β π΅ β§ π β (πΎ β { 0 })) β π β LVec) |
24 | 10, 12, 11, 13, 21, 22, 23, 4, 9 | lvecvsn0 20615 |
. . . . . 6
β’ ((π β LVec β§ π β π΅ β§ π β (πΎ β { 0 })) β ((π Β· π) β (0gβπ) β (π β 0 β§ π β (0gβπ)))) |
25 | 17, 20, 24 | mpbir2and 712 |
. . . . 5
β’ ((π β LVec β§ π β π΅ β§ π β (πΎ β { 0 })) β (π Β· π) β (0gβπ)) |
26 | | nelsn 4630 |
. . . . 5
β’ ((π Β· π) β (0gβπ) β Β¬ (π Β· π) β {(0gβπ)}) |
27 | 25, 26 | syl 17 |
. . . 4
β’ ((π β LVec β§ π β π΅ β§ π β (πΎ β { 0 })) β Β¬ (π Β· π) β {(0gβπ)}) |
28 | 15, 27 | eldifd 3925 |
. . 3
β’ ((π β LVec β§ π β π΅ β§ π β (πΎ β { 0 })) β (π Β· π) β ((Baseβπ) β {(0gβπ)})) |
29 | 28, 5 | eleqtrrdi 2845 |
. 2
β’ ((π β LVec β§ π β π΅ β§ π β (πΎ β { 0 })) β (π Β· π) β π΅) |
30 | | simp2 1138 |
. 2
β’ ((π β LVec β§ π β π΅ β§ π β (πΎ β { 0 })) β π β π΅) |
31 | | oveq1 7368 |
. . . . . 6
β’ (π = π β (π Β· π) = (π Β· π)) |
32 | 31 | eqcoms 2741 |
. . . . 5
β’ (π = π β (π Β· π) = (π Β· π)) |
33 | | tbtru 1550 |
. . . . 5
β’ ((π Β· π) = (π Β· π) β ((π Β· π) = (π Β· π) β β€)) |
34 | 32, 33 | sylib 217 |
. . . 4
β’ (π = π β ((π Β· π) = (π Β· π) β β€)) |
35 | 34 | adantl 483 |
. . 3
β’ (((π β LVec β§ π β π΅ β§ π β (πΎ β { 0 })) β§ π = π) β ((π Β· π) = (π Β· π) β β€)) |
36 | | trud 1552 |
. . 3
β’ ((π β LVec β§ π β π΅ β§ π β (πΎ β { 0 })) β
β€) |
37 | 4, 35, 36 | rspcedvd 3585 |
. 2
β’ ((π β LVec β§ π β π΅ β§ π β (πΎ β { 0 })) β βπ β πΎ (π Β· π) = (π Β· π)) |
38 | | prjsprel.1 |
. . 3
β’ βΌ =
{β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} |
39 | 38 | prjsprel 40989 |
. 2
β’ ((π Β· π) βΌ π β (((π Β· π) β π΅ β§ π β π΅) β§ βπ β πΎ (π Β· π) = (π Β· π))) |
40 | 29, 30, 37, 39 | syl21anbrc 1345 |
1
β’ ((π β LVec β§ π β π΅ β§ π β (πΎ β { 0 })) β (π Β· π) βΌ π) |