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