Step | Hyp | Ref
| Expression |
1 | | lflnegcl.w |
. . . . . . 7
β’ (π β π β LMod) |
2 | | lflnegcl.r |
. . . . . . . 8
β’ π
= (Scalarβπ) |
3 | 2 | lmodring 20344 |
. . . . . . 7
β’ (π β LMod β π
β Ring) |
4 | 1, 3 | syl 17 |
. . . . . 6
β’ (π β π
β Ring) |
5 | | ringgrp 19974 |
. . . . . 6
β’ (π
β Ring β π
β Grp) |
6 | 4, 5 | syl 17 |
. . . . 5
β’ (π β π
β Grp) |
7 | 6 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β π) β π
β Grp) |
8 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π) β π β LMod) |
9 | | lflnegcl.g |
. . . . . 6
β’ (π β πΊ β πΉ) |
10 | 9 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π) β πΊ β πΉ) |
11 | | simpr 486 |
. . . . 5
β’ ((π β§ π₯ β π) β π₯ β π) |
12 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβπ
) |
13 | | lflnegcl.v |
. . . . . 6
β’ π = (Baseβπ) |
14 | | lflnegcl.f |
. . . . . 6
β’ πΉ = (LFnlβπ) |
15 | 2, 12, 13, 14 | lflcl 37572 |
. . . . 5
β’ ((π β LMod β§ πΊ β πΉ β§ π₯ β π) β (πΊβπ₯) β (Baseβπ
)) |
16 | 8, 10, 11, 15 | syl3anc 1372 |
. . . 4
β’ ((π β§ π₯ β π) β (πΊβπ₯) β (Baseβπ
)) |
17 | | lflnegcl.i |
. . . . 5
β’ πΌ = (invgβπ
) |
18 | 12, 17 | grpinvcl 18803 |
. . . 4
β’ ((π
β Grp β§ (πΊβπ₯) β (Baseβπ
)) β (πΌβ(πΊβπ₯)) β (Baseβπ
)) |
19 | 7, 16, 18 | syl2anc 585 |
. . 3
β’ ((π β§ π₯ β π) β (πΌβ(πΊβπ₯)) β (Baseβπ
)) |
20 | | lflnegcl.n |
. . 3
β’ π = (π₯ β π β¦ (πΌβ(πΊβπ₯))) |
21 | 19, 20 | fmptd 7063 |
. 2
β’ (π β π:πβΆ(Baseβπ
)) |
22 | | ringabl 20007 |
. . . . . . . 8
β’ (π
β Ring β π
β Abel) |
23 | 4, 22 | syl 17 |
. . . . . . 7
β’ (π β π
β Abel) |
24 | 23 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β π
β Abel) |
25 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β π
β Ring) |
26 | | simpr1 1195 |
. . . . . . 7
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β π β (Baseβπ
)) |
27 | 1 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β π β LMod) |
28 | 9 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β πΊ β πΉ) |
29 | | simpr2 1196 |
. . . . . . . 8
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β π¦ β π) |
30 | 2, 12, 13, 14 | lflcl 37572 |
. . . . . . . 8
β’ ((π β LMod β§ πΊ β πΉ β§ π¦ β π) β (πΊβπ¦) β (Baseβπ
)) |
31 | 27, 28, 29, 30 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β (πΊβπ¦) β (Baseβπ
)) |
32 | | eqid 2733 |
. . . . . . . 8
β’
(.rβπ
) = (.rβπ
) |
33 | 12, 32 | ringcl 19986 |
. . . . . . 7
β’ ((π
β Ring β§ π β (Baseβπ
) β§ (πΊβπ¦) β (Baseβπ
)) β (π(.rβπ
)(πΊβπ¦)) β (Baseβπ
)) |
34 | 25, 26, 31, 33 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β (π(.rβπ
)(πΊβπ¦)) β (Baseβπ
)) |
35 | | simpr3 1197 |
. . . . . . 7
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β π§ β π) |
36 | 2, 12, 13, 14 | lflcl 37572 |
. . . . . . 7
β’ ((π β LMod β§ πΊ β πΉ β§ π§ β π) β (πΊβπ§) β (Baseβπ
)) |
37 | 27, 28, 35, 36 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β (πΊβπ§) β (Baseβπ
)) |
38 | | eqid 2733 |
. . . . . . 7
β’
(+gβπ
) = (+gβπ
) |
39 | 12, 38, 17 | ablinvadd 19593 |
. . . . . 6
β’ ((π
β Abel β§ (π(.rβπ
)(πΊβπ¦)) β (Baseβπ
) β§ (πΊβπ§) β (Baseβπ
)) β (πΌβ((π(.rβπ
)(πΊβπ¦))(+gβπ
)(πΊβπ§))) = ((πΌβ(π(.rβπ
)(πΊβπ¦)))(+gβπ
)(πΌβ(πΊβπ§)))) |
40 | 24, 34, 37, 39 | syl3anc 1372 |
. . . . 5
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β (πΌβ((π(.rβπ
)(πΊβπ¦))(+gβπ
)(πΊβπ§))) = ((πΌβ(π(.rβπ
)(πΊβπ¦)))(+gβπ
)(πΌβ(πΊβπ§)))) |
41 | | eqid 2733 |
. . . . . . . 8
β’
(+gβπ) = (+gβπ) |
42 | | eqid 2733 |
. . . . . . . 8
β’ (
Β·π βπ) = ( Β·π
βπ) |
43 | 13, 41, 2, 42, 12, 38, 32, 14 | lfli 37569 |
. . . . . . 7
β’ ((π β LMod β§ πΊ β πΉ β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β (πΊβ((π( Β·π
βπ)π¦)(+gβπ)π§)) = ((π(.rβπ
)(πΊβπ¦))(+gβπ
)(πΊβπ§))) |
44 | 27, 28, 26, 29, 35, 43 | syl113anc 1383 |
. . . . . 6
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β (πΊβ((π( Β·π
βπ)π¦)(+gβπ)π§)) = ((π(.rβπ
)(πΊβπ¦))(+gβπ
)(πΊβπ§))) |
45 | 44 | fveq2d 6847 |
. . . . 5
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β (πΌβ(πΊβ((π( Β·π
βπ)π¦)(+gβπ)π§))) = (πΌβ((π(.rβπ
)(πΊβπ¦))(+gβπ
)(πΊβπ§)))) |
46 | 12, 32, 17, 25, 26, 31 | ringmneg2 20026 |
. . . . . 6
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β (π(.rβπ
)(πΌβ(πΊβπ¦))) = (πΌβ(π(.rβπ
)(πΊβπ¦)))) |
47 | 46 | oveq1d 7373 |
. . . . 5
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β ((π(.rβπ
)(πΌβ(πΊβπ¦)))(+gβπ
)(πΌβ(πΊβπ§))) = ((πΌβ(π(.rβπ
)(πΊβπ¦)))(+gβπ
)(πΌβ(πΊβπ§)))) |
48 | 40, 45, 47 | 3eqtr4d 2783 |
. . . 4
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β (πΌβ(πΊβ((π( Β·π
βπ)π¦)(+gβπ)π§))) = ((π(.rβπ
)(πΌβ(πΊβπ¦)))(+gβπ
)(πΌβ(πΊβπ§)))) |
49 | 13, 2, 42, 12 | lmodvscl 20354 |
. . . . . . 7
β’ ((π β LMod β§ π β (Baseβπ
) β§ π¦ β π) β (π( Β·π
βπ)π¦) β π) |
50 | 27, 26, 29, 49 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β (π( Β·π
βπ)π¦) β π) |
51 | 13, 41 | lmodvacl 20351 |
. . . . . 6
β’ ((π β LMod β§ (π(
Β·π βπ)π¦) β π β§ π§ β π) β ((π( Β·π
βπ)π¦)(+gβπ)π§) β π) |
52 | 27, 50, 35, 51 | syl3anc 1372 |
. . . . 5
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β ((π( Β·π
βπ)π¦)(+gβπ)π§) β π) |
53 | | 2fveq3 6848 |
. . . . . 6
β’ (π₯ = ((π( Β·π
βπ)π¦)(+gβπ)π§) β (πΌβ(πΊβπ₯)) = (πΌβ(πΊβ((π( Β·π
βπ)π¦)(+gβπ)π§)))) |
54 | | fvex 6856 |
. . . . . 6
β’ (πΌβ(πΊβ((π( Β·π
βπ)π¦)(+gβπ)π§))) β V |
55 | 53, 20, 54 | fvmpt 6949 |
. . . . 5
β’ (((π(
Β·π βπ)π¦)(+gβπ)π§) β π β (πβ((π( Β·π
βπ)π¦)(+gβπ)π§)) = (πΌβ(πΊβ((π( Β·π
βπ)π¦)(+gβπ)π§)))) |
56 | 52, 55 | syl 17 |
. . . 4
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β (πβ((π( Β·π
βπ)π¦)(+gβπ)π§)) = (πΌβ(πΊβ((π( Β·π
βπ)π¦)(+gβπ)π§)))) |
57 | | 2fveq3 6848 |
. . . . . . . 8
β’ (π₯ = π¦ β (πΌβ(πΊβπ₯)) = (πΌβ(πΊβπ¦))) |
58 | | fvex 6856 |
. . . . . . . 8
β’ (πΌβ(πΊβπ¦)) β V |
59 | 57, 20, 58 | fvmpt 6949 |
. . . . . . 7
β’ (π¦ β π β (πβπ¦) = (πΌβ(πΊβπ¦))) |
60 | 29, 59 | syl 17 |
. . . . . 6
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β (πβπ¦) = (πΌβ(πΊβπ¦))) |
61 | 60 | oveq2d 7374 |
. . . . 5
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β (π(.rβπ
)(πβπ¦)) = (π(.rβπ
)(πΌβ(πΊβπ¦)))) |
62 | | 2fveq3 6848 |
. . . . . . 7
β’ (π₯ = π§ β (πΌβ(πΊβπ₯)) = (πΌβ(πΊβπ§))) |
63 | | fvex 6856 |
. . . . . . 7
β’ (πΌβ(πΊβπ§)) β V |
64 | 62, 20, 63 | fvmpt 6949 |
. . . . . 6
β’ (π§ β π β (πβπ§) = (πΌβ(πΊβπ§))) |
65 | 35, 64 | syl 17 |
. . . . 5
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β (πβπ§) = (πΌβ(πΊβπ§))) |
66 | 61, 65 | oveq12d 7376 |
. . . 4
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β ((π(.rβπ
)(πβπ¦))(+gβπ
)(πβπ§)) = ((π(.rβπ
)(πΌβ(πΊβπ¦)))(+gβπ
)(πΌβ(πΊβπ§)))) |
67 | 48, 56, 66 | 3eqtr4d 2783 |
. . 3
β’ ((π β§ (π β (Baseβπ
) β§ π¦ β π β§ π§ β π)) β (πβ((π( Β·π
βπ)π¦)(+gβπ)π§)) = ((π(.rβπ
)(πβπ¦))(+gβπ
)(πβπ§))) |
68 | 67 | ralrimivvva 3197 |
. 2
β’ (π β βπ β (Baseβπ
)βπ¦ β π βπ§ β π (πβ((π( Β·π
βπ)π¦)(+gβπ)π§)) = ((π(.rβπ
)(πβπ¦))(+gβπ
)(πβπ§))) |
69 | 13, 41, 2, 42, 12, 38, 32, 14 | islfl 37568 |
. . 3
β’ (π β LMod β (π β πΉ β (π:πβΆ(Baseβπ
) β§ βπ β (Baseβπ
)βπ¦ β π βπ§ β π (πβ((π( Β·π
βπ)π¦)(+gβπ)π§)) = ((π(.rβπ
)(πβπ¦))(+gβπ
)(πβπ§))))) |
70 | 1, 69 | syl 17 |
. 2
β’ (π β (π β πΉ β (π:πβΆ(Baseβπ
) β§ βπ β (Baseβπ
)βπ¦ β π βπ§ β π (πβ((π( Β·π
βπ)π¦)(+gβπ)π§)) = ((π(.rβπ
)(πβπ¦))(+gβπ
)(πβπ§))))) |
71 | 21, 68, 70 | mpbir2and 712 |
1
β’ (π β π β πΉ) |