Step | Hyp | Ref
| Expression |
1 | | df-cvs 24503 |
. . 3
β’
βVec = (βMod β© LVec) |
2 | 1 | elin2 4158 |
. 2
β’ (π β βVec β (π β βMod β§ π β LVec)) |
3 | | lveclmod 20582 |
. . . . 5
β’ (π β LVec β π β LMod) |
4 | | lmodabl 20384 |
. . . . 5
β’ (π β LMod β π β Abel) |
5 | 3, 4 | syl 17 |
. . . 4
β’ (π β LVec β π β Abel) |
6 | 5 | adantl 483 |
. . 3
β’ ((π β βMod β§ π β LVec) β π β Abel) |
7 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
8 | | cvsi.s |
. . . . . 6
β’ π =
(Baseβ(Scalarβπ)) |
9 | 7, 8 | clmsscn 24458 |
. . . . 5
β’ (π β βMod β π β
β) |
10 | | clmlmod 24446 |
. . . . . 6
β’ (π β βMod β π β LMod) |
11 | | cvsi.x |
. . . . . . 7
β’ π = (Baseβπ) |
12 | | cvsi.m |
. . . . . . 7
β’ β = (
Β·sf βπ) |
13 | 11, 7, 8, 12 | lmodscaf 20359 |
. . . . . 6
β’ (π β LMod β β
:(π Γ π)βΆπ) |
14 | 10, 13 | syl 17 |
. . . . 5
β’ (π β βMod β β
:(π Γ π)βΆπ) |
15 | 9, 14 | jca 513 |
. . . 4
β’ (π β βMod β (π β β β§ β
:(π Γ π)βΆπ)) |
16 | 15 | adantr 482 |
. . 3
β’ ((π β βMod β§ π β LVec) β (π β β β§ β
:(π Γ π)βΆπ)) |
17 | | cvsi.t |
. . . . . . 7
β’ Β· = (
Β·π βπ) |
18 | 11, 17 | clmvs1 24472 |
. . . . . 6
β’ ((π β βMod β§ π₯ β π) β (1 Β· π₯) = π₯) |
19 | 10 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β βMod β§ π₯ β π) β π β LMod) |
20 | 19 | ad2antrr 725 |
. . . . . . . . . 10
β’ ((((π β βMod β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β π β LMod) |
21 | | simplr 768 |
. . . . . . . . . 10
β’ ((((π β βMod β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β π¦ β π) |
22 | | simpllr 775 |
. . . . . . . . . 10
β’ ((((π β βMod β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β π₯ β π) |
23 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β βMod β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β π§ β π) |
24 | | cvsi.a |
. . . . . . . . . . 11
β’ + =
(+gβπ) |
25 | 11, 24, 7, 17, 8 | lmodvsdi 20360 |
. . . . . . . . . 10
β’ ((π β LMod β§ (π¦ β π β§ π₯ β π β§ π§ β π)) β (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§))) |
26 | 20, 21, 22, 23, 25 | syl13anc 1373 |
. . . . . . . . 9
β’ ((((π β βMod β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§))) |
27 | 26 | ralrimiva 3140 |
. . . . . . . 8
β’ (((π β βMod β§ π₯ β π) β§ π¦ β π) β βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§))) |
28 | 7 | clmadd 24453 |
. . . . . . . . . . . . . 14
β’ (π β βMod β + =
(+gβ(Scalarβπ))) |
29 | 28 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β βMod β§ π₯ β π) β§ π¦ β π) β + =
(+gβ(Scalarβπ))) |
30 | 29 | oveqdr 7386 |
. . . . . . . . . . . 12
β’ ((((π β βMod β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β (π¦ + π§) = (π¦(+gβ(Scalarβπ))π§)) |
31 | 30 | oveq1d 7373 |
. . . . . . . . . . 11
β’ ((((π β βMod β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β ((π¦ + π§) Β· π₯) = ((π¦(+gβ(Scalarβπ))π§) Β· π₯)) |
32 | 19 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β βMod β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β π β LMod) |
33 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π β βMod β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β π¦ β π) |
34 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π β βMod β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β π§ β π) |
35 | | simpllr 775 |
. . . . . . . . . . . 12
β’ ((((π β βMod β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β π₯ β π) |
36 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ)) |
37 | 11, 24, 7, 17, 8, 36 | lmodvsdir 20361 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ (π¦ β π β§ π§ β π β§ π₯ β π)) β ((π¦(+gβ(Scalarβπ))π§) Β· π₯) = ((π¦ Β· π₯) + (π§ Β· π₯))) |
38 | 32, 33, 34, 35, 37 | syl13anc 1373 |
. . . . . . . . . . 11
β’ ((((π β βMod β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β ((π¦(+gβ(Scalarβπ))π§) Β· π₯) = ((π¦ Β· π₯) + (π§ Β· π₯))) |
39 | 31, 38 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((((π β βMod β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β ((π¦ + π§) Β· π₯) = ((π¦ Β· π₯) + (π§ Β· π₯))) |
40 | 7 | clmmul 24454 |
. . . . . . . . . . . . . 14
β’ (π β βMod β
Β· = (.rβ(Scalarβπ))) |
41 | 40 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β βMod β§ π₯ β π) β§ π¦ β π) β Β· =
(.rβ(Scalarβπ))) |
42 | 41 | oveqdr 7386 |
. . . . . . . . . . . 12
β’ ((((π β βMod β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β (π¦ Β· π§) = (π¦(.rβ(Scalarβπ))π§)) |
43 | 42 | oveq1d 7373 |
. . . . . . . . . . 11
β’ ((((π β βMod β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β ((π¦ Β· π§) Β· π₯) = ((π¦(.rβ(Scalarβπ))π§) Β· π₯)) |
44 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(.rβ(Scalarβπ)) =
(.rβ(Scalarβπ)) |
45 | 11, 7, 17, 8, 44 | lmodvsass 20362 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ (π¦ β π β§ π§ β π β§ π₯ β π)) β ((π¦(.rβ(Scalarβπ))π§) Β· π₯) = (π¦ Β· (π§ Β· π₯))) |
46 | 32, 33, 34, 35, 45 | syl13anc 1373 |
. . . . . . . . . . 11
β’ ((((π β βMod β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β ((π¦(.rβ(Scalarβπ))π§) Β· π₯) = (π¦ Β· (π§ Β· π₯))) |
47 | 43, 46 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((((π β βMod β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β ((π¦ Β· π§) Β· π₯) = (π¦ Β· (π§ Β· π₯))) |
48 | 39, 47 | jca 513 |
. . . . . . . . 9
β’ ((((π β βMod β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β (((π¦ + π§) Β· π₯) = ((π¦ Β· π₯) + (π§ Β· π₯)) β§ ((π¦ Β· π§) Β· π₯) = (π¦ Β· (π§ Β· π₯)))) |
49 | 48 | ralrimiva 3140 |
. . . . . . . 8
β’ (((π β βMod β§ π₯ β π) β§ π¦ β π) β βπ§ β π (((π¦ + π§) Β· π₯) = ((π¦ Β· π₯) + (π§ Β· π₯)) β§ ((π¦ Β· π§) Β· π₯) = (π¦ Β· (π§ Β· π₯)))) |
50 | 27, 49 | jca 513 |
. . . . . . 7
β’ (((π β βMod β§ π₯ β π) β§ π¦ β π) β (βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β π (((π¦ + π§) Β· π₯) = ((π¦ Β· π₯) + (π§ Β· π₯)) β§ ((π¦ Β· π§) Β· π₯) = (π¦ Β· (π§ Β· π₯))))) |
51 | 50 | ralrimiva 3140 |
. . . . . 6
β’ ((π β βMod β§ π₯ β π) β βπ¦ β π (βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β π (((π¦ + π§) Β· π₯) = ((π¦ Β· π₯) + (π§ Β· π₯)) β§ ((π¦ Β· π§) Β· π₯) = (π¦ Β· (π§ Β· π₯))))) |
52 | 18, 51 | jca 513 |
. . . . 5
β’ ((π β βMod β§ π₯ β π) β ((1 Β· π₯) = π₯ β§ βπ¦ β π (βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β π (((π¦ + π§) Β· π₯) = ((π¦ Β· π₯) + (π§ Β· π₯)) β§ ((π¦ Β· π§) Β· π₯) = (π¦ Β· (π§ Β· π₯)))))) |
53 | 52 | ralrimiva 3140 |
. . . 4
β’ (π β βMod β
βπ₯ β π ((1 Β· π₯) = π₯ β§ βπ¦ β π (βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β π (((π¦ + π§) Β· π₯) = ((π¦ Β· π₯) + (π§ Β· π₯)) β§ ((π¦ Β· π§) Β· π₯) = (π¦ Β· (π§ Β· π₯)))))) |
54 | 53 | adantr 482 |
. . 3
β’ ((π β βMod β§ π β LVec) β
βπ₯ β π ((1 Β· π₯) = π₯ β§ βπ¦ β π (βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β π (((π¦ + π§) Β· π₯) = ((π¦ Β· π₯) + (π§ Β· π₯)) β§ ((π¦ Β· π§) Β· π₯) = (π¦ Β· (π§ Β· π₯)))))) |
55 | 6, 16, 54 | 3jca 1129 |
. 2
β’ ((π β βMod β§ π β LVec) β (π β Abel β§ (π β β β§ β
:(π Γ π)βΆπ) β§ βπ₯ β π ((1 Β· π₯) = π₯ β§ βπ¦ β π (βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β π (((π¦ + π§) Β· π₯) = ((π¦ Β· π₯) + (π§ Β· π₯)) β§ ((π¦ Β· π§) Β· π₯) = (π¦ Β· (π§ Β· π₯))))))) |
56 | 2, 55 | sylbi 216 |
1
β’ (π β βVec β (π β Abel β§ (π β β β§ β
:(π Γ π)βΆπ) β§ βπ₯ β π ((1 Β· π₯) = π₯ β§ βπ¦ β π (βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β π (((π¦ + π§) Β· π₯) = ((π¦ Β· π₯) + (π§ Β· π₯)) β§ ((π¦ Β· π§) Β· π₯) = (π¦ Β· (π§ Β· π₯))))))) |