Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . . . . 8
β’
(Scalarβπ) =
(Scalarβπ) |
2 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
3 | | ldual1dim.d |
. . . . . . . 8
β’ π· = (LDualβπ) |
4 | | eqid 2737 |
. . . . . . . 8
β’
(Scalarβπ·) =
(Scalarβπ·) |
5 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβ(Scalarβπ·)) = (Baseβ(Scalarβπ·)) |
6 | | ldual1dim.w |
. . . . . . . 8
β’ (π β π β LVec) |
7 | 1, 2, 3, 4, 5, 6 | ldualsbase 37598 |
. . . . . . 7
β’ (π β
(Baseβ(Scalarβπ·)) = (Baseβ(Scalarβπ))) |
8 | 7 | eleq2d 2824 |
. . . . . 6
β’ (π β (π β (Baseβ(Scalarβπ·)) β π β (Baseβ(Scalarβπ)))) |
9 | 8 | anbi1d 631 |
. . . . 5
β’ (π β ((π β (Baseβ(Scalarβπ·)) β§ π = (π( Β·π
βπ·)πΊ)) β (π β (Baseβ(Scalarβπ)) β§ π = (π( Β·π
βπ·)πΊ)))) |
10 | | ldual1dim.f |
. . . . . . . 8
β’ πΉ = (LFnlβπ) |
11 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
12 | | eqid 2737 |
. . . . . . . 8
β’
(.rβ(Scalarβπ)) =
(.rβ(Scalarβπ)) |
13 | | eqid 2737 |
. . . . . . . 8
β’ (
Β·π βπ·) = ( Β·π
βπ·) |
14 | 6 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (Baseβ(Scalarβπ))) β π β LVec) |
15 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β (Baseβ(Scalarβπ))) β π β (Baseβ(Scalarβπ))) |
16 | | ldual1dim.g |
. . . . . . . . 9
β’ (π β πΊ β πΉ) |
17 | 16 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (Baseβ(Scalarβπ))) β πΊ β πΉ) |
18 | 10, 11, 1, 2, 12, 3,
13, 14, 15, 17 | ldualvs 37602 |
. . . . . . 7
β’ ((π β§ π β (Baseβ(Scalarβπ))) β (π( Β·π
βπ·)πΊ) = (πΊ βf
(.rβ(Scalarβπ))((Baseβπ) Γ {π}))) |
19 | 18 | eqeq2d 2748 |
. . . . . 6
β’ ((π β§ π β (Baseβ(Scalarβπ))) β (π = (π( Β·π
βπ·)πΊ) β π = (πΊ βf
(.rβ(Scalarβπ))((Baseβπ) Γ {π})))) |
20 | 19 | pm5.32da 580 |
. . . . 5
β’ (π β ((π β (Baseβ(Scalarβπ)) β§ π = (π( Β·π
βπ·)πΊ)) β (π β (Baseβ(Scalarβπ)) β§ π = (πΊ βf
(.rβ(Scalarβπ))((Baseβπ) Γ {π}))))) |
21 | 9, 20 | bitrd 279 |
. . . 4
β’ (π β ((π β (Baseβ(Scalarβπ·)) β§ π = (π( Β·π
βπ·)πΊ)) β (π β (Baseβ(Scalarβπ)) β§ π = (πΊ βf
(.rβ(Scalarβπ))((Baseβπ) Γ {π}))))) |
22 | 21 | rexbidv2 3172 |
. . 3
β’ (π β (βπ β (Baseβ(Scalarβπ·))π = (π( Β·π
βπ·)πΊ) β βπ β (Baseβ(Scalarβπ))π = (πΊ βf
(.rβ(Scalarβπ))((Baseβπ) Γ {π})))) |
23 | 22 | abbidv 2806 |
. 2
β’ (π β {π β£ βπ β (Baseβ(Scalarβπ·))π = (π( Β·π
βπ·)πΊ)} = {π β£ βπ β (Baseβ(Scalarβπ))π = (πΊ βf
(.rβ(Scalarβπ))((Baseβπ) Γ {π}))}) |
24 | | lveclmod 20570 |
. . . . 5
β’ (π β LVec β π β LMod) |
25 | 3, 24 | lduallmod 37618 |
. . . 4
β’ (π β LVec β π· β LMod) |
26 | 6, 25 | syl 17 |
. . 3
β’ (π β π· β LMod) |
27 | | eqid 2737 |
. . . 4
β’
(Baseβπ·) =
(Baseβπ·) |
28 | 10, 3, 27, 6, 16 | ldualelvbase 37592 |
. . 3
β’ (π β πΊ β (Baseβπ·)) |
29 | | ldual1dim.n |
. . . 4
β’ π = (LSpanβπ·) |
30 | 4, 5, 27, 13, 29 | lspsn 20466 |
. . 3
β’ ((π· β LMod β§ πΊ β (Baseβπ·)) β (πβ{πΊ}) = {π β£ βπ β (Baseβ(Scalarβπ·))π = (π( Β·π
βπ·)πΊ)}) |
31 | 26, 28, 30 | syl2anc 585 |
. 2
β’ (π β (πβ{πΊ}) = {π β£ βπ β (Baseβ(Scalarβπ·))π = (π( Β·π
βπ·)πΊ)}) |
32 | | ldual1dim.l |
. . 3
β’ πΏ = (LKerβπ) |
33 | 11, 1, 10, 32, 2, 12, 6, 16 | lfl1dim 37586 |
. 2
β’ (π β {π β πΉ β£ (πΏβπΊ) β (πΏβπ)} = {π β£ βπ β (Baseβ(Scalarβπ))π = (πΊ βf
(.rβ(Scalarβπ))((Baseβπ) Γ {π}))}) |
34 | 23, 31, 33 | 3eqtr4d 2787 |
1
β’ (π β (πβ{πΊ}) = {π β πΉ β£ (πΏβπΊ) β (πΏβπ)}) |