Step | Hyp | Ref
| Expression |
1 | | lmodsubdir.w |
. . . 4
β’ (π β π β LMod) |
2 | | lmodsubdir.a |
. . . 4
β’ (π β π΄ β πΎ) |
3 | | lmodsubdir.f |
. . . . . . . 8
β’ πΉ = (Scalarβπ) |
4 | 3 | lmodring 20344 |
. . . . . . 7
β’ (π β LMod β πΉ β Ring) |
5 | 1, 4 | syl 17 |
. . . . . 6
β’ (π β πΉ β Ring) |
6 | | ringgrp 19974 |
. . . . . 6
β’ (πΉ β Ring β πΉ β Grp) |
7 | 5, 6 | syl 17 |
. . . . 5
β’ (π β πΉ β Grp) |
8 | | lmodsubdir.b |
. . . . 5
β’ (π β π΅ β πΎ) |
9 | | lmodsubdir.k |
. . . . . 6
β’ πΎ = (BaseβπΉ) |
10 | | eqid 2733 |
. . . . . 6
β’
(invgβπΉ) = (invgβπΉ) |
11 | 9, 10 | grpinvcl 18803 |
. . . . 5
β’ ((πΉ β Grp β§ π΅ β πΎ) β ((invgβπΉ)βπ΅) β πΎ) |
12 | 7, 8, 11 | syl2anc 585 |
. . . 4
β’ (π β
((invgβπΉ)βπ΅) β πΎ) |
13 | | lmodsubdir.x |
. . . 4
β’ (π β π β π) |
14 | | lmodsubdir.v |
. . . . 5
β’ π = (Baseβπ) |
15 | | eqid 2733 |
. . . . 5
β’
(+gβπ) = (+gβπ) |
16 | | lmodsubdir.t |
. . . . 5
β’ Β· = (
Β·π βπ) |
17 | | eqid 2733 |
. . . . 5
β’
(+gβπΉ) = (+gβπΉ) |
18 | 14, 15, 3, 16, 9, 17 | lmodvsdir 20361 |
. . . 4
β’ ((π β LMod β§ (π΄ β πΎ β§ ((invgβπΉ)βπ΅) β πΎ β§ π β π)) β ((π΄(+gβπΉ)((invgβπΉ)βπ΅)) Β· π) = ((π΄ Β· π)(+gβπ)(((invgβπΉ)βπ΅) Β· π))) |
19 | 1, 2, 12, 13, 18 | syl13anc 1373 |
. . 3
β’ (π β ((π΄(+gβπΉ)((invgβπΉ)βπ΅)) Β· π) = ((π΄ Β· π)(+gβπ)(((invgβπΉ)βπ΅) Β· π))) |
20 | | eqid 2733 |
. . . . . . 7
β’
(.rβπΉ) = (.rβπΉ) |
21 | | eqid 2733 |
. . . . . . 7
β’
(1rβπΉ) = (1rβπΉ) |
22 | 9, 20, 21, 10, 5, 8 | ringnegl 20023 |
. . . . . 6
β’ (π β
(((invgβπΉ)β(1rβπΉ))(.rβπΉ)π΅) = ((invgβπΉ)βπ΅)) |
23 | 22 | oveq1d 7373 |
. . . . 5
β’ (π β
((((invgβπΉ)β(1rβπΉ))(.rβπΉ)π΅) Β· π) = (((invgβπΉ)βπ΅) Β· π)) |
24 | 9, 21 | ringidcl 19994 |
. . . . . . . 8
β’ (πΉ β Ring β
(1rβπΉ)
β πΎ) |
25 | 5, 24 | syl 17 |
. . . . . . 7
β’ (π β (1rβπΉ) β πΎ) |
26 | 9, 10 | grpinvcl 18803 |
. . . . . . 7
β’ ((πΉ β Grp β§
(1rβπΉ)
β πΎ) β
((invgβπΉ)β(1rβπΉ)) β πΎ) |
27 | 7, 25, 26 | syl2anc 585 |
. . . . . 6
β’ (π β
((invgβπΉ)β(1rβπΉ)) β πΎ) |
28 | 14, 3, 16, 9, 20 | lmodvsass 20362 |
. . . . . 6
β’ ((π β LMod β§
(((invgβπΉ)β(1rβπΉ)) β πΎ β§ π΅ β πΎ β§ π β π)) β ((((invgβπΉ)β(1rβπΉ))(.rβπΉ)π΅) Β· π) = (((invgβπΉ)β(1rβπΉ)) Β· (π΅ Β· π))) |
29 | 1, 27, 8, 13, 28 | syl13anc 1373 |
. . . . 5
β’ (π β
((((invgβπΉ)β(1rβπΉ))(.rβπΉ)π΅) Β· π) = (((invgβπΉ)β(1rβπΉ)) Β· (π΅ Β· π))) |
30 | 23, 29 | eqtr3d 2775 |
. . . 4
β’ (π β
(((invgβπΉ)βπ΅) Β· π) = (((invgβπΉ)β(1rβπΉ)) Β· (π΅ Β· π))) |
31 | 30 | oveq2d 7374 |
. . 3
β’ (π β ((π΄ Β· π)(+gβπ)(((invgβπΉ)βπ΅) Β· π)) = ((π΄ Β· π)(+gβπ)(((invgβπΉ)β(1rβπΉ)) Β· (π΅ Β· π)))) |
32 | 19, 31 | eqtrd 2773 |
. 2
β’ (π β ((π΄(+gβπΉ)((invgβπΉ)βπ΅)) Β· π) = ((π΄ Β· π)(+gβπ)(((invgβπΉ)β(1rβπΉ)) Β· (π΅ Β· π)))) |
33 | | lmodsubdir.s |
. . . . 5
β’ π = (-gβπΉ) |
34 | 9, 17, 10, 33 | grpsubval 18801 |
. . . 4
β’ ((π΄ β πΎ β§ π΅ β πΎ) β (π΄ππ΅) = (π΄(+gβπΉ)((invgβπΉ)βπ΅))) |
35 | 2, 8, 34 | syl2anc 585 |
. . 3
β’ (π β (π΄ππ΅) = (π΄(+gβπΉ)((invgβπΉ)βπ΅))) |
36 | 35 | oveq1d 7373 |
. 2
β’ (π β ((π΄ππ΅) Β· π) = ((π΄(+gβπΉ)((invgβπΉ)βπ΅)) Β· π)) |
37 | 14, 3, 16, 9 | lmodvscl 20354 |
. . . 4
β’ ((π β LMod β§ π΄ β πΎ β§ π β π) β (π΄ Β· π) β π) |
38 | 1, 2, 13, 37 | syl3anc 1372 |
. . 3
β’ (π β (π΄ Β· π) β π) |
39 | 14, 3, 16, 9 | lmodvscl 20354 |
. . . 4
β’ ((π β LMod β§ π΅ β πΎ β§ π β π) β (π΅ Β· π) β π) |
40 | 1, 8, 13, 39 | syl3anc 1372 |
. . 3
β’ (π β (π΅ Β· π) β π) |
41 | | lmodsubdir.m |
. . . 4
β’ β =
(-gβπ) |
42 | 14, 15, 41, 3, 16, 10, 21 | lmodvsubval2 20392 |
. . 3
β’ ((π β LMod β§ (π΄ Β· π) β π β§ (π΅ Β· π) β π) β ((π΄ Β· π) β (π΅ Β· π)) = ((π΄ Β· π)(+gβπ)(((invgβπΉ)β(1rβπΉ)) Β· (π΅ Β· π)))) |
43 | 1, 38, 40, 42 | syl3anc 1372 |
. 2
β’ (π β ((π΄ Β· π) β (π΅ Β· π)) = ((π΄ Β· π)(+gβπ)(((invgβπΉ)β(1rβπΉ)) Β· (π΅ Β· π)))) |
44 | 32, 36, 43 | 3eqtr4d 2783 |
1
β’ (π β ((π΄ππ΅) Β· π) = ((π΄ Β· π) β (π΅ Β· π))) |