Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’
(LSubSpβπ) =
(LSubSpβπ) |
2 | | lspsn.n |
. . 3
β’ π = (LSpanβπ) |
3 | | simpl 484 |
. . 3
β’ ((π β LMod β§ π β π) β π β LMod) |
4 | | lspsn.v |
. . . 4
β’ π = (Baseβπ) |
5 | | lspsn.f |
. . . 4
β’ πΉ = (Scalarβπ) |
6 | | lspsn.t |
. . . 4
β’ Β· = (
Β·π βπ) |
7 | | lspsn.k |
. . . 4
β’ πΎ = (BaseβπΉ) |
8 | 4, 5, 6, 7, 1 | lss1d 20439 |
. . 3
β’ ((π β LMod β§ π β π) β {π£ β£ βπ β πΎ π£ = (π Β· π)} β (LSubSpβπ)) |
9 | | eqid 2733 |
. . . . . 6
β’
(1rβπΉ) = (1rβπΉ) |
10 | 5, 7, 9 | lmod1cl 20364 |
. . . . 5
β’ (π β LMod β
(1rβπΉ)
β πΎ) |
11 | 4, 5, 6, 9 | lmodvs1 20365 |
. . . . . 6
β’ ((π β LMod β§ π β π) β ((1rβπΉ) Β· π) = π) |
12 | 11 | eqcomd 2739 |
. . . . 5
β’ ((π β LMod β§ π β π) β π = ((1rβπΉ) Β· π)) |
13 | | oveq1 7365 |
. . . . . 6
β’ (π = (1rβπΉ) β (π Β· π) = ((1rβπΉ) Β· π)) |
14 | 13 | rspceeqv 3596 |
. . . . 5
β’
(((1rβπΉ) β πΎ β§ π = ((1rβπΉ) Β· π)) β βπ β πΎ π = (π Β· π)) |
15 | 10, 12, 14 | syl2an2r 684 |
. . . 4
β’ ((π β LMod β§ π β π) β βπ β πΎ π = (π Β· π)) |
16 | | eqeq1 2737 |
. . . . . . 7
β’ (π£ = π β (π£ = (π Β· π) β π = (π Β· π))) |
17 | 16 | rexbidv 3172 |
. . . . . 6
β’ (π£ = π β (βπ β πΎ π£ = (π Β· π) β βπ β πΎ π = (π Β· π))) |
18 | 17 | elabg 3629 |
. . . . 5
β’ (π β π β (π β {π£ β£ βπ β πΎ π£ = (π Β· π)} β βπ β πΎ π = (π Β· π))) |
19 | 18 | adantl 483 |
. . . 4
β’ ((π β LMod β§ π β π) β (π β {π£ β£ βπ β πΎ π£ = (π Β· π)} β βπ β πΎ π = (π Β· π))) |
20 | 15, 19 | mpbird 257 |
. . 3
β’ ((π β LMod β§ π β π) β π β {π£ β£ βπ β πΎ π£ = (π Β· π)}) |
21 | 1, 2, 3, 8, 20 | lspsnel5a 20472 |
. 2
β’ ((π β LMod β§ π β π) β (πβ{π}) β {π£ β£ βπ β πΎ π£ = (π Β· π)}) |
22 | 3 | adantr 482 |
. . . . . 6
β’ (((π β LMod β§ π β π) β§ π β πΎ) β π β LMod) |
23 | 4, 1, 2 | lspsncl 20453 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
24 | 23 | adantr 482 |
. . . . . 6
β’ (((π β LMod β§ π β π) β§ π β πΎ) β (πβ{π}) β (LSubSpβπ)) |
25 | | simpr 486 |
. . . . . 6
β’ (((π β LMod β§ π β π) β§ π β πΎ) β π β πΎ) |
26 | 4, 2 | lspsnid 20469 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β π β (πβ{π})) |
27 | 26 | adantr 482 |
. . . . . 6
β’ (((π β LMod β§ π β π) β§ π β πΎ) β π β (πβ{π})) |
28 | 5, 6, 7, 1 | lssvscl 20431 |
. . . . . 6
β’ (((π β LMod β§ (πβ{π}) β (LSubSpβπ)) β§ (π β πΎ β§ π β (πβ{π}))) β (π Β· π) β (πβ{π})) |
29 | 22, 24, 25, 27, 28 | syl22anc 838 |
. . . . 5
β’ (((π β LMod β§ π β π) β§ π β πΎ) β (π Β· π) β (πβ{π})) |
30 | | eleq1a 2829 |
. . . . 5
β’ ((π Β· π) β (πβ{π}) β (π£ = (π Β· π) β π£ β (πβ{π}))) |
31 | 29, 30 | syl 17 |
. . . 4
β’ (((π β LMod β§ π β π) β§ π β πΎ) β (π£ = (π Β· π) β π£ β (πβ{π}))) |
32 | 31 | rexlimdva 3149 |
. . 3
β’ ((π β LMod β§ π β π) β (βπ β πΎ π£ = (π Β· π) β π£ β (πβ{π}))) |
33 | 32 | abssdv 4026 |
. 2
β’ ((π β LMod β§ π β π) β {π£ β£ βπ β πΎ π£ = (π Β· π)} β (πβ{π})) |
34 | 21, 33 | eqssd 3962 |
1
β’ ((π β LMod β§ π β π) β (πβ{π}) = {π£ β£ βπ β πΎ π£ = (π Β· π)}) |