Step | Hyp | Ref
| Expression |
1 | | lcdvsubval.h |
. . . . 5
β’ π» = (LHypβπΎ) |
2 | | lcdvsubval.c |
. . . . 5
β’ πΆ = ((LCDualβπΎ)βπ) |
3 | | lcdvsubval.k |
. . . . 5
β’ (π β (πΎ β HL β§ π β π»)) |
4 | 1, 2, 3 | lcdlmod 40105 |
. . . 4
β’ (π β πΆ β LMod) |
5 | | lcdvsubval.f |
. . . 4
β’ (π β πΉ β π·) |
6 | | lcdvsubval.g |
. . . 4
β’ (π β πΊ β π·) |
7 | | lcdvsubval.d |
. . . . 5
β’ π· = (BaseβπΆ) |
8 | | eqid 2733 |
. . . . 5
β’
(+gβπΆ) = (+gβπΆ) |
9 | | lcdvsubval.m |
. . . . 5
β’ β =
(-gβπΆ) |
10 | | eqid 2733 |
. . . . 5
β’
(ScalarβπΆ) =
(ScalarβπΆ) |
11 | | eqid 2733 |
. . . . 5
β’ (
Β·π βπΆ) = ( Β·π
βπΆ) |
12 | | eqid 2733 |
. . . . 5
β’
(invgβ(ScalarβπΆ)) =
(invgβ(ScalarβπΆ)) |
13 | | eqid 2733 |
. . . . 5
β’
(1rβ(ScalarβπΆ)) =
(1rβ(ScalarβπΆ)) |
14 | 7, 8, 9, 10, 11, 12, 13 | lmodvsubval2 20421 |
. . . 4
β’ ((πΆ β LMod β§ πΉ β π· β§ πΊ β π·) β (πΉ β πΊ) = (πΉ(+gβπΆ)(((invgβ(ScalarβπΆ))β(1rβ(ScalarβπΆ)))(
Β·π βπΆ)πΊ))) |
15 | 4, 5, 6, 14 | syl3anc 1372 |
. . 3
β’ (π β (πΉ β πΊ) = (πΉ(+gβπΆ)(((invgβ(ScalarβπΆ))β(1rβ(ScalarβπΆ)))(
Β·π βπΆ)πΊ))) |
16 | 15 | fveq1d 6848 |
. 2
β’ (π β ((πΉ β πΊ)βπ) = ((πΉ(+gβπΆ)(((invgβ(ScalarβπΆ))β(1rβ(ScalarβπΆ)))(
Β·π βπΆ)πΊ))βπ)) |
17 | | lcdvsubval.u |
. . 3
β’ π = ((DVecHβπΎ)βπ) |
18 | | lcdvsubval.v |
. . 3
β’ π = (Baseβπ) |
19 | | lcdvsubval.r |
. . 3
β’ π
= (Scalarβπ) |
20 | | eqid 2733 |
. . 3
β’
(+gβπ
) = (+gβπ
) |
21 | | eqid 2733 |
. . . 4
β’
(Baseβπ
) =
(Baseβπ
) |
22 | 10 | lmodfgrp 20374 |
. . . . . . 7
β’ (πΆ β LMod β
(ScalarβπΆ) β
Grp) |
23 | 4, 22 | syl 17 |
. . . . . 6
β’ (π β (ScalarβπΆ) β Grp) |
24 | 10 | lmodring 20373 |
. . . . . . . 8
β’ (πΆ β LMod β
(ScalarβπΆ) β
Ring) |
25 | 4, 24 | syl 17 |
. . . . . . 7
β’ (π β (ScalarβπΆ) β Ring) |
26 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβ(ScalarβπΆ)) = (Baseβ(ScalarβπΆ)) |
27 | 26, 13 | ringidcl 19997 |
. . . . . . 7
β’
((ScalarβπΆ)
β Ring β (1rβ(ScalarβπΆ)) β (Baseβ(ScalarβπΆ))) |
28 | 25, 27 | syl 17 |
. . . . . 6
β’ (π β
(1rβ(ScalarβπΆ)) β (Baseβ(ScalarβπΆ))) |
29 | 26, 12 | grpinvcl 18806 |
. . . . . 6
β’
(((ScalarβπΆ)
β Grp β§ (1rβ(ScalarβπΆ)) β (Baseβ(ScalarβπΆ))) β
((invgβ(ScalarβπΆ))β(1rβ(ScalarβπΆ))) β
(Baseβ(ScalarβπΆ))) |
30 | 23, 28, 29 | syl2anc 585 |
. . . . 5
β’ (π β
((invgβ(ScalarβπΆ))β(1rβ(ScalarβπΆ))) β
(Baseβ(ScalarβπΆ))) |
31 | 1, 17, 19, 21, 2, 10, 26, 3 | lcdsbase 40113 |
. . . . 5
β’ (π β
(Baseβ(ScalarβπΆ)) = (Baseβπ
)) |
32 | 30, 31 | eleqtrd 2836 |
. . . 4
β’ (π β
((invgβ(ScalarβπΆ))β(1rβ(ScalarβπΆ))) β (Baseβπ
)) |
33 | 1, 17, 19, 21, 2, 7, 11, 3, 32, 6 | lcdvscl 40118 |
. . 3
β’ (π β
(((invgβ(ScalarβπΆ))β(1rβ(ScalarβπΆ)))(
Β·π βπΆ)πΊ) β π·) |
34 | | lcdvsubval.x |
. . 3
β’ (π β π β π) |
35 | 1, 17, 18, 19, 20, 2, 7, 8, 3, 5, 33, 34 | lcdvaddval 40111 |
. 2
β’ (π β ((πΉ(+gβπΆ)(((invgβ(ScalarβπΆ))β(1rβ(ScalarβπΆ)))(
Β·π βπΆ)πΊ))βπ) = ((πΉβπ)(+gβπ
)((((invgβ(ScalarβπΆ))β(1rβ(ScalarβπΆ)))(
Β·π βπΆ)πΊ)βπ))) |
36 | | eqid 2733 |
. . . . . . . . 9
β’
(invgβπ
) = (invgβπ
) |
37 | 1, 17, 19, 36, 2, 10, 12, 3 | lcdneg 40123 |
. . . . . . . 8
β’ (π β
(invgβ(ScalarβπΆ)) = (invgβπ
)) |
38 | | eqid 2733 |
. . . . . . . . 9
β’
(1rβπ
) = (1rβπ
) |
39 | 1, 17, 19, 38, 2, 10, 13, 3 | lcd1 40122 |
. . . . . . . 8
β’ (π β
(1rβ(ScalarβπΆ)) = (1rβπ
)) |
40 | 37, 39 | fveq12d 6853 |
. . . . . . 7
β’ (π β
((invgβ(ScalarβπΆ))β(1rβ(ScalarβπΆ))) = ((invgβπ
)β(1rβπ
))) |
41 | 40 | oveq1d 7376 |
. . . . . 6
β’ (π β
(((invgβ(ScalarβπΆ))β(1rβ(ScalarβπΆ)))(
Β·π βπΆ)πΊ) = (((invgβπ
)β(1rβπ
))( Β·π
βπΆ)πΊ)) |
42 | 41 | fveq1d 6848 |
. . . . 5
β’ (π β
((((invgβ(ScalarβπΆ))β(1rβ(ScalarβπΆ)))(
Β·π βπΆ)πΊ)βπ) = ((((invgβπ
)β(1rβπ
))( Β·π
βπΆ)πΊ)βπ)) |
43 | | eqid 2733 |
. . . . . 6
β’
(.rβπ
) = (.rβπ
) |
44 | 1, 17, 3 | dvhlmod 39623 |
. . . . . . . . 9
β’ (π β π β LMod) |
45 | 19 | lmodring 20373 |
. . . . . . . . 9
β’ (π β LMod β π
β Ring) |
46 | 44, 45 | syl 17 |
. . . . . . . 8
β’ (π β π
β Ring) |
47 | | ringgrp 19977 |
. . . . . . . 8
β’ (π
β Ring β π
β Grp) |
48 | 46, 47 | syl 17 |
. . . . . . 7
β’ (π β π
β Grp) |
49 | 19, 21, 38 | lmod1cl 20393 |
. . . . . . . 8
β’ (π β LMod β
(1rβπ
)
β (Baseβπ
)) |
50 | 44, 49 | syl 17 |
. . . . . . 7
β’ (π β (1rβπ
) β (Baseβπ
)) |
51 | 21, 36 | grpinvcl 18806 |
. . . . . . 7
β’ ((π
β Grp β§
(1rβπ
)
β (Baseβπ
))
β ((invgβπ
)β(1rβπ
)) β (Baseβπ
)) |
52 | 48, 50, 51 | syl2anc 585 |
. . . . . 6
β’ (π β
((invgβπ
)β(1rβπ
)) β (Baseβπ
)) |
53 | 1, 17, 18, 19, 21, 43, 2, 7, 11, 3, 52, 6, 34 | lcdvsval 40117 |
. . . . 5
β’ (π β
((((invgβπ
)β(1rβπ
))(
Β·π βπΆ)πΊ)βπ) = ((πΊβπ)(.rβπ
)((invgβπ
)β(1rβπ
)))) |
54 | 1, 17, 18, 19, 21, 2, 7, 3, 6, 34 | lcdvbasecl 40109 |
. . . . . 6
β’ (π β (πΊβπ) β (Baseβπ
)) |
55 | 21, 43, 38, 36, 46, 54 | ringnegr 20027 |
. . . . 5
β’ (π β ((πΊβπ)(.rβπ
)((invgβπ
)β(1rβπ
))) =
((invgβπ
)β(πΊβπ))) |
56 | 42, 53, 55 | 3eqtrd 2777 |
. . . 4
β’ (π β
((((invgβ(ScalarβπΆ))β(1rβ(ScalarβπΆ)))(
Β·π βπΆ)πΊ)βπ) = ((invgβπ
)β(πΊβπ))) |
57 | 56 | oveq2d 7377 |
. . 3
β’ (π β ((πΉβπ)(+gβπ
)((((invgβ(ScalarβπΆ))β(1rβ(ScalarβπΆ)))(
Β·π βπΆ)πΊ)βπ)) = ((πΉβπ)(+gβπ
)((invgβπ
)β(πΊβπ)))) |
58 | 1, 17, 18, 19, 21, 2, 7, 3, 5, 34 | lcdvbasecl 40109 |
. . . 4
β’ (π β (πΉβπ) β (Baseβπ
)) |
59 | | lcdvsubval.s |
. . . . 5
β’ π = (-gβπ
) |
60 | 21, 20, 36, 59 | grpsubval 18804 |
. . . 4
β’ (((πΉβπ) β (Baseβπ
) β§ (πΊβπ) β (Baseβπ
)) β ((πΉβπ)π(πΊβπ)) = ((πΉβπ)(+gβπ
)((invgβπ
)β(πΊβπ)))) |
61 | 58, 54, 60 | syl2anc 585 |
. . 3
β’ (π β ((πΉβπ)π(πΊβπ)) = ((πΉβπ)(+gβπ
)((invgβπ
)β(πΊβπ)))) |
62 | 57, 61 | eqtr4d 2776 |
. 2
β’ (π β ((πΉβπ)(+gβπ
)((((invgβ(ScalarβπΆ))β(1rβ(ScalarβπΆ)))(
Β·π βπΆ)πΊ)βπ)) = ((πΉβπ)π(πΊβπ))) |
63 | 16, 35, 62 | 3eqtrd 2777 |
1
β’ (π β ((πΉ β πΊ)βπ) = ((πΉβπ)π(πΊβπ))) |