Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . . . 5
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β π β LMod) |
2 | | simp3l 1202 |
. . . . 5
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β π β π) |
3 | | lflsub.d |
. . . . . . . . . 10
β’ π· = (Scalarβπ) |
4 | 3 | lmodring 20373 |
. . . . . . . . 9
β’ (π β LMod β π· β Ring) |
5 | 4 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β π· β Ring) |
6 | | ringgrp 19977 |
. . . . . . . 8
β’ (π· β Ring β π· β Grp) |
7 | 5, 6 | syl 17 |
. . . . . . 7
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β π· β Grp) |
8 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβπ·) =
(Baseβπ·) |
9 | | eqid 2733 |
. . . . . . . . 9
β’
(1rβπ·) = (1rβπ·) |
10 | 8, 9 | ringidcl 19997 |
. . . . . . . 8
β’ (π· β Ring β
(1rβπ·)
β (Baseβπ·)) |
11 | 5, 10 | syl 17 |
. . . . . . 7
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β (1rβπ·) β (Baseβπ·)) |
12 | | eqid 2733 |
. . . . . . . 8
β’
(invgβπ·) = (invgβπ·) |
13 | 8, 12 | grpinvcl 18806 |
. . . . . . 7
β’ ((π· β Grp β§
(1rβπ·)
β (Baseβπ·))
β ((invgβπ·)β(1rβπ·)) β (Baseβπ·)) |
14 | 7, 11, 13 | syl2anc 585 |
. . . . . 6
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β ((invgβπ·)β(1rβπ·)) β (Baseβπ·)) |
15 | | simp3r 1203 |
. . . . . 6
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β π β π) |
16 | | lflsub.v |
. . . . . . 7
β’ π = (Baseβπ) |
17 | | eqid 2733 |
. . . . . . 7
β’ (
Β·π βπ) = ( Β·π
βπ) |
18 | 16, 3, 17, 8 | lmodvscl 20383 |
. . . . . 6
β’ ((π β LMod β§
((invgβπ·)β(1rβπ·)) β (Baseβπ·) β§ π β π) β (((invgβπ·)β(1rβπ·))(
Β·π βπ)π) β π) |
19 | 1, 14, 15, 18 | syl3anc 1372 |
. . . . 5
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β (((invgβπ·)β(1rβπ·))(
Β·π βπ)π) β π) |
20 | | eqid 2733 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
21 | 16, 20 | lmodcom 20412 |
. . . . 5
β’ ((π β LMod β§ π β π β§ (((invgβπ·)β(1rβπ·))(
Β·π βπ)π) β π) β (π(+gβπ)(((invgβπ·)β(1rβπ·))(
Β·π βπ)π)) = ((((invgβπ·)β(1rβπ·))(
Β·π βπ)π)(+gβπ)π)) |
22 | 1, 2, 19, 21 | syl3anc 1372 |
. . . 4
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β (π(+gβπ)(((invgβπ·)β(1rβπ·))(
Β·π βπ)π)) = ((((invgβπ·)β(1rβπ·))(
Β·π βπ)π)(+gβπ)π)) |
23 | 22 | fveq2d 6850 |
. . 3
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β (πΊβ(π(+gβπ)(((invgβπ·)β(1rβπ·))(
Β·π βπ)π))) = (πΊβ((((invgβπ·)β(1rβπ·))(
Β·π βπ)π)(+gβπ)π))) |
24 | | simp2 1138 |
. . . 4
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β πΊ β πΉ) |
25 | | eqid 2733 |
. . . . 5
β’
(+gβπ·) = (+gβπ·) |
26 | | eqid 2733 |
. . . . 5
β’
(.rβπ·) = (.rβπ·) |
27 | | lflsub.f |
. . . . 5
β’ πΉ = (LFnlβπ) |
28 | 16, 20, 3, 17, 8, 25, 26, 27 | lfli 37573 |
. . . 4
β’ ((π β LMod β§ πΊ β πΉ β§ (((invgβπ·)β(1rβπ·)) β (Baseβπ·) β§ π β π β§ π β π)) β (πΊβ((((invgβπ·)β(1rβπ·))(
Β·π βπ)π)(+gβπ)π)) = ((((invgβπ·)β(1rβπ·))(.rβπ·)(πΊβπ))(+gβπ·)(πΊβπ))) |
29 | 1, 24, 14, 15, 2, 28 | syl113anc 1383 |
. . 3
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β (πΊβ((((invgβπ·)β(1rβπ·))(
Β·π βπ)π)(+gβπ)π)) = ((((invgβπ·)β(1rβπ·))(.rβπ·)(πΊβπ))(+gβπ·)(πΊβπ))) |
30 | 3, 8, 16, 27 | lflcl 37576 |
. . . . . . 7
β’ ((π β LMod β§ πΊ β πΉ β§ π β π) β (πΊβπ) β (Baseβπ·)) |
31 | 30 | 3adant3l 1181 |
. . . . . 6
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β (πΊβπ) β (Baseβπ·)) |
32 | 8, 26, 9, 12, 5, 31 | ringnegl 20026 |
. . . . 5
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β (((invgβπ·)β(1rβπ·))(.rβπ·)(πΊβπ)) = ((invgβπ·)β(πΊβπ))) |
33 | 32 | oveq1d 7376 |
. . . 4
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β ((((invgβπ·)β(1rβπ·))(.rβπ·)(πΊβπ))(+gβπ·)(πΊβπ)) = (((invgβπ·)β(πΊβπ))(+gβπ·)(πΊβπ))) |
34 | | ringabl 20010 |
. . . . . 6
β’ (π· β Ring β π· β Abel) |
35 | 5, 34 | syl 17 |
. . . . 5
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β π· β Abel) |
36 | 8, 12 | grpinvcl 18806 |
. . . . . 6
β’ ((π· β Grp β§ (πΊβπ) β (Baseβπ·)) β ((invgβπ·)β(πΊβπ)) β (Baseβπ·)) |
37 | 7, 31, 36 | syl2anc 585 |
. . . . 5
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β ((invgβπ·)β(πΊβπ)) β (Baseβπ·)) |
38 | 3, 8, 16, 27 | lflcl 37576 |
. . . . . 6
β’ ((π β LMod β§ πΊ β πΉ β§ π β π) β (πΊβπ) β (Baseβπ·)) |
39 | 38 | 3adant3r 1182 |
. . . . 5
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β (πΊβπ) β (Baseβπ·)) |
40 | 8, 25 | ablcom 19589 |
. . . . 5
β’ ((π· β Abel β§
((invgβπ·)β(πΊβπ)) β (Baseβπ·) β§ (πΊβπ) β (Baseβπ·)) β (((invgβπ·)β(πΊβπ))(+gβπ·)(πΊβπ)) = ((πΊβπ)(+gβπ·)((invgβπ·)β(πΊβπ)))) |
41 | 35, 37, 39, 40 | syl3anc 1372 |
. . . 4
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β (((invgβπ·)β(πΊβπ))(+gβπ·)(πΊβπ)) = ((πΊβπ)(+gβπ·)((invgβπ·)β(πΊβπ)))) |
42 | 33, 41 | eqtrd 2773 |
. . 3
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β ((((invgβπ·)β(1rβπ·))(.rβπ·)(πΊβπ))(+gβπ·)(πΊβπ)) = ((πΊβπ)(+gβπ·)((invgβπ·)β(πΊβπ)))) |
43 | 23, 29, 42 | 3eqtrd 2777 |
. 2
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β (πΊβ(π(+gβπ)(((invgβπ·)β(1rβπ·))(
Β·π βπ)π))) = ((πΊβπ)(+gβπ·)((invgβπ·)β(πΊβπ)))) |
44 | | lflsub.a |
. . . . 5
β’ β =
(-gβπ) |
45 | 16, 20, 44, 3, 17, 12, 9 | lmodvsubval2 20421 |
. . . 4
β’ ((π β LMod β§ π β π β§ π β π) β (π β π) = (π(+gβπ)(((invgβπ·)β(1rβπ·))(
Β·π βπ)π))) |
46 | 1, 2, 15, 45 | syl3anc 1372 |
. . 3
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β (π β π) = (π(+gβπ)(((invgβπ·)β(1rβπ·))(
Β·π βπ)π))) |
47 | 46 | fveq2d 6850 |
. 2
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β (πΊβ(π β π)) = (πΊβ(π(+gβπ)(((invgβπ·)β(1rβπ·))(
Β·π βπ)π)))) |
48 | | lflsub.m |
. . . 4
β’ π = (-gβπ·) |
49 | 8, 25, 12, 48 | grpsubval 18804 |
. . 3
β’ (((πΊβπ) β (Baseβπ·) β§ (πΊβπ) β (Baseβπ·)) β ((πΊβπ)π(πΊβπ)) = ((πΊβπ)(+gβπ·)((invgβπ·)β(πΊβπ)))) |
50 | 39, 31, 49 | syl2anc 585 |
. 2
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β ((πΊβπ)π(πΊβπ)) = ((πΊβπ)(+gβπ·)((invgβπ·)β(πΊβπ)))) |
51 | 43, 47, 50 | 3eqtr4d 2783 |
1
β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β (πΊβ(π β π)) = ((πΊβπ)π(πΊβπ))) |