Step | Hyp | Ref
| Expression |
1 | | prjsprel.1 |
. . . . . . 7
β’ βΌ =
{β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} |
2 | 1 | cnveqi 5875 |
. . . . . 6
β’ β‘ βΌ = β‘{β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} |
3 | | cnvopab 6139 |
. . . . . 6
β’ β‘{β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} = {β¨π¦, π₯β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} |
4 | 2, 3 | eqtri 2761 |
. . . . 5
β’ β‘ βΌ = {β¨π¦, π₯β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} |
5 | 4 | eceq2i 8744 |
. . . 4
β’ [π]β‘ βΌ = [π]{β¨π¦, π₯β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} |
6 | | df-ec 8705 |
. . . . . 6
β’ [π]{β¨π¦, π₯β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} = ({β¨π¦, π₯β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} β {π}) |
7 | 6 | a1i 11 |
. . . . 5
β’ ((π β LVec β§ π β π΅) β [π]{β¨π¦, π₯β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} = ({β¨π¦, π₯β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} β {π})) |
8 | | imaopab 41050 |
. . . . . 6
β’
({β¨π¦, π₯β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} β {π}) = {π₯ β£ βπ¦ β {π} ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} |
9 | 8 | a1i 11 |
. . . . 5
β’ ((π β LVec β§ π β π΅) β ({β¨π¦, π₯β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} β {π}) = {π₯ β£ βπ¦ β {π} ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))}) |
10 | | df-rex 3072 |
. . . . . . . . 9
β’
(βπ¦ β
{π} ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦)) β βπ¦(π¦ β {π} β§ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦)))) |
11 | | velsn 4645 |
. . . . . . . . . . . 12
β’ (π¦ β {π} β π¦ = π) |
12 | 11 | anbi1i 625 |
. . . . . . . . . . 11
β’ ((π¦ β {π} β§ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))) β (π¦ = π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦)))) |
13 | | eleq1 2822 |
. . . . . . . . . . . . . 14
β’ (π¦ = π β (π¦ β π΅ β π β π΅)) |
14 | 13 | anbi2d 630 |
. . . . . . . . . . . . 13
β’ (π¦ = π β ((π₯ β π΅ β§ π¦ β π΅) β (π₯ β π΅ β§ π β π΅))) |
15 | | oveq2 7417 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β (π Β· π¦) = (π Β· π)) |
16 | 15 | eqeq2d 2744 |
. . . . . . . . . . . . . 14
β’ (π¦ = π β (π₯ = (π Β· π¦) β π₯ = (π Β· π))) |
17 | 16 | rexbidv 3179 |
. . . . . . . . . . . . 13
β’ (π¦ = π β (βπ β πΎ π₯ = (π Β· π¦) β βπ β πΎ π₯ = (π Β· π))) |
18 | 14, 17 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π¦ = π β (((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦)) β ((π₯ β π΅ β§ π β π΅) β§ βπ β πΎ π₯ = (π Β· π)))) |
19 | 18 | pm5.32i 576 |
. . . . . . . . . . 11
β’ ((π¦ = π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))) β (π¦ = π β§ ((π₯ β π΅ β§ π β π΅) β§ βπ β πΎ π₯ = (π Β· π)))) |
20 | 12, 19 | bitri 275 |
. . . . . . . . . 10
β’ ((π¦ β {π} β§ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))) β (π¦ = π β§ ((π₯ β π΅ β§ π β π΅) β§ βπ β πΎ π₯ = (π Β· π)))) |
21 | 20 | exbii 1851 |
. . . . . . . . 9
β’
(βπ¦(π¦ β {π} β§ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))) β βπ¦(π¦ = π β§ ((π₯ β π΅ β§ π β π΅) β§ βπ β πΎ π₯ = (π Β· π)))) |
22 | | 19.41v 1954 |
. . . . . . . . . 10
β’
(βπ¦(π¦ = π β§ ((π₯ β π΅ β§ π β π΅) β§ βπ β πΎ π₯ = (π Β· π))) β (βπ¦ π¦ = π β§ ((π₯ β π΅ β§ π β π΅) β§ βπ β πΎ π₯ = (π Β· π)))) |
23 | | elisset 2816 |
. . . . . . . . . . . 12
β’ (π β π΅ β βπ¦ π¦ = π) |
24 | 23 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π₯ β π΅ β§ π β π΅) β§ βπ β πΎ π₯ = (π Β· π)) β βπ¦ π¦ = π) |
25 | 24 | pm4.71ri 562 |
. . . . . . . . . 10
β’ (((π₯ β π΅ β§ π β π΅) β§ βπ β πΎ π₯ = (π Β· π)) β (βπ¦ π¦ = π β§ ((π₯ β π΅ β§ π β π΅) β§ βπ β πΎ π₯ = (π Β· π)))) |
26 | 22, 25 | bitr4i 278 |
. . . . . . . . 9
β’
(βπ¦(π¦ = π β§ ((π₯ β π΅ β§ π β π΅) β§ βπ β πΎ π₯ = (π Β· π))) β ((π₯ β π΅ β§ π β π΅) β§ βπ β πΎ π₯ = (π Β· π))) |
27 | 10, 21, 26 | 3bitri 297 |
. . . . . . . 8
β’
(βπ¦ β
{π} ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦)) β ((π₯ β π΅ β§ π β π΅) β§ βπ β πΎ π₯ = (π Β· π))) |
28 | 27 | abbii 2803 |
. . . . . . 7
β’ {π₯ β£ βπ¦ β {π} ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} = {π₯ β£ ((π₯ β π΅ β§ π β π΅) β§ βπ β πΎ π₯ = (π Β· π))} |
29 | | iba 529 |
. . . . . . . . . 10
β’ (π β π΅ β (π₯ β π΅ β (π₯ β π΅ β§ π β π΅))) |
30 | 29 | bicomd 222 |
. . . . . . . . 9
β’ (π β π΅ β ((π₯ β π΅ β§ π β π΅) β π₯ β π΅)) |
31 | 30 | anbi1d 631 |
. . . . . . . 8
β’ (π β π΅ β (((π₯ β π΅ β§ π β π΅) β§ βπ β πΎ π₯ = (π Β· π)) β (π₯ β π΅ β§ βπ β πΎ π₯ = (π Β· π)))) |
32 | 31 | abbidv 2802 |
. . . . . . 7
β’ (π β π΅ β {π₯ β£ ((π₯ β π΅ β§ π β π΅) β§ βπ β πΎ π₯ = (π Β· π))} = {π₯ β£ (π₯ β π΅ β§ βπ β πΎ π₯ = (π Β· π))}) |
33 | 28, 32 | eqtrid 2785 |
. . . . . 6
β’ (π β π΅ β {π₯ β£ βπ¦ β {π} ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} = {π₯ β£ (π₯ β π΅ β§ βπ β πΎ π₯ = (π Β· π))}) |
34 | 33 | adantl 483 |
. . . . 5
β’ ((π β LVec β§ π β π΅) β {π₯ β£ βπ¦ β {π} ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} = {π₯ β£ (π₯ β π΅ β§ βπ β πΎ π₯ = (π Β· π))}) |
35 | 7, 9, 34 | 3eqtrd 2777 |
. . . 4
β’ ((π β LVec β§ π β π΅) β [π]{β¨π¦, π₯β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} = {π₯ β£ (π₯ β π΅ β§ βπ β πΎ π₯ = (π Β· π))}) |
36 | 5, 35 | eqtrid 2785 |
. . 3
β’ ((π β LVec β§ π β π΅) β [π]β‘
βΌ
= {π₯ β£ (π₯ β π΅ β§ βπ β πΎ π₯ = (π Β· π))}) |
37 | | df-rab 3434 |
. . . 4
β’ {π₯ β π΅ β£ βπ β πΎ π₯ = (π Β· π)} = {π₯ β£ (π₯ β π΅ β§ βπ β πΎ π₯ = (π Β· π))} |
38 | 37 | a1i 11 |
. . 3
β’ ((π β LVec β§ π β π΅) β {π₯ β π΅ β£ βπ β πΎ π₯ = (π Β· π)} = {π₯ β£ (π₯ β π΅ β§ βπ β πΎ π₯ = (π Β· π))}) |
39 | | prjspertr.b |
. . . . 5
β’ π΅ = ((Baseβπ) β
{(0gβπ)}) |
40 | 39 | rabeqi 3446 |
. . . 4
β’ {π₯ β π΅ β£ βπ β πΎ π₯ = (π Β· π)} = {π₯ β ((Baseβπ) β {(0gβπ)}) β£ βπ β πΎ π₯ = (π Β· π)} |
41 | | rabdif 41032 |
. . . . 5
β’ ({π₯ β (Baseβπ) β£ βπ β πΎ π₯ = (π Β· π)} β {(0gβπ)}) = {π₯ β ((Baseβπ) β {(0gβπ)}) β£ βπ β πΎ π₯ = (π Β· π)} |
42 | 41 | a1i 11 |
. . . 4
β’ ((π β LVec β§ π β π΅) β ({π₯ β (Baseβπ) β£ βπ β πΎ π₯ = (π Β· π)} β {(0gβπ)}) = {π₯ β ((Baseβπ) β {(0gβπ)}) β£ βπ β πΎ π₯ = (π Β· π)}) |
43 | 40, 42 | eqtr4id 2792 |
. . 3
β’ ((π β LVec β§ π β π΅) β {π₯ β π΅ β£ βπ β πΎ π₯ = (π Β· π)} = ({π₯ β (Baseβπ) β£ βπ β πΎ π₯ = (π Β· π)} β {(0gβπ)})) |
44 | 36, 38, 43 | 3eqtr2d 2779 |
. 2
β’ ((π β LVec β§ π β π΅) β [π]β‘
βΌ
= ({π₯ β
(Baseβπ) β£
βπ β πΎ π₯ = (π Β· π)} β {(0gβπ)})) |
45 | | prjspertr.s |
. . . . . 6
β’ π = (Scalarβπ) |
46 | | prjspertr.x |
. . . . . 6
β’ Β· = (
Β·π βπ) |
47 | | prjspertr.k |
. . . . . 6
β’ πΎ = (Baseβπ) |
48 | 1, 39, 45, 46, 47 | prjsper 41350 |
. . . . 5
β’ (π β LVec β βΌ Er
π΅) |
49 | 48 | adantr 482 |
. . . 4
β’ ((π β LVec β§ π β π΅) β βΌ Er π΅) |
50 | | ercnv 8724 |
. . . . 5
β’ ( βΌ Er
π΅ β β‘ βΌ = βΌ
) |
51 | 50 | eqcomd 2739 |
. . . 4
β’ ( βΌ Er
π΅ β βΌ = β‘ βΌ ) |
52 | 49, 51 | syl 17 |
. . 3
β’ ((π β LVec β§ π β π΅) β βΌ = β‘ βΌ ) |
53 | 52 | eceq2d 8745 |
. 2
β’ ((π β LVec β§ π β π΅) β [π] βΌ = [π]β‘ βΌ ) |
54 | | lveclmod 20717 |
. . . . 5
β’ (π β LVec β π β LMod) |
55 | | difss 4132 |
. . . . . . 7
β’
((Baseβπ)
β {(0gβπ)}) β (Baseβπ) |
56 | 39, 55 | eqsstri 4017 |
. . . . . 6
β’ π΅ β (Baseβπ) |
57 | 56 | sseli 3979 |
. . . . 5
β’ (π β π΅ β π β (Baseβπ)) |
58 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
59 | | prjsprellsp.n |
. . . . . 6
β’ π = (LSpanβπ) |
60 | 45, 47, 58, 46, 59 | lspsn 20613 |
. . . . 5
β’ ((π β LMod β§ π β (Baseβπ)) β (πβ{π}) = {π₯ β£ βπ β πΎ π₯ = (π Β· π)}) |
61 | 54, 57, 60 | syl2an 597 |
. . . 4
β’ ((π β LVec β§ π β π΅) β (πβ{π}) = {π₯ β£ βπ β πΎ π₯ = (π Β· π)}) |
62 | | simpr 486 |
. . . . . . . . 9
β’ ((((π β LVec β§ π β π΅) β§ π β πΎ) β§ π₯ = (π Β· π)) β π₯ = (π Β· π)) |
63 | 54 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β LVec β§ π β π΅) β π β LMod) |
64 | 63 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β LVec β§ π β π΅) β§ π β πΎ) β π β LMod) |
65 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β LVec β§ π β π΅) β§ π β πΎ) β π β πΎ) |
66 | 57 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β LVec β§ π β π΅) β§ π β πΎ) β π β (Baseβπ)) |
67 | 58, 45, 46, 47, 64, 65, 66 | lmodvscld 41104 |
. . . . . . . . . 10
β’ (((π β LVec β§ π β π΅) β§ π β πΎ) β (π Β· π) β (Baseβπ)) |
68 | 67 | adantr 482 |
. . . . . . . . 9
β’ ((((π β LVec β§ π β π΅) β§ π β πΎ) β§ π₯ = (π Β· π)) β (π Β· π) β (Baseβπ)) |
69 | 62, 68 | eqeltrd 2834 |
. . . . . . . 8
β’ ((((π β LVec β§ π β π΅) β§ π β πΎ) β§ π₯ = (π Β· π)) β π₯ β (Baseβπ)) |
70 | 69 | rexlimdva2 3158 |
. . . . . . 7
β’ ((π β LVec β§ π β π΅) β (βπ β πΎ π₯ = (π Β· π) β π₯ β (Baseβπ))) |
71 | 70 | pm4.71rd 564 |
. . . . . 6
β’ ((π β LVec β§ π β π΅) β (βπ β πΎ π₯ = (π Β· π) β (π₯ β (Baseβπ) β§ βπ β πΎ π₯ = (π Β· π)))) |
72 | 71 | abbidv 2802 |
. . . . 5
β’ ((π β LVec β§ π β π΅) β {π₯ β£ βπ β πΎ π₯ = (π Β· π)} = {π₯ β£ (π₯ β (Baseβπ) β§ βπ β πΎ π₯ = (π Β· π))}) |
73 | | df-rab 3434 |
. . . . 5
β’ {π₯ β (Baseβπ) β£ βπ β πΎ π₯ = (π Β· π)} = {π₯ β£ (π₯ β (Baseβπ) β§ βπ β πΎ π₯ = (π Β· π))} |
74 | 72, 73 | eqtr4di 2791 |
. . . 4
β’ ((π β LVec β§ π β π΅) β {π₯ β£ βπ β πΎ π₯ = (π Β· π)} = {π₯ β (Baseβπ) β£ βπ β πΎ π₯ = (π Β· π)}) |
75 | 61, 74 | eqtrd 2773 |
. . 3
β’ ((π β LVec β§ π β π΅) β (πβ{π}) = {π₯ β (Baseβπ) β£ βπ β πΎ π₯ = (π Β· π)}) |
76 | 75 | difeq1d 4122 |
. 2
β’ ((π β LVec β§ π β π΅) β ((πβ{π}) β {(0gβπ)}) = ({π₯ β (Baseβπ) β£ βπ β πΎ π₯ = (π Β· π)} β {(0gβπ)})) |
77 | 44, 53, 76 | 3eqtr4d 2783 |
1
β’ ((π β LVec β§ π β π΅) β [π] βΌ = ((πβ{π}) β {(0gβπ)})) |