Step | Hyp | Ref
| Expression |
1 | | ldualvsubval.d |
. . . . 5
β’ π· = (LDualβπ) |
2 | | ldualvsubval.w |
. . . . 5
β’ (π β π β LMod) |
3 | 1, 2 | lduallmod 37618 |
. . . 4
β’ (π β π· β LMod) |
4 | | ldualvsubval.f |
. . . . 5
β’ πΉ = (LFnlβπ) |
5 | | eqid 2737 |
. . . . 5
β’
(Baseβπ·) =
(Baseβπ·) |
6 | | ldualvsubval.g |
. . . . 5
β’ (π β πΊ β πΉ) |
7 | 4, 1, 5, 2, 6 | ldualelvbase 37592 |
. . . 4
β’ (π β πΊ β (Baseβπ·)) |
8 | | ldualvsubval.h |
. . . . 5
β’ (π β π» β πΉ) |
9 | 4, 1, 5, 2, 8 | ldualelvbase 37592 |
. . . 4
β’ (π β π» β (Baseβπ·)) |
10 | | eqid 2737 |
. . . . 5
β’
(+gβπ·) = (+gβπ·) |
11 | | ldualvsubval.m |
. . . . 5
β’ β =
(-gβπ·) |
12 | | eqid 2737 |
. . . . 5
β’
(Scalarβπ·) =
(Scalarβπ·) |
13 | | eqid 2737 |
. . . . 5
β’ (
Β·π βπ·) = ( Β·π
βπ·) |
14 | | eqid 2737 |
. . . . 5
β’
(invgβ(Scalarβπ·)) =
(invgβ(Scalarβπ·)) |
15 | | eqid 2737 |
. . . . 5
β’
(1rβ(Scalarβπ·)) =
(1rβ(Scalarβπ·)) |
16 | 5, 10, 11, 12, 13, 14, 15 | lmodvsubval2 20380 |
. . . 4
β’ ((π· β LMod β§ πΊ β (Baseβπ·) β§ π» β (Baseβπ·)) β (πΊ β π») = (πΊ(+gβπ·)(((invgβ(Scalarβπ·))β(1rβ(Scalarβπ·)))(
Β·π βπ·)π»))) |
17 | 3, 7, 9, 16 | syl3anc 1372 |
. . 3
β’ (π β (πΊ β π») = (πΊ(+gβπ·)(((invgβ(Scalarβπ·))β(1rβ(Scalarβπ·)))(
Β·π βπ·)π»))) |
18 | 17 | fveq1d 6845 |
. 2
β’ (π β ((πΊ β π»)βπ) = ((πΊ(+gβπ·)(((invgβ(Scalarβπ·))β(1rβ(Scalarβπ·)))(
Β·π βπ·)π»))βπ)) |
19 | | ldualvsubval.v |
. . 3
β’ π = (Baseβπ) |
20 | | ldualvsubval.r |
. . 3
β’ π
= (Scalarβπ) |
21 | | eqid 2737 |
. . 3
β’
(+gβπ
) = (+gβπ
) |
22 | | eqid 2737 |
. . . 4
β’
(Baseβπ
) =
(Baseβπ
) |
23 | 12 | lmodfgrp 20334 |
. . . . . . 7
β’ (π· β LMod β
(Scalarβπ·) β
Grp) |
24 | 3, 23 | syl 17 |
. . . . . 6
β’ (π β (Scalarβπ·) β Grp) |
25 | 12 | lmodring 20333 |
. . . . . . . 8
β’ (π· β LMod β
(Scalarβπ·) β
Ring) |
26 | 3, 25 | syl 17 |
. . . . . . 7
β’ (π β (Scalarβπ·) β Ring) |
27 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβ(Scalarβπ·)) = (Baseβ(Scalarβπ·)) |
28 | 27, 15 | ringidcl 19990 |
. . . . . . 7
β’
((Scalarβπ·)
β Ring β (1rβ(Scalarβπ·)) β (Baseβ(Scalarβπ·))) |
29 | 26, 28 | syl 17 |
. . . . . 6
β’ (π β
(1rβ(Scalarβπ·)) β (Baseβ(Scalarβπ·))) |
30 | 27, 14 | grpinvcl 18799 |
. . . . . 6
β’
(((Scalarβπ·)
β Grp β§ (1rβ(Scalarβπ·)) β (Baseβ(Scalarβπ·))) β
((invgβ(Scalarβπ·))β(1rβ(Scalarβπ·))) β
(Baseβ(Scalarβπ·))) |
31 | 24, 29, 30 | syl2anc 585 |
. . . . 5
β’ (π β
((invgβ(Scalarβπ·))β(1rβ(Scalarβπ·))) β
(Baseβ(Scalarβπ·))) |
32 | 20, 22, 1, 12, 27, 2 | ldualsbase 37598 |
. . . . 5
β’ (π β
(Baseβ(Scalarβπ·)) = (Baseβπ
)) |
33 | 31, 32 | eleqtrd 2840 |
. . . 4
β’ (π β
((invgβ(Scalarβπ·))β(1rβ(Scalarβπ·))) β (Baseβπ
)) |
34 | 4, 20, 22, 1, 13, 2, 33, 8 | ldualvscl 37604 |
. . 3
β’ (π β
(((invgβ(Scalarβπ·))β(1rβ(Scalarβπ·)))(
Β·π βπ·)π») β πΉ) |
35 | | ldualvsubval.x |
. . 3
β’ (π β π β π) |
36 | 19, 20, 21, 4, 1, 10, 2, 6, 34, 35 | ldualvaddval 37596 |
. 2
β’ (π β ((πΊ(+gβπ·)(((invgβ(Scalarβπ·))β(1rβ(Scalarβπ·)))(
Β·π βπ·)π»))βπ) = ((πΊβπ)(+gβπ
)((((invgβ(Scalarβπ·))β(1rβ(Scalarβπ·)))(
Β·π βπ·)π»)βπ))) |
37 | | eqid 2737 |
. . . . . . . . 9
β’
(invgβπ
) = (invgβπ
) |
38 | 20, 37, 1, 12, 14, 2 | ldualneg 37614 |
. . . . . . . 8
β’ (π β
(invgβ(Scalarβπ·)) = (invgβπ
)) |
39 | | eqid 2737 |
. . . . . . . . 9
β’
(1rβπ
) = (1rβπ
) |
40 | 20, 39, 1, 12, 15, 2 | ldual1 37613 |
. . . . . . . 8
β’ (π β
(1rβ(Scalarβπ·)) = (1rβπ
)) |
41 | 38, 40 | fveq12d 6850 |
. . . . . . 7
β’ (π β
((invgβ(Scalarβπ·))β(1rβ(Scalarβπ·))) = ((invgβπ
)β(1rβπ
))) |
42 | 41 | oveq1d 7373 |
. . . . . 6
β’ (π β
(((invgβ(Scalarβπ·))β(1rβ(Scalarβπ·)))(
Β·π βπ·)π») = (((invgβπ
)β(1rβπ
))( Β·π
βπ·)π»)) |
43 | 42 | fveq1d 6845 |
. . . . 5
β’ (π β
((((invgβ(Scalarβπ·))β(1rβ(Scalarβπ·)))(
Β·π βπ·)π»)βπ) = ((((invgβπ
)β(1rβπ
))( Β·π
βπ·)π»)βπ)) |
44 | | eqid 2737 |
. . . . . 6
β’
(.rβπ
) = (.rβπ
) |
45 | 20 | lmodring 20333 |
. . . . . . . . 9
β’ (π β LMod β π
β Ring) |
46 | 2, 45 | syl 17 |
. . . . . . . 8
β’ (π β π
β Ring) |
47 | | ringgrp 19970 |
. . . . . . . 8
β’ (π
β Ring β π
β Grp) |
48 | 46, 47 | syl 17 |
. . . . . . 7
β’ (π β π
β Grp) |
49 | 20, 22, 39 | lmod1cl 20352 |
. . . . . . . 8
β’ (π β LMod β
(1rβπ
)
β (Baseβπ
)) |
50 | 2, 49 | syl 17 |
. . . . . . 7
β’ (π β (1rβπ
) β (Baseβπ
)) |
51 | 22, 37 | grpinvcl 18799 |
. . . . . . 7
β’ ((π
β Grp β§
(1rβπ
)
β (Baseβπ
))
β ((invgβπ
)β(1rβπ
)) β (Baseβπ
)) |
52 | 48, 50, 51 | syl2anc 585 |
. . . . . 6
β’ (π β
((invgβπ
)β(1rβπ
)) β (Baseβπ
)) |
53 | 4, 19, 20, 22, 44, 1, 13, 2, 52, 8, 35 | ldualvsval 37603 |
. . . . 5
β’ (π β
((((invgβπ
)β(1rβπ
))(
Β·π βπ·)π»)βπ) = ((π»βπ)(.rβπ
)((invgβπ
)β(1rβπ
)))) |
54 | 20, 22, 19, 4 | lflcl 37529 |
. . . . . . 7
β’ ((π β LMod β§ π» β πΉ β§ π β π) β (π»βπ) β (Baseβπ
)) |
55 | 2, 8, 35, 54 | syl3anc 1372 |
. . . . . 6
β’ (π β (π»βπ) β (Baseβπ
)) |
56 | 22, 44, 39, 37, 46, 55 | ringnegr 20020 |
. . . . 5
β’ (π β ((π»βπ)(.rβπ
)((invgβπ
)β(1rβπ
))) =
((invgβπ
)β(π»βπ))) |
57 | 43, 53, 56 | 3eqtrd 2781 |
. . . 4
β’ (π β
((((invgβ(Scalarβπ·))β(1rβ(Scalarβπ·)))(
Β·π βπ·)π»)βπ) = ((invgβπ
)β(π»βπ))) |
58 | 57 | oveq2d 7374 |
. . 3
β’ (π β ((πΊβπ)(+gβπ
)((((invgβ(Scalarβπ·))β(1rβ(Scalarβπ·)))(
Β·π βπ·)π»)βπ)) = ((πΊβπ)(+gβπ
)((invgβπ
)β(π»βπ)))) |
59 | 20, 22, 19, 4 | lflcl 37529 |
. . . . 5
β’ ((π β LMod β§ πΊ β πΉ β§ π β π) β (πΊβπ) β (Baseβπ
)) |
60 | 2, 6, 35, 59 | syl3anc 1372 |
. . . 4
β’ (π β (πΊβπ) β (Baseβπ
)) |
61 | | ldualvsubval.s |
. . . . 5
β’ π = (-gβπ
) |
62 | 22, 21, 37, 61 | grpsubval 18797 |
. . . 4
β’ (((πΊβπ) β (Baseβπ
) β§ (π»βπ) β (Baseβπ
)) β ((πΊβπ)π(π»βπ)) = ((πΊβπ)(+gβπ
)((invgβπ
)β(π»βπ)))) |
63 | 60, 55, 62 | syl2anc 585 |
. . 3
β’ (π β ((πΊβπ)π(π»βπ)) = ((πΊβπ)(+gβπ
)((invgβπ
)β(π»βπ)))) |
64 | 58, 63 | eqtr4d 2780 |
. 2
β’ (π β ((πΊβπ)(+gβπ
)((((invgβ(Scalarβπ·))β(1rβ(Scalarβπ·)))(
Β·π βπ·)π»)βπ)) = ((πΊβπ)π(π»βπ))) |
65 | 18, 36, 64 | 3eqtrd 2781 |
1
β’ (π β ((πΊ β π»)βπ) = ((πΊβπ)π(π»βπ))) |