Step | Hyp | Ref
| Expression |
1 | | fvex 6859 |
. . . . 5
β’
(Baseβπ£)
β V |
2 | 1 | difexi 5289 |
. . . 4
β’
((Baseβπ£)
β {(0gβπ£)}) β V |
3 | 2 | a1i 11 |
. . 3
β’ (π£ = π β ((Baseβπ£) β {(0gβπ£)}) β V) |
4 | | fveq2 6846 |
. . . . . . . . 9
β’ (π£ = π β (Baseβπ£) = (Baseβπ)) |
5 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π£ = π β (0gβπ£) = (0gβπ)) |
6 | 5 | sneqd 4602 |
. . . . . . . . 9
β’ (π£ = π β {(0gβπ£)} = {(0gβπ)}) |
7 | 4, 6 | difeq12d 4087 |
. . . . . . . 8
β’ (π£ = π β ((Baseβπ£) β {(0gβπ£)}) = ((Baseβπ) β
{(0gβπ)})) |
8 | | prjspval.b |
. . . . . . . 8
β’ π΅ = ((Baseβπ) β
{(0gβπ)}) |
9 | 7, 8 | eqtr4di 2791 |
. . . . . . 7
β’ (π£ = π β ((Baseβπ£) β {(0gβπ£)}) = π΅) |
10 | 9 | eqeq2d 2744 |
. . . . . 6
β’ (π£ = π β (π = ((Baseβπ£) β {(0gβπ£)}) β π = π΅)) |
11 | 10 | biimpd 228 |
. . . . 5
β’ (π£ = π β (π = ((Baseβπ£) β {(0gβπ£)}) β π = π΅)) |
12 | 11 | imp 408 |
. . . 4
β’ ((π£ = π β§ π = ((Baseβπ£) β {(0gβπ£)})) β π = π΅) |
13 | 11 | imdistani 570 |
. . . . . 6
β’ ((π£ = π β§ π = ((Baseβπ£) β {(0gβπ£)})) β (π£ = π β§ π = π΅)) |
14 | | eleq2 2823 |
. . . . . . . 8
β’ (π = π΅ β (π₯ β π β π₯ β π΅)) |
15 | | eleq2 2823 |
. . . . . . . 8
β’ (π = π΅ β (π¦ β π β π¦ β π΅)) |
16 | 14, 15 | anbi12d 632 |
. . . . . . 7
β’ (π = π΅ β ((π₯ β π β§ π¦ β π) β (π₯ β π΅ β§ π¦ β π΅))) |
17 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π£ = π β (Scalarβπ£) = (Scalarβπ)) |
18 | | prjspval.s |
. . . . . . . . . . 11
β’ π = (Scalarβπ) |
19 | 17, 18 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π£ = π β (Scalarβπ£) = π) |
20 | 19 | fveq2d 6850 |
. . . . . . . . 9
β’ (π£ = π β (Baseβ(Scalarβπ£)) = (Baseβπ)) |
21 | | prjspval.k |
. . . . . . . . 9
β’ πΎ = (Baseβπ) |
22 | 20, 21 | eqtr4di 2791 |
. . . . . . . 8
β’ (π£ = π β (Baseβ(Scalarβπ£)) = πΎ) |
23 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π£ = π β (
Β·π βπ£) = ( Β·π
βπ)) |
24 | | prjspval.x |
. . . . . . . . . . 11
β’ Β· = (
Β·π βπ) |
25 | 23, 24 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π£ = π β (
Β·π βπ£) = Β· ) |
26 | 25 | oveqd 7378 |
. . . . . . . . 9
β’ (π£ = π β (π( Β·π
βπ£)π¦) = (π Β· π¦)) |
27 | 26 | eqeq2d 2744 |
. . . . . . . 8
β’ (π£ = π β (π₯ = (π( Β·π
βπ£)π¦) β π₯ = (π Β· π¦))) |
28 | 22, 27 | rexeqbidv 3319 |
. . . . . . 7
β’ (π£ = π β (βπ β (Baseβ(Scalarβπ£))π₯ = (π( Β·π
βπ£)π¦) β βπ β πΎ π₯ = (π Β· π¦))) |
29 | 16, 28 | bi2anan9r 639 |
. . . . . 6
β’ ((π£ = π β§ π = π΅) β (((π₯ β π β§ π¦ β π) β§ βπ β (Baseβ(Scalarβπ£))π₯ = (π( Β·π
βπ£)π¦)) β ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦)))) |
30 | 13, 29 | syl 17 |
. . . . 5
β’ ((π£ = π β§ π = ((Baseβπ£) β {(0gβπ£)})) β (((π₯ β π β§ π¦ β π) β§ βπ β (Baseβ(Scalarβπ£))π₯ = (π( Β·π
βπ£)π¦)) β ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦)))) |
31 | 30 | opabbidv 5175 |
. . . 4
β’ ((π£ = π β§ π = ((Baseβπ£) β {(0gβπ£)})) β {β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π) β§ βπ β (Baseβ(Scalarβπ£))π₯ = (π( Β·π
βπ£)π¦))} = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))}) |
32 | 12, 31 | qseq12d 40713 |
. . 3
β’ ((π£ = π β§ π = ((Baseβπ£) β {(0gβπ£)})) β (π / {β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π) β§ βπ β (Baseβ(Scalarβπ£))π₯ = (π( Β·π
βπ£)π¦))}) = (π΅ / {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))})) |
33 | 3, 32 | csbied 3897 |
. 2
β’ (π£ = π β β¦((Baseβπ£) β
{(0gβπ£)})
/ πβ¦(π / {β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π) β§ βπ β (Baseβ(Scalarβπ£))π₯ = (π( Β·π
βπ£)π¦))}) = (π΅ / {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))})) |
34 | | df-prjsp 40987 |
. 2
β’
βπ£π π = (π£ β LVec β¦
β¦((Baseβπ£) β {(0gβπ£)}) / πβ¦(π / {β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π) β§ βπ β (Baseβ(Scalarβπ£))π₯ = (π( Β·π
βπ£)π¦))})) |
35 | | fvex 6859 |
. . . . 5
β’
(Baseβπ)
β V |
36 | 35 | difexi 5289 |
. . . 4
β’
((Baseβπ)
β {(0gβπ)}) β V |
37 | 8, 36 | eqeltri 2830 |
. . 3
β’ π΅ β V |
38 | 37 | qsex 8721 |
. 2
β’ (π΅ / {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))}) β V |
39 | 33, 34, 38 | fvmpt 6952 |
1
β’ (π β LVec β
(βπ£π πβπ) = (π΅ / {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))})) |